Low-level systems programming such as device driver development is tedious and error-prone, and 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 deductive verification techniques such as Hoare Logic inapplicable: device drivers aren't meant to terminate (so what's the post-condition?), and the state of the driver are 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 semantics 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 interaction trees is needed.

 

The aim of this project is to develop just such a logic. It should be formulated, and ideally proven sound, in the HOL4 interactive theorem prover.

This work occurs in the context of the broader 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.

School

Computer Science and Engineering

Research Area

Programming languages | Formal methods

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.
Lecturer (EF) Johannes Aman Pohjola
opens in a new window