Trustworthy components

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

• Aim: Component-based development of systems, resulting in verified code that is used for the overall system proof.

• Latest news:

  • CAmkES has been released as open source (BSD license).
  • We have developed a CAmkES-based Smart Elecrticity Meter.
  • Matthew Fernandez presented Towards a verified component platform at the PLOS 2013 workshop.
  • CAmkES is being used for the development of software for the QB50 satellite project.

• Overview: Given the software architecture of a system we can implement it as a component-based system and use the componentised structure to aid in verifying the whole system.

  The first thing we need for this is a component platform. This platform takes as input an architecture description, together with detailed communication interface descriptions, component behaviour specifications and component implementations, and generates a full system description together with all glue code that implements the connectors between the components. Along with a user-level system initialiser and the kernel these combine to form the full executable system.

  In order to make the system verifiable we must be able to:

  • Verify system initialisation (separation setup in the diagram) — proving that it sets up the user-level system as specified, including isolation and capability distribution;
  • Verify connector code (green connector in the diagram) — proving that it is implemented as specified, in particular for trusted components;
  • Verify trusted component code (green component in the diagram) — proving that it implements the behaviour that is expected and defined in the security architecture.

Research Activities

• Component Platform: we continue to develop and extend the CAmkES component platform. Our main activities are optimising performance and supporting requirements of systems being developed on CAmkES.
• Verified Glue Code: we have formalised the CAmkES component model in Isabelle/HOL. We are currently defining a formal semantics for the inter-component communication in CAmkES so that we can later prove correctness of generated glue code.
• Verified System Initialisation: we have defined a language (called capDL) for describing the capability distribution of a seL4 system. We must show, on the one hand, that the generated capDL description represents the desired software architecture and, on the other hand, that the system initialisation produces a system state that reflects a capDL description.
• Trustworthy Component Code: synthesising component code reduces reliance on manually produced code, and improves the reliability and trustworthiness of the resulting code (correct by construction). Current work is focused on filesystem synthesis. Future work will also investigate applying formal methods to verify that a component's implementation (synthesised or manual) corresponds to its specification.

People

Publications

		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
		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
		Matthew Fernandez Formal verification of a component platform PhD Thesis, School of Computer Science and Engineering, UNSW, Sydney, Australia, Sydney, Australia, July, 2016
		Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz CAmkES glue code semantics Technical Report, NICTA and UNSW, November, 2013
		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
		Matthew Fernandez, Gerwin Klein, Ihor Kuz and Toby Murray CAmkES formalisation of a component platform Technical Report, NICTA and UNSW, November, 2013
		Matthew Fernandez, Ihor Kuz and Gerwin Klein Formalisation of a component platform Poster presented at Operating Systems Design and Implementation 2012, October, 2012
		Nicholas FitzRoy-Dale Architecture optimisation PhD Thesis, UNSW, Sydney, Australia, March, 2011
		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
		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
		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 Preprint
		Nicholas FitzRoy-Dale A declarative approach to extensible interface compilation International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007