The Trustworthy Systems project plans to change the game of software design, implementation, verification and deployment, aiming for unprecedented security, safety, reliability and efficiency. This is to be achieved by advancing the theory and practice of systems design, combined with the application of cutting-edge formal methods.
The Trustworthy Systems project is a major activity of Data61's Software Computational Systems group. It is the successor of the first-phase ERTOS projects running in NICTA from 2004 to 2009, specifically the seL4, L4.verified and CAmkES projects. These sub-projects produced the core platform on which the Trustworthy Systems project is based, and continue with expanded scope within the Trustworthy Systems project. The project combines competencies in operating systems, formal methods and software engineering.
Software systems are growing in functionality, and consequently in complexity. This increases the likelihood of critical faults. At the same time, they are increasingly deployed in mission-critical or even life-critical scenarios, therefore such faults can have serious consequences. In devices deployed in national-security settings, used for financial transactions or for storing or accessing sensitive personal data, faults enable security compromises that lead to unauthorised disclosure of critical data. Faults in the embedded systems of aeroplanes, automobiles or medical devices present safety risks that can have fatal consequences. Faults in other devices undermine reliability and can lead to loss or revenue or reputation. Furthermore, the need for reliability, safety or security frequently leads to highly defensive designs that have a high cost in terms of performance or energy consumption.
The upshot is that software systems are increasingly trusted with critical operations. Yet, the traditional ways in which they are engineered provide limited or no assurance that they are worthy of such trust: In general, no guarantees can be made for the security, safety or reliability of such devices. The implications are scary: these systems are becoming more and more complex, and thus error prone. At the same time, more and more trust is put on them. This is a time bomb of silently growing destructive power.
NICTA believes that this situation is far too dangerous to tolerate, and that fundamental change is both necessary and possible. Such change is exactly what the Trustworthy Systems project is aiming to achieve. The project takes a strategic approach to trustworthiness, by combining and integrating innovation in operating systems, systems architecture and formal methods. The outcome will be a software-systems design framework, design rules and techniques which together enable system designers to make guarantees about the security, safety and reliability of software systems. These guarantees are based on the rigour of mathematical proof.
At the heart of this approach is microkernel technology. The operating-system kernel that is at the core of any software system runs in the privileged mode of the hardware. It therefore has complete and uninhibited control over everything in the system, and it is impossible to guard the rest of the system against faults in the kernel. By choosing a well-designed microkernel, seL4, we reduce the size of this most dangerous part of any system to a bare minimum, small enough to be able to provide mathematical proof of its correctness, and thus ultimate trustworthiness.
The microkernel provides the mechanisms for structuring the rest of the system software into interacting yet strongly-encapsulated components. The Trustworthy Systems project will develop frameworks and techniques for the design of such componentised systems. We will use formal methods to make guarantees about the behaviour of such a componentised system, focussing on safety and security guarantees. This includes formal proofs of isolation and security properties, and assurances about non-functional properties such as timeliness and energy consumption. For details see the project's activities.
The Trustworthy Systems team is strongly committed to outcomes which not only further the body of knowledge, but achieve real impact by being applicable in real life. We have a strong track record of commercialisation of research, with the creation of the spin-out company Open Kernel Labs (OK Labs). The company has already deployed Trustworthy Systems research outputs in hundreds of millions of devices.