You are here

Event Details

MP Associates, Inc.
WEDNESDAY October 18, 8:30am - 9:30am | Crystal
Trustworthy Operating Systems for Critical Embedded and Cyberphysical Systems
Gernot Heiser - Univ. of New South Wales
With the spread of cyberphysical systems and the IoT, trustworthiness of these devices, i.e. security, safety and dependability, is becoming increasingly important. Trustworthiness of non-trivial systems is critically dependent on the operating system (OS) enforcing isolation between components. However, traditional OS technology fails spectacularly to provide such isolation, resulting in the deluge of cyber-attacks we are experiencing. Such attacks are becoming a serious threat to economic stability and the functioning of society.

This talk will discuss the technical requirements for OSes for safety- and security-critical systems. It will present the seL4 microkernel as the system that goes furthest in supporting these requirements. Specifically, seL4 has formal, machine-checked proofs of implementation correctness from a high-level functional specification to machine code, and proofs that the kernel is able to enforce spatial isolation, including provable absence of covert storage channels. The kernel supports temporal integrity enforcement designed to support mixed-criticality real-time systems, an important feature for emerging cyber-physical systems with co-located functionalities (verification of these features is in progress). Integration with AADL-based model-driven development tools support seL4’s use in real-world systems. The talk will also discuss on-going work on ensuring temporal confidentiality, i.e. prevention of covert timing channels.

Biography: Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW Sydney and Chief Research Scientist at Data61, CSIRO. He has a 20-year track record of building high-performance operating-system microkernels as a minimal basis for trustworthy systems. He is the founder and past leader of Data61’s Trustworthy Systems group, which pioneered large-scale formal verification of systems code, specifically the design, implementation and verification of the seL4 microkernel. His former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and more recently ships on the secure enclave processor of all iOS devices. Heiser is a Fellow of the ACM, the IEEE and the Australian Academy of Technology and Engineering (ATSE).