Device driver bugs are one of the leading sources of cybersecurity vulnerabilities in operating systems. Formal verification of device drivers can address this issue, but traditional device drivers have at least two features that make traditional techniques like Hoare Logic inapplicable: they aren't meant to terminate (so what's the post-condition?), and the state of the driver is less interesting than its interaction with the device and O/S (so what use would a post-condition be anyway?).
Interaction trees is a recent denotational model that addresses both of these concerns, by representing the semantics of a program as an infinite tree, whose nodes are I/O events and whose branches represent possible responses by the environment. To make reasoning about interaction trees scalable, a Hoare-like logic that can prove branching-time properties about them is needed.
This project is to develop just such a logic. It should be formulated, and ideally proven sound, in the HOL4 interactive theorem prover.
School
Research Area
Programming languages | Formal methods
- Research Environment
- Expected Outcomes
- Reference Material/Links
- Our team
This work occurs in the context of the broaded Pancake project. 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.
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) Pull request against the CakeML repository with definitions and proofs.
2) Report outlining the work undertaken.