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 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