Funding

Verification of OS components

via Pancake-to-Viper transpilation

Aim

Repeatable, cost-effective verification of OS components using SMT-solvers.

Context

Pancake is a new programming language for imperative, space-constrained programming, designed from the ground up with ease of verification in mind. It has a verified compiler, which guarantees that the compiled code behaves the same as the source code. We are incrementally adding components written in Pancake to LionsOS.

We have a prototype transpiler that converts annotated Pancake code into Viper, an intermediate language for efficient SMT-based verification. We have used this framework to verify an ethernet driver written in Pancake and also are applying the same framework on more OS components.

We plan to verify the Pancake components as we add them to LionsOS, and we consider SMT-based verification via this transpiler more accessible in the general systems engineering context compared to the approach based on interactive theorem provers, even though we will be using both approaches as needed. We also aim to evolve the transpiler something more integrated into the Pancake ecosystem and remove it from the TCB.

Getting Started

You can find a draft version of the Pancake syntax reference here. You can also experiment with Pancake codes and annotations on our Pancake Playground.

Latest News

• 2025-01-20: Cyberagentur launches the ÖViT program, which funds Pancake through the PISTIs-V project.

Support

The Pancake work is financially supported by:

• Cyberagentur under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program funds the PISTIs-V Project of which our Pancake work is a part.

It was previously supported by National Cyber Security Centre and the Technology Innovation Institute.

Collaborations

The prototype transpiler is written by Alessandro Legnani as part of external collaboration.

Contact

• Miki Tanaka, miki.tanaka<at>unsw.edu.au

People

Publications