SCorCH : Secure Code for Capability Hardware
Lead Research Organisation:
University of Oxford
Department Name: Computer Science
Abstract
Abstracts are not currently available in GtR for all funded research. This is normally because the abstract was not required at the time of proposal submission, but may be because it included sensitive information such as personal details.
Publications
Park S
(2022)
A Formal CHERI-C Semantics for Verification
Thévenon G
(2024)
B-Side: Binary-Level Static System Call Identification
| Description | Our research has produced the first ever formal verification of a CHERI RISC-V processor with compressed capabilities. The methodology for this may be usable more widely in the semiconductor design sector. |
| Exploitation Route | Semiconductor industry may make use of our verification methodology and maybe even some of the code. |
| Sectors | Digital/Communication/Information Technologies (including Software) |
| Description | Professor Tom Melham and undergraduate student Louis-Emile Ploix have played a key role in a groundbreaking formal verification effort that enhances the quality and reliability of the CHERIoT-Ibex processor. This work, conducted in collaboration with the University of Cambridge, lowRISC CIC, and Microsoft, marks a major advancement in ensuring the correctness of the CHERIoT-Ibex RISC-V processor design through rigorous mathematical proofs. Formal verification is a critical step in processor design, ensuring that a processor behaves exactly as intended under all possible conditions. Traditional methods, such as simulation-based testing, can only check a limited number of scenarios, potentially leaving undetected errors. However, formal verification mathematically proves that a processor's design is correct across all possible executions, significantly improving confidence in its reliability. At the heart of this achievement is a formal verification framework developed by Professor Tom Melham and Louis-Emile Ploix, alongside Alasdair Armstrong from the University of Cambridge. Their framework establishes observational equivalence - a method that ensures the CHERIoT-Ibex hardware behaves identically to its formal specification, known as the RISC-V International Sail specification. This is done using unbounded proofs, meaning the verification holds true for all possible executions, not just a subset of test cases. Oxford's contribution is particularly significant in developing and applying new formal methods to verify the CHERIoT-Ibex processor. Using Cadence Jasperâ„¢ verification tools and Sail support, the team has automated the generation of a SystemVerilog reference model from the Sail specification. This rigorous verification process ensures that the security mechanisms in CHERIoT-Ibex, which protect against memory vulnerabilities and enable secure compartmentalisation, are implemented correctly. |
| First Year Of Impact | 2025 |
| Sector | Digital/Communication/Information Technologies (including Software),Electronics |
| Impact Types | Economic |
| Description | SCorCH : Secure Code for Capability Hardware - Collaboration with Manchester, AWS, and Arm. |
| Organisation | Amazon.com |
| Department | Amazon Web Services |
| Country | United States |
| Sector | Private |
| PI Contribution | Tom Melham an expert in formal hardware verification, model checking, and theorem proving. The Oxford team will contribute with research on novel, automated formal analysis methods applied to software that leverages capability hardware and novel formal verification methods and algorithms applied to the underlying capability hardware architecture. This will involve identifying the most promising and valuable targets for formal analysis, selecting appropriate tooling and algorithms - making innovative, theoretically well-grounded, extensions to these as needed - devising novel analysis methods, and carrying out at-scale case studies. |
| Collaborator Contribution | The SCorCH research collaboration with Manchester involves the Formal Methods (FM), Information Management Group (IMG), and Advanced Processor Technology (APT) research groups at the University of Manchester. The FM group host various other researchers working on formal design and verification, leading on automated reasoning, static analysis of programs, software, and hardware verification. The IMG specializes in design, development and use of data and how users can interact with the data. The APT group is focused on identifying novel ways to exploit the complexity of the billion transistor microchips that semiconductor technology will make commonplace over the next decade. |
| Impact | We have developed a formal proof of the correctness of an implementation of CHERI RISC-V, an open source processor design adapted from the Flute processor by adding capability pointers. The proof effort has been publicised in seminars to the SCorCH group and others, and we are planning publications. |
| Start Year | 2020 |
| Description | SCorCH : Secure Code for Capability Hardware - Collaboration with Manchester, AWS, and Arm. |
| Organisation | Arm Limited |
| Country | United Kingdom |
| Sector | Private |
| PI Contribution | Tom Melham an expert in formal hardware verification, model checking, and theorem proving. The Oxford team will contribute with research on novel, automated formal analysis methods applied to software that leverages capability hardware and novel formal verification methods and algorithms applied to the underlying capability hardware architecture. This will involve identifying the most promising and valuable targets for formal analysis, selecting appropriate tooling and algorithms - making innovative, theoretically well-grounded, extensions to these as needed - devising novel analysis methods, and carrying out at-scale case studies. |
| Collaborator Contribution | The SCorCH research collaboration with Manchester involves the Formal Methods (FM), Information Management Group (IMG), and Advanced Processor Technology (APT) research groups at the University of Manchester. The FM group host various other researchers working on formal design and verification, leading on automated reasoning, static analysis of programs, software, and hardware verification. The IMG specializes in design, development and use of data and how users can interact with the data. The APT group is focused on identifying novel ways to exploit the complexity of the billion transistor microchips that semiconductor technology will make commonplace over the next decade. |
| Impact | We have developed a formal proof of the correctness of an implementation of CHERI RISC-V, an open source processor design adapted from the Flute processor by adding capability pointers. The proof effort has been publicised in seminars to the SCorCH group and others, and we are planning publications. |
| Start Year | 2020 |
| Description | SCorCH : Secure Code for Capability Hardware - Collaboration with Manchester, AWS, and Arm. |
| Organisation | University of Manchester |
| Country | United Kingdom |
| Sector | Academic/University |
| PI Contribution | Tom Melham an expert in formal hardware verification, model checking, and theorem proving. The Oxford team will contribute with research on novel, automated formal analysis methods applied to software that leverages capability hardware and novel formal verification methods and algorithms applied to the underlying capability hardware architecture. This will involve identifying the most promising and valuable targets for formal analysis, selecting appropriate tooling and algorithms - making innovative, theoretically well-grounded, extensions to these as needed - devising novel analysis methods, and carrying out at-scale case studies. |
| Collaborator Contribution | The SCorCH research collaboration with Manchester involves the Formal Methods (FM), Information Management Group (IMG), and Advanced Processor Technology (APT) research groups at the University of Manchester. The FM group host various other researchers working on formal design and verification, leading on automated reasoning, static analysis of programs, software, and hardware verification. The IMG specializes in design, development and use of data and how users can interact with the data. The APT group is focused on identifying novel ways to exploit the complexity of the billion transistor microchips that semiconductor technology will make commonplace over the next decade. |
| Impact | We have developed a formal proof of the correctness of an implementation of CHERI RISC-V, an open source processor design adapted from the Flute processor by adding capability pointers. The proof effort has been publicised in seminars to the SCorCH group and others, and we are planning publications. |
| Start Year | 2020 |
| Title | Artifact for Paper A formal CHERI-C Semantics for Verification |
| Description | To use this artifact, use the TACAS23 VM [1]. Follow the instructions in REPRODUCIBILITY_INSTRUCTIONS.txt to replicate the results in this paper. Note that deps.zip and deps_qemu.zip are extracted before the files/folders are placed in the shared folder for the VM, whereas the other zip files are placed directly in the shared folder for the VM. MINOR UPDATE: When installing the dependencies - at the very beginning - as stated in the instructions, you may encounter the following error:
npm is only required for installing
esy online, but because the package already has
esy preinstalled,
npm and its dependencies are not required). Thus, the error message above can be ignored. [1] https://zenodo.org/record/7113223 |
| Type Of Technology | Software |
| Year Produced | 2023 |
| Open Source License? | Yes |
| URL | https://zenodo.org/record/7504675 |
| Title | Artifact for Paper A formal CHERI-C Semantics for Verification |
| Description | To use this artifact, use the TACAS23 VM [1]. Follow the instructions in REPRODUCIBILITY_INSTRUCTIONS.txt to replicate the results in this paper. Note that deps.zip and deps_qemu.zip are extracted before the files/folders are placed in the shared folder for the VM, whereas the other zip files are placed directly in the shared folder for the VM. MINOR UPDATE: When installing the dependencies - at the very beginning - as stated in the instructions, you may encounter the following error:
npm is only required for installing
esy online, but because the package already has
esy preinstalled,
npm and its dependencies are not required). Thus, the error message above can be ignored. [1] https://zenodo.org/record/7113223 |
| Type Of Technology | Software |
| Year Produced | 2023 |
| Impact | N/A. |
| URL | https://zenodo.org/record/7504674 |