seL4 is a microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. Low-level systems programming such as device driver development is tedious and error-prone.

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 and ease of verification.

The Pancake runtime expects to be the main function of a binary. But when writing drivers in the seL4 device driver framework, the need arises to use Pancake as a library, where other programs can call specific entry points and then gain back control. This project is to invent and implement an approach to supporting such entry points in a principled, low-cost and verifiable way. As a stretch goal, this work would be fully integrated into the Pancake compiler stack and verified.

School

Computer Science and Engineering

Research Area

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. Report outlining the approach taken, tradeoffs considered and work done.
  2. Pull request to the CakeML/Pancake github repository with an implementation and HOL4 formalisation.
Lecturer (EF) Johannes Aman Pohjola
opens in a new window
Senior Proof Engineer Miki Tanaka
Senior Proof Engineer
opens in a new window
Scientia Professor and John Lions Chair Gernot Heiser
Scientia Professor and John Lions Chair
opens in a new window