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.

Publications

10 25 50

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 18/09/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