http://ertos.nicta.com.au/research/sel4/Secure Microkernel Project (seL4)OverviewThe L4 microkernel provides a minimal and efficient basis for constructing operating system software for a broad range of systems from single-purpose embedded devices to multi-processor servers. This project aims to extend L4's applicability to application domains requiring strong security guarantees. Strong security is a fundamental requirement for some existing and emerging embedded application domains and devices, such as personal digital assistants, mobile phones, and set-top boxes. It is widely acknowledged that to build a secure system, security must be considered in all layers of the system — from hardware to software applications. It is also widely acknowledged that it is extremely difficult (if not impossible) to retrofit security mechanisms to an existing insecure system. Security is becoming a critical component of new embedded devices such as mobile phones, personal digital assistants, and set-top boxes. There is an expectation from users and service providers that such devices will store sensitive data owned by either party, i.e., data that either party wishes to control access to and dissemination of. Such devices are also expected to run third-party applications whose origin, quality and functionality is not directly or even indirectly controlled by the embedded-device supplier. Given that end-users are unlikely to be able or willing to identify applications of dubious nature (or outright malicious intent), any secure embedded system must be capable of enforcing security requirements between application instances on an individual device, in an environment where hostile applications are unknowingly installed by end users. The susceptibility to viruses, trojan horses, ad-ware, and spyware of modern desktop platforms is largely due to the inability of the underlying base system to apply and enforce the principle of least authority, which undermines the ability of higher-level layers to provide security. The inability of users to finely control their own software results in uncontrolled propagation of viruses, the disclosure or modification of private data, or denial of service to the user. Attempts to secure platforms via various scanners, fire walls, and integrity checkers have been of only limited success, and largely unsatisfactory if one requires strong guarantees regarding control of their data. seL4's goal is to provide the secure software base upon which further secure software layers (system and application services) can be composed to form a trustworthy embedded system. To provide a high degree of assurance to the guarantees we expect to provide with seL4, we have a strong collaboration with the NICTA Formal Methods and Logic and Computation programs in the form of the L4.verified project. A high degree of assurance can ultimately only be established by mathematical rigour, and thus the collaboration aims to formally model the kernel's programming interface, and formally verify the implementation of the modeled interface. Ultimately, strong security guarantees will be assured by mathematical proof. Further technical details of the project are available here. A document describing the seL4 Kernel API is here. PeopleCurrentPastPublications |
