End-to-end formal verification of a RISC-V processor extended with capability pointers
Capability Hardware Enhanced RISC Instructions (CHERI) extend conventional ISAs with capabilities that can enable fine-grained memory protection and scalable software compartmentalisation. CHERI-RISC-V is an extended version of the RISC-V ISA with support for CHERI, and Flute is an open-source 64-bi...
| Main Authors: | , |
|---|---|
| Format: | Conference item |
| Language: | English |
| Published: |
TU Wien Academic Press/IEEE
2021
|
| _version_ | 1797077828693393408 |
|---|---|
| author | Gao, D Melham, T |
| author_facet | Gao, D Melham, T |
| author_sort | Gao, D |
| collection | OXFORD |
| description | Capability Hardware Enhanced RISC Instructions (CHERI) extend conventional ISAs with capabilities that can enable fine-grained memory protection and scalable software compartmentalisation. CHERI-RISC-V is an extended version of the RISC-V ISA with support for CHERI, and Flute is an open-source 64-bit RISC-V processor with a five-stage, in-order pipeline. This case study presents the formal verification of CHERI-Flute, a modified version of Flute that implements CHERI-RISC-V, against the Sail CHERI-RISC-V specification. To the best of our knowledge, this is the first extensive formal verification of a CHERI-enabled processor.
We first translated relevant portions of the Sail CHERIRISC-V specification to SystemVerilog Assertions. Then we formulated and proved four classes of end-to-end correctness properties about CHERI-Flute, covering the CHERI instructions and certain liveness properties about the entire processor. None of these results are routine—they all rely on novel proof engineering methodologies that extract microarchitectural invariants to serve as lemmas for the end-to-end proofs. This work exposed several previously-unknown bugs in CHERI-Flute, most of which occur in the implementation of
sophisticated combinational logic for certain CHERI instructions. |
| first_indexed | 2024-03-07T00:23:36Z |
| format | Conference item |
| id | oxford-uuid:7d5d94f7-23f0-46ba-a206-41e59fa7744a |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-07T00:23:36Z |
| publishDate | 2021 |
| publisher | TU Wien Academic Press/IEEE |
| record_format | dspace |
| spelling | oxford-uuid:7d5d94f7-23f0-46ba-a206-41e59fa7744a2022-03-26T21:03:14ZEnd-to-end formal verification of a RISC-V processor extended with capability pointersConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7d5d94f7-23f0-46ba-a206-41e59fa7744aEnglishSymplectic ElementsTU Wien Academic Press/IEEE2021Gao, DMelham, TCapability Hardware Enhanced RISC Instructions (CHERI) extend conventional ISAs with capabilities that can enable fine-grained memory protection and scalable software compartmentalisation. CHERI-RISC-V is an extended version of the RISC-V ISA with support for CHERI, and Flute is an open-source 64-bit RISC-V processor with a five-stage, in-order pipeline. This case study presents the formal verification of CHERI-Flute, a modified version of Flute that implements CHERI-RISC-V, against the Sail CHERI-RISC-V specification. To the best of our knowledge, this is the first extensive formal verification of a CHERI-enabled processor. We first translated relevant portions of the Sail CHERIRISC-V specification to SystemVerilog Assertions. Then we formulated and proved four classes of end-to-end correctness properties about CHERI-Flute, covering the CHERI instructions and certain liveness properties about the entire processor. None of these results are routine—they all rely on novel proof engineering methodologies that extract microarchitectural invariants to serve as lemmas for the end-to-end proofs. This work exposed several previously-unknown bugs in CHERI-Flute, most of which occur in the implementation of sophisticated combinational logic for certain CHERI instructions. |
| spellingShingle | Gao, D Melham, T End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title | End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title_full | End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title_fullStr | End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title_full_unstemmed | End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title_short | End-to-end formal verification of a RISC-V processor extended with capability pointers |
| title_sort | end to end formal verification of a risc v processor extended with capability pointers |
| work_keys_str_mv | AT gaod endtoendformalverificationofariscvprocessorextendedwithcapabilitypointers AT melhamt endtoendformalverificationofariscvprocessorextendedwithcapabilitypointers |