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:
Errors were encountered while processing: libnode-dev node-gyp npm
Please note that this does not affect the artefact evaluation at all ( 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