In this talk, I will give an overview of the various current activities within NICTA’s Trustworthy Systems team. Building on our work on seL4, we aim at providing unprecedented security, safety, reliability and efficiency for software systems. seL4 is a real-world, general-purpose operating system, with a guarantee that its machine code is correct with respect to its specification, and that it enforces critical security properties such as information flow control, integrity and authority confinement.

Present activities focus on extending the safety and security properties of seL4, and extending the formal guarantees to user-level code, including automatic co-generation of code and proofs. For tightly constrained devices without memory protection, we are also working on verifying eChronos, a small real-time OS for embedded micro-controllers. Both seL4 and eChronos are used in a DARPA-funded project aiming at the demonstration of a complete high-assurance system and technology transfer to a real autonomous helicopter built by Boeing.