Formal proof of an integrated hardware garbage collector
Lead Research Organisation:
University of Bristol
Department Name: Computer Science
Abstract
The Integrated Hardware Garbage Collector is an innovative new design for hardware garbage collection which promises to significantly improve system security and reliability by replacing traditional MMUs. It achieves this by replacing the traditional flat address space memory model with a new object-based sparsely-connected memory model. This entirely prevents buffer overflow issues and similar classes of errors and vulnerabilities. In addition, it can offer real-time performance for high level languages such as Java, C# and Haskell. However, without strong guarantees of correctness the design cannot be trusted in general purpose applications. To provide these guarantees, this thesis formally proves the correctness of the IHGC design for both an abstract model and a Verilog implementation.
Organisations
People |
ORCID iD |
| David May (Primary Supervisor) | |
| Edward Nutting (Student) |
Studentship Projects
| Project Reference | Relationship | Related To | Start | End | Student Name |
|---|---|---|---|---|---|
| EP/N509619/1 | 01/10/2016 | 30/09/2021 | |||
| 1942419 | Studentship | EP/N509619/1 | 01/10/2017 | 30/04/2021 | Edward Nutting |
| Description | We have formalised our understanding of the computer hardware we've invented. We have also discovered new ways to apply mathematics to understanding whether computer hardware and software works properly. Critically this means we can prevent cyber attacks such as the Whatsapp hacks in 2019, the Apple iPhone web browser hacks of 2019, or the Intel Meltdown attack. This means we can better protect individuals being targeted through their mobile devices by organizations such as nation states. We can also better protect people from ransomware and other mass-cyrber-attacks. Our technology can be used in everything from Internet of Things devices to mobile phones and web servers. This is a critical problem: existing technologies cannot protect IoT devices and they frequently fail to protect larger devices like mobile phones and servers. Our techniques can be applied to a broad range of computer hardware and software, meaning electronic devices generally can be improved by using our techniques to discover mistakes and fix them. |
| Exploitation Route | At the time of writing, the spinout company BeyondRISC will be commercialising the technology. The techniques used to formally prove the correctness of the technology will be published and made available to industry for general use in verifying hardware and software systems. |
| Sectors | Aerospace, Defence and Marine,Digital/Communication/Information Technologies (including Software),Electronics,Security and Diplomacy |
| URL | https://www.beyondrisc.com |
| Title | Proof by refinement in Agda |
| Description | The method invented enables the creation of flexible, robust, incremental proofs by refinement of hardware in the dependently-typed programming language Agda. The method is applicable to other dependently typed languages and to any form of hardware. The method applies Hoare Logic to this new area and encodes Hoare Triples in an intuitive and executable form inside Agda. It enables the integration of specification, proof by refinement, proof by equivalence and compilation to hardware within a trustworthy, formal framework. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2020 |
| Provided To Others? | No |
| Impact | This will be published in future to make it generally available for research and industry use. |
| Title | Speccam: Hardware specification language |
| Description | The category selected seems to be the only one which makes sense - why am I seeing biological sciences categories for my project in computer science? Speccam is a new specification language based on a simplified Occam semantics, modern syntax and targeted at the key pain points of hardware specification. It is readily human and machine readable making specifications easy to write, read and process into multiple formats for publication, simulation, formal verification and hardware implementation. The language meets the requirements laid out by other research in the field of hardware specification and verification. In particular challenges identified by Cambridge researchers during their verification of the ARM6 instruction set architecture. |
| Type Of Material | Improvements to research infrastructure |
| Year Produced | 2019 |
| Provided To Others? | No |
| Impact | Speccam has been used to specify the integrated hardware garbage collector (IHGC) - the design at the heart of our research - providing a common specification for the researchers in our team to work from. For example, this ensures the specification, being verified by one team member, is the same as another is implementing in simulation. Speccam has also been used to specify the new instruction set architecture (ISA) we are working (that includes the IHGC). This allows fast implementation of simulators, including updating them when issues are found or new ideas attempted. This increases the speed with which we can research new design ideas, adapt to different research requirements and obtain accurate experimental results. |
| Title | BeyondRISC FPGA implementation |
| Description | An FPGA implementation of the core subset of the BeyondRISC ISA. |
| Type Of Technology | New/Improved Technique/Technology |
| Year Produced | 2019 |
| Impact | - |
| Title | BeyondRISC ISA |
| Description | A new instruction set architecture that takes advantage of the IHGC technology. |
| Type Of Technology | New/Improved Technique/Technology |
| Year Produced | 2019 |
| Impact | - |
| Title | Experimental C# compiler |
| Description | An experimental C# compiler that takes standalone, embedded applications written in C# and compiles them to the BeyondRISC ISA. Outputs have been tested in simulation and with real-world applications on our FPGA implementation of the BeyondRISC design. |
| Type Of Technology | Software |
| Year Produced | 2019 |
| Impact | - |
| Title | IHGC Proof in Agda |
| Description | A proof of correctness, liveness, safety and other properties of the IHGC design. The stop-the-world form of the design is complete. The concurrency proof and equivalence to the Speccam-based specification are ongoing work. |
| Type Of Technology | Software |
| Year Produced | 2020 |
| Impact | - |
| Title | Speccam parser |
| Description | A parser written using Megaparsec for parsing Speccam code and converting it into LaTeX, Agda, Go and Verilog. This is ongoing work - the parser is implemented but the conversions are still being implemented. |
| Type Of Technology | Software |
| Year Produced | 2020 |
| Impact | - |
| Title | Visual memory debugger |
| Description | A visual debugger for the BeyondRISC memory architecture enabling much more rapid debug cycles. |
| Type Of Technology | Software |
| Year Produced | 2019 |
| Impact | - |
| Company Name | BEYONDRISC LIMITED |
| Description | BeyondRISC aims to eliminate the most common mistakes in computing by building a new microprocessor, based upon the research and IP from Ed Nutting, Andres Amaya Garcia and Prof. David May. As part of this, we aim to improve software through better hardware design, targeting energy efficiency, performance and developer productivity. BeyondRISC's technology eliminates the biggest cause of security vulnerabilities worldwide: memory safety issues, including buffer overflows. Our new microprocessor will be the only one guaranteeing no memory safety vulnerabilities. Our technology also makes it the first and only processor to support modern programming languages in low-power, production-ready Edge and IoT devices. We also provide energy and performance improvements between 1.2x and 7x for applications written in both modern and old languages. |
| Year Established | 2019 |
| Impact | The company is in the process of raising seed investment. |
| Website | http://www.beyondrisc.com |