The challenge

Software failures and cyber attacks

As more features are included in software systems, the software becomes larger and more complex.

Complexity makes dependability more difficult and can lead to increased failure points. Failure or misbehaviour of software systems can then have significant consequences such as leakage of sensitive information and exposure to cyber-attacks.

For systems on critical devices, we must at the very least build software that we can depend on to perform safely and as expected.

Our response

Design and isolation for verification

For a system to be truly dependable, we must be able to guarantee that it behaves correctly and has the required security and safety properties. This guarantee can be achieved through testing, certification and formal verification.

Formal software verification, using machine-checked mathematical proof, provides the strongest guarantees of software properties. However, it is not feasible to formally verify all the code in a real system, particularly systems which are large and complex. This makes the design for verification crucial.

By reducing the trusted computing base (TCB) – the part of the system that can break security or safety if it misbehaves - we have a key strategy for verification design. In many systems, the TCB is large; but in well-designed systems it is minimal, and suitable for formal verification.

In response, our scientists developed the sel4 microkernel which provides the necessary minimal TCB and offers a reliable, secure, fast and verified foundation for building trustworthy systems.

The results

seL4 for dependable systems software

sel4 is the world's fastest operating kernel designed for security and safety.  It enforces security within componentised system architectures by ensuring isolation between trusted and untrusted system components, and by carefully controlling software access to hardware devices in the system.

Built on 15 years' experience with the L4 microkernel, sel4 is the only operating system that has undergone formal verification, proving bug-free implementation and enforcement of spatial isolation ensuring data confidentiality and integrity. It is also the first protected-mode operating system with a sound timeliness analysis.

SeL4 was released under open-source (GPL2) licence in mid-2014, and has since been deployed to support dependable systems in various real-world applications from autonomous vehicles to military intelligence and aerospace.  Proprietary licences are also available through General Dynamics .

seL4's predecessor, OKL4, created by the same team, has been deployed on billions of mobile and connected devices.

Find out more: The seL4 microkernel

Do business with us to help your organisation thrive

We partner with small and large companies, government and industry in Australia and around the world.

Contact us now to start doing business

Contact Data61

How can we help you create your data-driven future? Use the form below to send us a message.
Your contact details
0 / 100
0 / 1900
You shouldn't be able to see this field. Please try again and leave the field blank.

For security reasons attachments are not accepted.