seL4 is a strict microkernel, meaning that all device drivers are user-level programs, as are network protocol stacks and file systems. The seL4 device driver framework (sDDF) is designed to simplify implementation of high-performance drivers for seL4. Pancake is a new programming language under development at TS aimed at easing verification of sDDF drivers.

The Pancake language itself is still under development. This project is to evaluate the current Pancake language by using it to implement drivers of various complexity and providing feedback to the language developers."


Computer Science and Engineering

Research Area

Operating systems | 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. Sample device drivers and other sDDF components written in Pancake. Desirable targets are Ethernet and SD-card drivers and sDDF modules such as a multiplexer.
  2. Report outlining the experience with Pancake, discussion of limitations and other shortcomings, and suggestions for improvement."
Scientia Professor and John Lions Chair Gernot Heiser
Scientia Professor and John Lions Chair
opens in a new window
Lecturer (EF) Johannes Aman Pohjola
opens in a new window