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