Low-level systems programming such as device driver development is tedious and error-prone, and device driver bugs are one of the leading sources of cybersecurity vulnerabilities in operating systems. Pancake is a research programming language currently under development at Chalmers University of Technology, ANU, and UNSW. It comes with a formally verified compiler and is built from the ground up for predictable compilation, ease of verification and the right expressive power for low-level systems programming.

Pancake is designed to avoid some of the pitfalls involved in C, the de-facto standard systems programming language, that make systems code hard to verify. For example, expressions are free of side-effects, programs are single-threaded, and memory is flat and statically allocated. The semantics of a memory access outside this statically allocated region is to fail; however, this is not enforced at runtime because the performance overhead of bounds checks is undesirable.

Ideally, full formal verification of a Pancake program will address memory safety anyway, because a memory-unsafe program cannot be shown to not fail. Even more ideally, the proof engineer should not be burdened with this task. prover.

The aim of this project is to prototype a way of automating proofs of memory safety for Pancake programs. This can be done in different ways: for example, by developing a type system that implies memory safety, or by developing tactics and algoritms for proof automation. Assessing these tradeoffs is part of the project. Any output should be formulated, and ideally proven sound, in the HOL4 interactive theorem prover.


Computer Science and Engineering

Research Area

Formal methods | Programming languages

The Trustworthy Systems (TS) Group is the pioneer in formal (mathematical) correctness and security proofs of computer systems software. Its formally verified seL4 microkernel, now backed by the seL4 Foundation, is deployed in real-world systems ranging from defence systems via medical devices, autonomous cars to critical infrastructure. The group's vision is to make verified software the standard for security- and safety-critical systems. Core to this a focus on performance as well as making software verification more scalable and less expensive.

  1. Pull request against the CakeML repository with definitions and proofs.
  2. Report outlining the work undertaken.
Lecturer (EF) Johannes Aman Pohjola
opens in a new window