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.
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:
Past
|
|
 |
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 |
|
|
|
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 |