Trustworthy Systems

Trustworthy components

We have developed a trustworthy OS kernel, seL4. The next step is to develop trustworthy software components.

seL4 Stack

Research Activities



  • Andrew Boyton
  • Francois Pradel
  • Japheth Lim
  • Matthew Fernandez
  • Stephen Sherratt
  • Steve Xie


Abstract PDF Gernot Heiser, Gerwin Klein and June Andronick
seL4 in Australia: From research to real-world trustworthy systems
Communications of the ACM, Volume 63, Issue 4, pp. 72-75, April, 2020
Abstract PDF Gerwin Klein, June Andronick, Ihor Kuz, Toby Murray, Gernot Heiser and Matthew Fernandez
Formally verified software in the real world
Communications of the ACM, Volume 61, Issue 10, pp. 68-77, October, 2018
Abstract PDF Matthew Fernandez
Formal verification of a component platform
PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
PDF Matthew Fernandez, Ihor Kuz, Gerwin Klein and June Andronick
Towards a verified component platform
Workshop on Programming Languages and Operating Systems (PLOS), pp. 1–7, Farmington, PA, USA, November, 2013
Abstract PDF Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray
CAmkES formalisation of a component platform
Technical Report, NICTA and UNSW, November, 2013
Abstract PDF Matthew Fernandez, Ihor Kuz and Gerwin Klein
Formalisation of a component platform
Poster presented at Operating Systems Design and Implementation 2012, October, 2012
Abstract PDF Nicholas FitzRoy-Dale
Architecture optimisation
PhD Thesis, UNSW, Sydney, Australia, March, 2011
Abstract PDF Ihor Kuz, Gerwin Klein, Corey Lewis and Adam Christopher Walker
capDL: A language for describing capability-based systems
Asia-Pacific Workshop on Systems (APSys), pp. 31–35, New Delhi, India, August, 2010
Abstract PDF Gernot Heiser, Kevin Elphinstone, Ihor Kuz, Gerwin Klein and Stefan M. Petters
Towards trustworthy computing systems: Taking microkernels to the next level
ACM Operating Systems Review, Volume 41, Number 4, pp. 3–11, December, 2007
Abstract link Ihor Kuz, Yan Liu, Ian Gorton and Gernot Heiser
CAmkES: A component model for secure microkernel-based embedded systems
Journal of Systems and Software Special Edition on Component-Based Software Engineering of Trustworthy Embedded Systems, Volume 80, Number 5, pp. 687–699, May, 2007
Abstract PDF Nicholas FitzRoy-Dale
A declarative approach to extensible interface compilation
International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007