Trustworthy Systems

Evaluating programming languages for verified LionsOS components

Authors

Zhewen Shen

    School of Computer Science and Engineering
    UNSW,
    Sydney 2052, Australia

Abstract

Achieving end-to-end verification of operating system components requires removing the compiler from the trusted computing base. Pancake is a systems programming language with a verified compiler, designed for low level code such as device drivers. This thesis evaluates Pancake's suitability for implementing components of LionsOS, a modular operating system built on the seL4 microkernel.

We port over 20 LionsOS components to Pancake, comprising over 5,500 lines of code, including device drivers, virtualisers, and the core runtime library. We document the engineering effort involved and measure performance against C compiled with Clang and the verified CompCert compiler. Through targeted optimisations, we bring Pancake components within 10 to 15 percent overhead of their C counterparts. We conclude that Pancake is a viable language for building verification ready LionsOS components.

BibTeX Entry

  @mastersthesis{Shen:bsc,
    address          = {Sydney, Australia},
    author           = {Zhewen Shen},
    keywords         = {LionsOS, Pancake, CompCert},
    month            = dec,
    paperUrl         = {https://trustworthy.systems/publications/theses_public/25/Shen%3Absc.pdf},
    school           = {School of Computer Science and Engineering},
    title            = {Evaluating Programming Languages for Verified {LionsOS} Components},
    type             = {{BSc(Hons)} Thesis},
    year             = {2025}
  }

Download