Trustworthy Systems archive

Trustworthy Systems project

Trustworthy Systems 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.

• Previous achievements/projects: seL4 kernel, L4.verified, CAmKES.

• Read more: About this project. Also see our list of Activities below, or look at our Publications, Project Plan 2009-2013.

SMACCM

• Many of our activities in the Trustworthy Systems area are part of the SMACCM project, funded by DARPA under their high-assurance cyber-military systems (HACMS) program.

Specific Activities

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, utilising a component-based software development platform (CAmkES), and 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.
• CakeML: verified compilation of functional programs, for end-to-end correctness of applications-level software.
• Cogent: design and implementation of provably correct file systems through code and proof co-generation.
• Information Flow: Reasoning about information flow and seL4.
• Timing channels: Quantitative assessment of time-based covert information flow in seL4-based systems, and development of kernel mechanisms for its mitigation.
• 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: ensuring temporal isolation properties of seL4, and providing support for mixed-criticality real-time systems, to enable the kernel's use in safety-critical systems.
• 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 and improvements of our existing kernel and correctness proofs.

• Proving Compiler Correctness: eliminating the compiler correctness assumption of the original seL4 functional correctness proof, using translation validation approach.
• seL4 Kernel: continuing to develop seL4 to make it the system of choice as a trustworthy foundation for complex software systems.
• Proof Method Language: enabling users to easily write automated reasoning procedures (proof methods) to write more robust, and maintainable proof scripts.

Publications and People

On the Trustworthy Systems publications and people pages.