| EPSRC Reference: |
EP/X021173/1 |
| Title: |
Transparent pointer safety: Rust to Lua to OS Components |
| Principal Investigator: |
Batty, Professor M |
| Other Investigators: |
|
| Researcher Co-Investigators: |
|
| Project Partners: |
|
| Department: |
Sch of Computing |
| Organisation: |
University of Kent |
| Scheme: |
Standard Research |
| Starts: |
01 May 2022 |
Ends: |
31 October 2024 |
Value (£): |
494,770
|
| EPSRC Research Topic Classifications: |
| Computer Sys. & Architecture |
Software Engineering |
|
| EPSRC Industrial Sector Classifications: |
|
| Related Grants: |
|
| Panel History: |
|
|
Summary on Grant Application Form |
The Digital Security by Design (DSbD) challenge builds a software ecosystem atop Morello, an ARM processor extended with capabilities. Capabilities combine a pointer to memory with permissions and bounds information that Morello processors use to enforce memory safety at run time, halting programs in error when safety is violated. This project develops a vertical stack in the DSbD ecosystem in three parts: a Rust compiler, an implementation of Lua in Rust, and integration of this Lua interpreter into FreeBSD, replacing a core component of the FreeBSD bootloader with software built in DSbD tech.
Rust maximises the guarantees provided by capabilities with a memory-saftey-first design, and Lua is a high-level language used for joining systems components together, with the details of memory management safely automated. We will support this vertical with a theoretical development. In our Lua interpreter, we anticipate allocation and reclamation requiring unsafe Rust code, and we will verify that these components cannot produce capability errors. We will raise this to memory safety of the whole interpreter by proving that safe Rust code should never exhibit capability errors.
Rust is a systems language from academia with substantial industrial use. Rust is proposed as the second language of the Linux kernel after C, with support from the creator of Linux. Rust excludes the vast majority of pointer misuse - ensuring memory safety - with a static (compile time) check, and a fall-back run-time check for complex cases. Our Rust compiler port will, as a consequence, port all safe Rust code to Morello, and typical Rust programmers may target Morello with no change to their working practices.
Sometimes a Rust programmer must subvert the type system, e.g. to interface with hardware or C OS components. These regions of code must be declared as unsafe, enabling a limited set of additional operations that the compiler cannot check, forgoing the automatic guarantees afforded to safe code. This segregation of unsafe code offers a model for programming capability hardware: Rust ensures safe code cannot exhibit capability errors, and unsafe code highlights regions where verification tools can be targeted.
Lua is a safe managed language that is used to set up the FreeBSD bootloader. We will port the Lua interpreter to Rust, integrate it into FreeBSD and establish that the garbage collector cannot capability fault.
We offer Rust, memory-safe Lua and OS components, together with a theoretical case study that demonstrates scalable security reasoning enabled by the new capability features.
|
|
Key Findings |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Potential use in non-academic contexts |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
|
Impacts |
|
| Description |
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk |
| Summary |
|
| Date Materialised |
|
|
|
|
Sectors submitted by the Researcher |
|
This information can now be found on Gateway to Research (GtR) http://gtr.rcuk.ac.uk
|
| Project URL: |
|
| Further Information: |
|
| Organisation Website: |
http://www.kent.ac.uk |