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.
| 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 | 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 |
| Impact | N/A. |
| URL | https://zenodo.org/record/7504674 |