Funding Our Partners

Formalisation of Device Interfaces

Aim

Formalise the software interfaces of peripheral devices in a way that correctly represents the hardware designs.

Problem

Device driver bugs are a major source of operating system exploits. Our earlier work (summarised in the diagram on the left) shows that the leading source of these bugs is inaccurate, misunderstood or outright incorrect specifications of device interfaces. Our ultimate goal is to eliminate driver bugs through driver verification, but such verification will only be as good as the device specification it uses.

Solution

We aims to address the specification issue by developing formal specifications of real-world devices from their Verilog implementation, and prove that the specification correctly describes the implementation, or, more precisely, that the implementation refines the specification. The aim is to produce specifications that can be used as a reference for writing drivers, as well as a formal model for verifying them.

Approach

Current Process

We develop our formal specification of devices on the theorem prover HOL4. The specifications are derived from the actual Verilog designs using a partially-automated, systematic process. This is done with an appropriate level of abstraction, using inductive datatypes such as lists.

To show that this specification faithfully represents the device implementation generated from the Verilog design, we use the existing HOL4 formalisation of Verilog (AST and semantics) by Andreas Lööw as the intermediate representations for step-wise validation of the behaviours of the specification: we first derive a direct HOL4 representation (shallow embedding) of the Verilog design via a (presently) partially-automated process, capturing the finite state machine (FSM) described by Verilog as HOL4 functions. We then apply Lööw's proof-producing translator to convert this HOL4 representation into an abstract syntax tree (AST, deep embedding).

Pretty-printing this will produce a new Verilog implementation of the device, which we prove to behave equivalently to the original Verilog via equivalence checking or refinement. It is also possible to use this Verilog instead of the original Verilog for generating the device logic.

We show the behavioural equivalence between the HOL4 decive specification and the HOL4 representation of Verilog using interactive theorem proving (ITP), specifically HOL4. The top-level HOL4 device specification is sufficiently abstract to be used for device verification.

Desired Process

The above process is feasible but labour-intensive. Our medium-term goal is to largely automate it, by (1) parsing Verilog directly into an abstract syntax tree (AST) in the theorem prover, and (2) using decompilation to abstract the AST into an FSM representation, as shown in the diagram on the left.

This will not only eliminate much of the manual work, it also obsoletes the detour via a verified Verilog export. The remaining manual task will be to verify the abstraction used for driver development and verification.

Status

We are trialling our approach on I²C and SPI controllers from the OpenTitan peripherals used in the PULP Project. Our plan is to then move on to a 1Gb/s Ethernet NIC controller.

Development

You can find our formal specifications here in one of Trustworthy Systems Group GitHub repositories. This currently contains specifications of I²C device and SPI device based on open source Verilog designs

Support

This project is supported by Cyberagentur as part of the PISTIs-V Project under the Ecosystem formally verifiable IT – Provable cybersecurity (EvIT) program.

Partners

This project is a collaboration with:

• Our colleague Hammond Pearce at UNSW Computer Science & Engineering
• Albert Rizaldi at PlanV.

Latest News

• 2025-09-08: Our workshop paper on formal specifications of I2C and SPI devices has been accepted by PLOS 2025.
• 2025-01-20: Cyberagentur launches the ÖViT program, which funds tis work through the PISTIs-V project.

Contact

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

People

Publications

Liam Murphy, Albert Rizaldi, Lesley Rossouw, Chen George, James Treloar, Hammond Pearce, Miki Tanaka and Gernot Heiser High-fidelity specification of real-world devices Workshop on Programming Languages and Operating Systems (PLOS), October, 2025