The Trustworthy Systems (TS) group is working on verifying device drivers for LionsOS using the Pancake language. This work is inevitably dependent on a correct formalisation of the HW interface.
We have established a workflow to take an open-source hardware designs of device controllers (from the OpenTitan project, for example) and formalise its software interface in the theorem prover HOL4. We then validate the formalised model against the origial hardware design by showing the equivalence/refinement between them.
The project is to apply this workflow to produce more use cases, possibly by taking part in the on-going formalisation of devices such as I2C and SPI.
School
Computer Science and Engineering
Research Area
Formal verification | Hardware | Operating systems
Suitable for recognition of Work Integrated Learning (industrial training)?
Yes
- 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.
- Pull request to the Trustworthy Systems Group's github repository with formalization and proofs.
