PI: Scott Owens, University of Kent
- CakeML is a functional programming language and an ecosystem of associated proofs and tools, including a formally verified compiler to various processor architectures.
- CakeML currently lacks support for verifying libraries that use unsafe features, for example, array accesses w/o bounds checks.
- The RustBelt project uses the Iris framework to reason about unsafe features of Mozilla’s Rust language.
- This exploratory project investigated the feasibility of using RustBelt’s Iris to verify CakeML programs: we established that it is not possible to use Iris as-is, and that it one must develop an Iris-like logic for CakeML.
CakeML is a dialect of the ML family of programming languages and was originally designed to play a central role in trustworthy software systems. The CakeML project is an ongoing collaboration between S. Owens (Kent, UK), M. Myreen (Chalmers, Sweden), and J. Pohjola and M. Norrish (Data61, Australia). The project’s main accomplishment is the first fully verified compiler for a practical, functional programming language.
The RustBelt project aims to put the safety of Mozilla’s Rust programming language on a firm semantic foundation. Rust’s standard libraries make widespread internal use of unsafe blocks, which enable them to opt out of the type system when necessary. The hope is that such unsafe code is properly encapsulated, preserving language-level safety guarantees from Rust’s type system. However, subtle significant bugs with such code have already been discovered by RustBelt.
This project explored the way in which fundamental mathematical insights from RustBelt could be incorporated into CakeML’s suite of verification tools, setting the foundation for follow-up projects with greater scope for more advanced unsafe features, such as C’s malloc and free, or passing CakeML data to C functions. Such features are important, as they bring end-to-end verification to performance-critical areas, such as uni-kernel operating systems, or distributed systems where even (non-end-to-end) verified systems are known to be buggy.
We have established, while Iris technology can, in principle, solve the problems observed in CakeML, we would need to re-design the logical foundations of Iris to accommodate the CakeML proof ecosystem. In particular, the HOL4 theorem prover of CakeML has foundational differences from RustBelt’s Coq theorem prover. This is the subject of our subsequent VeTSS project.
RELATED GRANTS. Dr Scott Owens, EPSRC Grant: “Trustworthy Refactoring”, 09/2016-03/2020, £728,766.
PUBLICATIONS. H. Férée, J. Å. Pohjola, R. Kumar, S. Owens, M. O. Myreen, and S. Ho “Program Verification in the Presence of I/O Semantics, verified library routines, and verified applications”, VSTTE 2018.
IMPACT. “At Rockwell Collins, we use CakeML in projects to build avionics components with formally proven behavioural guarantees: these components have to exhibit high performance. In some cases, this can be achieved by algorithmic transformations already justifiable in CakeML. Beyond that, a great deal more performance can be obtained by unsafe (formally verified) compilation steps, and we are eager to take advantage of such advances when they become available.”– Konrad Slind, Senior Industrial Logician, Rockwell Collins –
