Trustworthy Systems Research @ SSRG
Trustworthy Systems is one of the main research activities of the Software System Research Group (SSRG). It represents the confluence of formal methods and operating systems, applying the former in the context of the latter, and advancing the state of the art in both areas.
Aim: Unprecedented security, safety, reliability and efficiency for software systems, and especially critical cyber-physical systems.
Approach : large, complex, performant systems, built on a formally verified microkernel (seL4), which isolates untrusted components from formally verified or correct-by-construction synthesised trusted components. Formal, machine-checked proof for safety and security properties on the code level for systems with over a million lines of code.
Case Study: Secure Access Controller, a demonstrator system enabling to switch one front-end terminal between different back-end networks of separate classification levels, for which we formally proved, at a security model level, the absence of data flow between networks.
- Many of our activities in the Trustworthy Systems area are part of the SMACCM project in DARPA's high-assurance cyber-military systems program (HACMS).
We tackle the challenge of building truly trustworthy software systems with a number of inter-related activities. Our first focus is security and how to design systems with formally proved security properties on the source code level.
- Security Architecture: the first step is modelling and analysing architectures of secure systems, resulting in a desired design, identifying trusted and untrusted components, together with a formal proof of security on the architecture level, assuming correct behaviour of trusted components.
- Trustworthy Components: developing component-based systems, resulting in formally verified code for the trusted components, including the system initialisation components, guaranteeing that the system is set-up as required by the architecture.
- Automatic Device Driver Synthesis: generating drivers automatically from formal specifications, resulting in correct-by-construction device drivers and reducing the effort involved in development and testing.
- Automatic Specification Abstraction: simplifying reasoning about concrete C code, resulting reduced time and cost required for verifying software implementations.
- Trustworthy File Systems: design and implementation of provably correct file systems.
- Information Flow: formally proving that seL4 enforces information flow control, guaranteeing isolation between trusted and untrusted components.
- Whole-System Assurance: formally proving security properties down to the source code level of systems comprising of millions of lines of code; this combines the proof of security at the architecture level, the proof of the trusted components and the proof of isolation of seL4.
We are also investigating safety-critical applications with the following activities.
- eChronos: a highly configurable high-assurance real-time OS for resource-constrained micro-controllers without memory protection.
- Real Time: providing sound upper bounds on interrupt latencies for seL4, making it usable in safety-critical systems.
- Safety-Critical Systems: using seL4 as a basis in safety-critical systems such as AUTOSAR and evaluating the safety properties resulting from using a verified kernel.
- Analysis of Protocols for High-Assurance Networks: providing authentication and reliable communication protocols for unmanned aerial vehicles (UAVs).
In order for our technology to be deployed realistically, we are working on making the verification methodology more efficient, predictable and repeatable, with the following activities.
- Proof Measurement and Estimation: providing metrics and estimation methods for large-scale system formal verification projects, resulting in reliable plans for verification projects.
- Automated Reasoning: better and faster general automated and interactive provers for software verification.
Finally, the following activities address the maintenance phase of formally verified software systems and improvements of our existing kernel and correctness proofs.
- Improving the seL4 Correctness Proof: addressing some of the assumptions of the proof and further validating the specification (formally and non-formally).
- seL4 Kernel: continuing to develop seL4 to make it the system of choice as a trustworthy foundation for complex software systems.
Some of the lessons learned from the past 20 years of L4 microkernels are summarised in this paper.
- seL4 Proof Maintenance: keeping seL4 and its proof of correctness up-to-date following kernel improvements and new features, focusing on increasing automation and resulting in a maintained large-scale verified system.
ContactGerwin Klein, gerwin.klein <at> nicta.com.au (formal methods)
Gernot Heiser, gernot <at> nicta.com.au (operating systems)