Trustworthy Systems archive
This is an archive of our project website, dating back
to the Software Systems Research Group in
National ICT Australia (NICTA).
Visit our home page or projects list
to see all of our current projects and activities.
Trustworthy Systems project
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
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.
Read more: About this project.
Also see our list of Activities below,
or look at our Publications,
Project Plan 2009-2013.
- 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.
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
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
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
- eChronos: a highly configurable
high-assurance real-time OS for
resource-constrained micro-controllers without memory
- Real Time: ensuring
temporal isolation properties of seL4, and providing support for
mixed-criticality real-time systems, to enable the kernel's use in
- Analysis of Protocols for
High-Assurance Networks: providing authentication and
reliable communication protocols for unmanned aerial
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
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
- Proof Method Language:
enabling users to easily write automated reasoning
procedures (proof methods) to write more robust, and maintainable
Publications and People
On the Trustworthy Systems publications