Skip to main content

Verified Component-Based Development

Verified Component-Based Development

Verified Component-Based Development is one activity of the Trustworthy Systems group.

  • Aim: Develop a supporting framework for specifying component-based systems on seL4. This framework must be capable of generating the necessary glue code to instantiate the system. It should also guarantee that proofs of information flow properties on the system architecture hold on the code level at runtime.

    CAmkES architecture
  • Overview: While seL4 provides attractive safety and security properties to user-level applications, its API is low-level and little support is provided in the way of libraries. This can be sufficient for building simple applications, but larger systems require a significant amount of time to be devoted to developing supporting infrastructure. In embedded systems, these elements are often developed without reuse in mind, requiring the work to be repeated for future systems.

    Component-based development increases reusability and simplifies construction of user-level applications, but introduces dependencies on generated glue code and coincident assumptions about its correctness. The net effect is to increase the amount of code in the trusted computing base of the system. The correctness guarantees of the seL4 kernel can be undermined in a component system by an error or malicious code in the component framework. In order to use a component framework while retaining the guarantees provided by seL4, the code provided by the framework itself must be either implicitly trusted or proven correct. One of the aims of this project is to use formal verification techniques to provide such a correctness proof.

    A component framework with a proof of correctness enables not only the specification of more complex trustworthy systems, but also more tractable proofs of user-level code. By abstracting details such as component communication from the user-level design in this way, proofs of component systems can assume the correctness of underlying mechanisms.

    A requirement for the validity of reasoning about an abstraction of a component system is that the system at runtime corresponds to the architecture description of the system; that is, the system described is what is actually running. To guarantee this, we leverage the verification of system initialisation. The CAmkES platform produces a capDL bootable description of the system that can be used as input during system initialisation. There is ongoing work to prove this description corresponds to the high level architecture provided as input.

  • Technical research challenges:

    • Proving the functional correctness of CAmkES glue code.
    • Translating CAmkES architecture description language to capDL. A capDL description of a system facilitates reasoning about access control and authority. To maintain trustworthiness, this translation must be proved correct.
    • Maintaining or improving glue code performance. The existing CAmkES glue code has been optimised for use on a microkernel and any degradation of this performance may be unacceptable in an embedded environment.
    • Supporting correctness proofs of user-level component systems. One of the aims of the whole-system assurance activity is to prove properties of user-level code on seL4. For this to be possible, the component platform must provide suitable abstractions of its mechanisms for use in a proof context.





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 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
Served by Apache on Linux on seL4.