VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866910543725461504 |
|---|---|
| author | Antón, Anna Lena Duque Müller, Johannes Schmitz, Philipp Jauch, Tobias Wezel, Alex Deutschmann, Lucas Fadiheh, Mohammad Rahmani Stoffel, Dominik Kunz, Wolfgang |
| author_facet | Antón, Anna Lena Duque Müller, Johannes Schmitz, Philipp Jauch, Tobias Wezel, Alex Deutschmann, Lucas Fadiheh, Mohammad Rahmani Stoffel, Dominik Kunz, Wolfgang |
| contents | Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. This paper presents VeriCHERI, a novel approach to security verification. It is conceptionally different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2407_18679 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL Antón, Anna Lena Duque Müller, Johannes Schmitz, Philipp Jauch, Tobias Wezel, Alex Deutschmann, Lucas Fadiheh, Mohammad Rahmani Stoffel, Dominik Kunz, Wolfgang Cryptography and Security Protecting data in memory from attackers continues to be a concern in computing systems. CHERI is a promising approach to achieve such protection, by providing and enforcing fine-grained memory protection directly in the hardware. Creating trust for the entire system stack, however, requires a gap-free verification of CHERI's hardware-based protection mechanisms. Existing verification methods for CHERI target the abstract ISA model rather than the underlying hardware implementation. Fully ensuring the CHERI security guarantees for a concrete RTL implementation is a challenge in previous flows and demands high manual efforts. This paper presents VeriCHERI, a novel approach to security verification. It is conceptionally different from previous works in that it does not require any ISA specification. Instead of checking compliance with a golden ISA model, we check against well-established global security objectives of confidentiality and integrity. Fully covering these objectives, VeriCHERI uses as few as four unbounded properties to exhaustively prove or disprove any vulnerability. We demonstrate the effectiveness and scalability of VeriCHERI on a RISC-V based processor implementing a CHERI variant. |
| title | VeriCHERI: Exhaustive Formal Security Verification of CHERI at the RTL |
| topic | Cryptography and Security |
| url | https://arxiv.org/abs/2407.18679 |