RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2024
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916414259986432 |
|---|---|
| author | Hsiao, Yao Nikoleris, Nikos Khyzha, Artem Mulligan, Dominic P. Petri, Gustavo Fletcher, Christopher W. Trippel, Caroline |
| author_facet | Hsiao, Yao Nikoleris, Nikos Khyzha, Artem Mulligan, Dominic P. Petri, Gustavo Fletcher, Christopher W. Trippel, Caroline |
| contents | The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $μ$SPEC models. Despite the efficacy of this approach, a verification gap between $μ$SPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2$μ$SPEC, narrows this gap by automatically synthesizing formally verified $μ$SPEC models from SystemVerilog implementations of simple processors. But, RTL2$μ$SPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path ($μ$PATH, e.g., a cache hit or miss path) -- its single-execution-path assumption.
In this paper, we first propose an automated approach and tool, called RTL2M$μ$PATH, that resolves RTL2$μ$SPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2M$μ$PATH finds a complete set of formally verified $μ$PATHs for each instruction. Next, we make an important observation: an instruction that can exhibit more than one $μ$PATH strongly indicates the presence of a microarchitectural side channel in the input design. Based on this observation, we then propose an automated approach and tool, called SynthLC, that extends RTL2M$μ$PATH with a symbolic information flow analysis to support synthesizing a variety of formally verified leakage contracts from SystemVerilog processor designs. Leakage contracts are foundational to state-of-the-art defenses against hardware side-channel attacks. SynthLC is the first automated methodology for formally verifying hardware adherence to them. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2409_19478 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification Hsiao, Yao Nikoleris, Nikos Khyzha, Artem Mulligan, Dominic P. Petri, Gustavo Fletcher, Christopher W. Trippel, Caroline Cryptography and Security Hardware Architecture The Check tools automate formal memory consistency model and security verification of processors by analyzing abstract models of microarchitectures, called $μ$SPEC models. Despite the efficacy of this approach, a verification gap between $μ$SPEC models, which must be manually written, and RTL limits the Check tools' broad adoption. Our prior work, called RTL2$μ$SPEC, narrows this gap by automatically synthesizing formally verified $μ$SPEC models from SystemVerilog implementations of simple processors. But, RTL2$μ$SPEC assumes input designs where an instruction (e.g., a load) cannot exhibit more than one microarchitectural execution path ($μ$PATH, e.g., a cache hit or miss path) -- its single-execution-path assumption. In this paper, we first propose an automated approach and tool, called RTL2M$μ$PATH, that resolves RTL2$μ$SPEC's single-execution-path assumption. Given a SystemVerilog processor design, instruction encodings, and modest design metadata, RTL2M$μ$PATH finds a complete set of formally verified $μ$PATHs for each instruction. Next, we make an important observation: an instruction that can exhibit more than one $μ$PATH strongly indicates the presence of a microarchitectural side channel in the input design. Based on this observation, we then propose an automated approach and tool, called SynthLC, that extends RTL2M$μ$PATH with a symbolic information flow analysis to support synthesizing a variety of formally verified leakage contracts from SystemVerilog processor designs. Leakage contracts are foundational to state-of-the-art defenses against hardware side-channel attacks. SynthLC is the first automated methodology for formally verifying hardware adherence to them. |
| title | RTL2M$μ$PATH: Multi-$μ$PATH Synthesis with Applications to Hardware Security Verification |
| topic | Cryptography and Security Hardware Architecture |
| url | https://arxiv.org/abs/2409.19478 |