Trustworthy Systems (ERTOS)
News: C verification tool released under BSD license More...
The Trustworthy Systems project plans to change the game of software design and implementation, 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 NICTA's Software Systems Research Group and is mostly based at the Neville Roach Lab (NRL) at Kensington (Sydney). The project combines competencies in operating systems and formal methods. It is the successor of the first-phase ERTOS projects running 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.
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.
The Path to Trustworthy Software Systems
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 ERTOS research.
In line with NICTA's mandate of use-inspired basic research, the ERTOS team is strongly committed to outcomes which not only further the body of knowledge, but achieve real impact by being applicable in real life. The team has a strong track record of commercialisation of research, with the creation of the spinout company Open Kernel Labs (OK Labs). The company has already deployed ERTOS research outputs in hundreds of millions of devices, and there is an on-going process of collaboration and technology transfer between ERTOS and OK Labs. This process also feeds real-life requirements back into ERTOS, thereby ensuring that our research remains practically relevant. See collaboration and commercialisation for more.
The ERTOS team strongly believes in a tight integration of research and education, and consequently has a strategic education agenda, aimed at producing graduates with world-class knowledge and skills in operating systems and software systems design. These graduates power or own research, spread skills to Australian industry, and enhance NICTA's and UNSW's reputation when taking jobs overseas. Details can be found under education.
Past achievements of the ERTOS team include:
- world's first formal proof of functional correctness of a complete, general-purpose operating-system kernel;
- two papers accepted to SOSP'09. These are the first papers from Australia in the 42-year history of the top OS conference;
- machine-checked proof of security and isolation properties of the access control model of the capability-based operating system seL4;
- design and implementation of a high-performance capability-based secure microkernel (seL4) that integrates kernel and user resources in the same protection and management framework;
- the automatic generation of well-performing device drivers from formal specifications (Termite);
- a new approach to the design of device drivers which eliminates the majority of typical driver bugs by construction (Dingo);
- a comprehensive approach to accurate energy management via dynamic voltage and frequency scaling that does not rely on pre-characterisation or inaccurate models of the hardware (Koala);
- highest message-passing performance ever reported on a number of architectures.
Formal awards won by the ERTOS team:
- Best-Paper Award at SOSP'09 for seL4: Formal verification of an OS kernel
- September 2009: Gernot Heiser wins the Engineering, Mathematics and Computer Sciences Category of the NSW Scientist of the Year 2009 Award
- August 2008: ACSAC'08 Best Paper Award for Pre-virtualization: Soft layering for virtual machines
- May 2008: NICTA's Richard A Newton Impact Award for Research Excellence to Gernot Heiser for research leading to the creation of Open Kernel Labs
- November 2007: CISRA Award for best research paper to ERTOS PhD student Harvey Tuch
- April 2005: USENIX'05 Best Student-Paper Award for Itanium—a system implementor's tale
A few notable near misses: