Skip to main content

Trustworthy Components

Trustworthy Components

Trustworthy Components is one activity of the Trustworthy Systems project.

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

  • Latest news:

  • 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.

Contact

Ihor Kuz, ihor.kuz<at>nicta.com.au

People

Current

Past

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

Publications

Abstract PDF Matthew Fernandez, Peter Gammie, June Andronick, Gerwin Klein and Ihor Kuz
CAmkES glue code semantics
Technical Report, NICTA and UNSW, November, 2013
Abstract
Slides
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 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
Preprint
Abstract PDF Nicholas FitzRoy-Dale
A declarative approach to extensible interface compilation
International Workshop on Microkernels for Embedded Systems, Sydney, Australia, January, 2007
Served by Apache on Linux on seL4.
Served by Apache on Linux on seL4.