Computer Science and Engineering
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.
Weaving together a proof story that connects device drivers written in Pancake with devices and the seL4 device driver framework requires interfacing between interaction trees (the semantic domain of Pancake programs) and traditional labelled transition systems (that model devices). The aim of this project is to explore the theory and practice of how to make this connection. This may involve working on topics including but not limited to automata theory, concurrency theory, interactive theorem proving, and model checking; exploring the tradeoffs between different approaches is part of the project.
School
Research Area
Operating systems | Programming languages
- 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.
- Report outlining the approach taken, tradeoffs considered and work done.
- A case study of applying the approach to the verification of a simple serial driver.
