Trustworthy Systems

Our research areas

Trustworthy Systems features a unique combination of experts in operating systems, formal methods and programming language design. By working closely together, we have produced systems that are efficient and practical, while at the same time they are backed by rigorous theoretical guarantees.

Operating systems

Providing software systems with guaranteed levels of security, safety, reliability and efficiency.

Formal methods

Verifying large-scale systems with mathematical precision, from overall design to executable code.

Programming languages

Designing languages and toolchains to enable software that is correct by construction.

Our best papers

See all publications

Presentation Video
Qian Ge, Yuval Yarom, Tom Chothia and Gernot Heiser
Time protection: The missing OS abstraction
EuroSys Conference, Dresden, Germany, March, 2019
Best Paper Award
Abstract PDF Anna Lyons, Kent Mcleod, Hesham Almatary and Gernot Heiser
Scheduling-context capabilities: A principled, light-weight OS mechanism for managing time
EuroSys Conference, Porto, Portugal, April, 2018
Abstract PDF Gernot Heiser and Kevin Elphinstone
L4 microkernels: The lessons from 20 years of research and deployment
ACM Transactions on Computer Systems, Volume 34, Number 1, pp. 1:1-1:29, April, 2016
Abstract PDF Thomas Sewell, Chi Kam and Gernot Heiser
Complete, high-assurance determination of loop bounds and infeasible paths for WCET analysis
IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), Vienna, Austria, April, 2016
Outstanding Paper award
Abstract PDF Carroll Morgan, Mário Alvim, Konstantinos Chatzikokolakis, Annabelle McIver, Catuscia Palamidessi and Geoffrey Smith
Additive and multiplicative notions of leakage, and their capacities
Computer Security Foundations, pp. 308–322, Vienna, Austria, July, 2014
Winner of the 2015 NSA Best Scientific Cybersecurity Paper Award
Abstract PDF Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski and Gernot Heiser
Comprehensive formal verification of an OS microkernel
ACM Transactions on Computer Systems, Volume 32, Number 1, pp. 2:1-2:70, February, 2014
PDF Thomas Sewell, Magnus Myreen and Gerwin Klein
Translation validation for a verified OS kernel
ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 471–481, Seattle, Washington, USA, June, 2013
PDF Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao and Gerwin Klein
seL4: From general purpose to a proof of information flow enforcement
IEEE Symposium on Security and Privacy, pp. 415–429, San Francisco, CA, May, 2013
PDF Aaron Carroll and Gernot Heiser
An analysis of power consumption in a smartphone
USENIX Annual Technical Conference, pp. 271–284, Boston, MA, US, June, 2010
Presentation Video
Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch and Simon Winwood
seL4: Formal verification of an OS kernel
ACM Symposium on Operating Systems Principles, pp. 207–220, Big Sky, MT, USA, October, 2009
Best Paper Award
Hall of Fame Award
Abstract PDF Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur and Gernot Heiser
Automatic device driver synthesis with Termite
ACM Symposium on Operating Systems Principles, pp. 73–86, Big Sky, MT, US, October, 2009
Abstract PDF Dave Snowdon, Etienne Le Sueur, Stefan M. Petters and Gernot Heiser
Koala: A platform for OS-level power management
EuroSys Conference, pp. 289–302, Nuremberg, DE, April, 2009