Verifying Efficient Libraries in CakeML

This project aims to explore the way in which fundamental mathematical insights from RustBelt could be incorporated into CakeML’s suite of verification tools. It will be a collaboration between Dr Scott Owens (University of Kent) and Dr Derek Dreyer (Max Planck Institute for Software Systems, Germany). Dr Owens is one of the leaders of the CakeML project and Dr Dreyer is the leader of the RustBelt project, funded by his ERC consolidator grant.

The CakeML compiler generates code with quality roughly comparable to other ML compilers, making this the ideal time to shift focus from compiler verification, to verifying programs that will use the compiler. The RustBelt project is starting to make significant theoretical breakthroughs, and transferring some of them to CakeML early will help inform future development on the pragmatics of using them in practical verification tools.

CakeML is a dialect of the ML family of programming languages, designed to play a central role in trustworthy software systems. The project is an active, ongoing collaboration between Dr Owens at Kent, Dr Myreen at Chalmers, Sweden, and Dr Kumar and Dr Norrish at the Data61 research lab in Australia. The project’s main accomplishment to date is the world’s first fully verified compiler for a practical, functional programming language.

RustBelt aims to put the safety of Mozilla’s Rust programming language on a firm semantic foundation. Rust uses an advanced ownership-based type system to rule out important classes of bugs, including data races and freeing in-use memory. Unfortunately, none of Rust’s safety claims have been formally investigated, and it is not at all clear that they hold. The key technique used by Rust’s type system is to prohibit the aliasing of mutable state, but this is too restrictive for implementing some low-level data structures. Consequently, 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 the language-level safety guarantees from Rust’s type system. However, subtle bugs with such code have been discovered before.

This project will help bring two existing high-visibility projects together and set the foundation for follow-up projects with greater scope for more advanced unsafe features, such as malloc and free to avoid GC overhead, or passing CakeML data to C functions via the foreign function interface. Such features will be important to 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.

Researchers: Scott Owens, University of Kent, UK and Derek Dreyer, Max Planck Institute for Software Systems, Germany.