2026-03-25 – TS team members Lesley Rossouw, Julia Vassiliki, and Liam Murphy presented at Down Underflow 2026. Our team presented Sealing the hardware-software contract with LionsOS on Serengeti using time protection and device verification in this weekend of presentations and networking for the open silicon community. They talked about two weaknesses in the typical hardware-software contract and our approach to solving them.

Speculative execution attacks such as Spectre rely on their use of a covert timing channel to leak information through speculation's effect on microarchitectural state. Julia described our work on time protection, an extension of the hardware-software contract to systematically prevent timing channels.

Device drivers are a major source of operating system bugs, a large portion of which are caused by violations of the devices' hardware-software contracts. These contracts are often represented by unreliable datasheets, making it difficult to ensure correctness. Liam covered the device formalisation project, which strengthens this contract by replacing datasheets with formal specifications verified against the device's source code, enabling formal verification of device drivers and the prevention of driver bugs.

Lesley introduced LionsOS and Serengeti, our secure operating system and experimental SoC development platform. These are the host for all the custom hardware and software features used in this work.