Find out how ICT can support biomedical and clinical researchFind out more. Managing complexity by developing new tools and processes. Managing Complexity

Trustworthy Embedded Systems (ERTOS)

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

News:  ERTOS commences 4-year trustworthy embedded systems project   More...
 		ERTOS_Header_Image

 

Summary

The Trustworthy Embedded Systems project plans to change the game of embedded 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 Embedded Systems project is an integral part of NICTA's Embedded Systems Theme and is mostly based at the Neville Roach Lab (NRL) at Kensington (Sydney). It is the main activity the ERTOS group at NRL, whose core competencies are in operating systems and formal methods. The Software Engineering group at the ATP Lab contributes know-how in software architecture, and and the Managing Complexity group at the Canberra lab contributes automatic analysis techniques.

The project 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 Embedded Systems project is based, and continue with expanded scope within the Trustworthy Embedded Systems Project.

Embedded Systems

Embedded systems are computer systems that form part of a larger system the primary purpose of which is not computation. These systems are ubiquitous and diverse, and include mobile phones, entertainment devices, automobiles, aeroplanes, toys, smart cards, medical devices, network switching equipment, sensors, industrial robots to name a few. Many embedded systems are real-time systems and have to react to external events within a defined period of time. Other constraints such as size, energy supply and unit price often severely limit the design space, affecting costs and reliability.

Challenges

Embedded 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 embedded 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 Embedded 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 Embedded 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 an embedded-systems design framework, design rules and techniques which together enable system designers to make guarantees about the security, safety and reliability of embedded 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 embedded-system software into interacting yet strongly-encapsulated components. The Trustworthy Embedded 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 embedded-software 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:

  • two papers accepted to the SOSP'09. These are the first papers from Australia in the 42-year history of the top OS conference;
  • machine-checked proof of isolation properties of a 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;
  • 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: