Subscribe: Contact: Sitemap: Printer Friendly
Subscribe to our RSS feed
Home >  Research >  Software Systems >  ERTOS
ERTOS group photo

Trustworthy Systems (ERTOS)

The Trustworthy Systems project develops game-changing techniques and frameworks for the design of truly secure, safe and reliable software systems. The outcomes will be suitable for practical use and create significant real-world impact.

News:  C verification tool released under BSD license   More...

Summary

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.

Challenges

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.

Practical Use

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.

Education

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.

Achievements

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:

A few notable near misses: