Secure Embedded L4

The Secure Embedded L4 microkernel aims to provide a secure software base as the foundation for a trustworthy embedded system. Strong security is a fundamental requirement for embedded devices such as handheld computers, mobile phones and set-top boxes.

The Secure Embedded L4 project aims to improve the way that small portable devices such as mobile phones carry out specific tasks in a way that does not compromise other functions.

Modern software platforms are susceptible to viruses, trojan horses, adware and spyware largely due to their inability to apply and enforce the principle of least authority. Because users cannot finely control their own software, they risk propagation of viruses, disclosure or modification of private data or denial of service. The use of scanners, firewalls and integrity checkers has proved to be of limited success and cannot provide strong guarantees over the control of data.

This project will make more robust many of the capabilities that manufacturers of such devices want to offer their customers. The problem it will solve is that sometimes we want to run untrustworthy applications or that some people may trust the application and others do not. It will answer the question: how do we run untrustworthy or insecure software programs on a device and ensure they don’t compromise the rest of the system?

See also:

What will this research achieve?

Embedded devices such as mobile phones and set-top boxes are likely to contain sensitive data that users or service providers want to control access to and dissemination of. A secure embedded system must be capable of enforcing security requirements between applications, in an environment where hostile applications can unknowingly be installed by end users.

Secure Embedded L4 reduces the risks of running applications that are untrustworthy. Untrustworthy applications may contain unwanted code such as computer viruses or Trojan horses. Reducing the risk of running applications will reduce the costs of providing and using these functions and the potential damage.

Who will benefit?

The end users are manufacturers of embedded devices and ultimately the customers who use them. For now our research is targeted at those manufacturers of the devices and microchips.

What are the key features?

For many embedded devices, the microkernel provides the same functions as a computer’s operating system. We are building a microkernel called L4, which is a highly efficient and effective way to control an embedded device. The Secure Embedded L4 project allows us to isolate operating system functions so even if some part of it goes down, it does not mean the whole system fails. We focus on separating the functions to ensure they remain immune from each other’s troubles.

The Secure Embedded L4 microkernel works on the principle of giving someone one key to the drawer you want them to access rather than handing your entire keychain to someone you don’t know or trust. It gives untrustworthy visitors access only to the parts of the system they need and makes sure they only do what you want or expect them to do.

Progress update

Research team

Publications

Progress

  • We now have a prototype and a mathematical model to prove that our secure embedded L4 microkernel works.
  • Our challenge is to provide even more of the functionalities of large operating systems, building on the secure fundamentals of the microkernel.
  • In five years, we aim for our technology to be the de facto industry standard in the mobile phone world.
  • We expect that this technology will be licensed to NICTA startup OKL, which already has prospective customers ready to use Secure Embedded L4 applications proven by L4.verified.

Research team

Philip Derrin

Research Engineer

Philip Derrin is a research engineer working on the seL4 project, which aims to develop a specification for a new secure microkernel as a successor to L4. His research interests include the construction of secure systems and rapid prototyping and formalisation of microkernels in functional languages.

Dhammika Elkaduwe

PhD Student

Dhammika Elkaduwe is a student in NICTA's Embedded, Real-Time and Operating Systems program. He is interested in the development of secure embedded kernels.

Kevin Elphinstone

Project Leader

Kevin Elphinstone’s main research interest lies in the area of operating systems, specifically small operating system kernels and the infrastructure required to support larger systems upon them. His current focus includes user-level device drivers, and the construction of small, secure operating systems to form the basis of future embedded devices.

Publications

Philip Derrin, Kevin Elphinstone, Gerwin Klein, David Cock and Manuel M. T. Chakravarty

Running the manual: an approach to high-assurance microkernel development

Proceedings of the ACM SIGPLAN Haskell Workshop, Portland, Oregon, USA, September 2006

Kevin Elphinstone, Gerwin Klein and Rafal Kolanski

Formalising a high-performance microkernel

Workshop on Verified Software: Theories, Tools, and Experiments (VSTTE 06), Seattle, USA, August 2006

Dhammika Elkaduwe, Philip Derrin and Kevin Elphinstone

Kernel data – first class citizens of the system

Proceedings of the 2nd International Workshop on Object Systems and Software Architectures , Victor Harbor, South Australia, Australia, January 2006

Kevin Elphinstone

Future directions in the evolution of the L4 microkernel

Proceedings of the NICTA workshop on OS verification 2004, Technical Report 0401005T-1, Sydney, Australia, October 2004