The verified seL4 microkernel is implemented mostly in C (with a small amount of assembler code). Pancake is a new systems language developed by an international collaboration centered at Trustworthy Systems. Pancake's unique advantage is that it has a verified compiler that guarantees correct code generation, while having a much simpler (and thus more verification-friendly) semantics than C. It is mature enough to allow implementing much of LionsOS without a need for foreign function calls (FFIs) while performing close to C.
This opens up an exciting possibility: Would it be possible to re-implement seL4 in Pancake, and potentially reducing the cost of maintaining seL4's proofs (to which the complexities of the C semantics are a major contributor)?
This project is to evaluate the use of Pancake for implementing seL4. It does not require a formal-verification background, but deep experience in low-level programming in general and strong familiarity with kernel code in particular, as covered in COMP9242.
School
Computer Science and Engineering
Research Area
Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- Research environment
- Expected outcomes
- Supervisory team
- Reference material/links
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.
- Prototype implementation of critical parts of the seL4 kernel, at least the IPC, Notification and interrupt fastpath, with missing functionality provided by C code (invoked via FFI).
- Evaluation of fastpath performance compared to the original C version.
- Report describing experience and performance.
