Embedded Files
Intelligent Vehicle Security and Safety Needs a Verified Operating System
Intelligent Vehicle Security and Safety Needs a Verified Operating System
Gernot Heiser, UNSW Sydney, Australia
Gernot Heiser, UNSW Sydney, Australia
Modern vehicles, even those under nominal control of a driver or pilot, are controlled by computer systems that process human input besides a multitude of sensor inputs. As such, they cannot be safe if these computer systems can be compromised by an attacker. And preventing such attacks is a core duty of the operating system (OS).
In reality, almost all operating systems can be compromised and are therefore unable to ensure the safety of a system, even if all other critical components operate correctly. One of the rare exceptions is the seL4 microkernel, the world’s first OS kernel with a machine-checked proof of implementation correctness. seL4 is still the most thoroughly assured OS kernel, including proofs of security- and safety enforcement across multiple processor architectures. Its use has been demonstrated on autonomous vehicles in the defence space and it is being adopted by car manufacturers.
seL4 itself is not an OS, but a microkernel that essentially guarantees isolation with controlled communication. To date, most deployments use seL4 as a hypervisor, leading to course-grained system structures, still dependent on significant amounts of unverified code. At UNSW’s Trustworthy Systems group we are working on changing this, by developing a highly modular, yet high-performance seL4-based OS that can be verified with automatic proof techniques. In this talk I will give an overview of seL4 and its verification story, and then discuss the approach we are taking in developing and verifying this new OS.
Gernot Heiser is Scientia (distinguished) Professor and John Lions Chair of Operating Systems at UNSW Sydney. His research interest are in operating systems, real-time systems, security and safety. His research vision is to completely change the cybersecurity game from playing catch-up with attackers to systems that are provably secure. As leader of the Trustworthy Systems group, he pioneered large-scale formal verification of systems code, specifically the design, implementation and formal verification of the seL4 microkernel; seL4 is now being used in real-world security- and safety-critical systems.
Heiser's former company Open Kernel Labs, acquired by General Dynamics in 2012, marketed the OKL4 microkernel, which shipped on billions of mobile wireless chips and is deployed on the secure enclave of all iOS devices. He presently serves as Chief Scientist of Neutrality and Chairman of the seL4 Foundation. Gernot is a Fellow of the ACM, the IEEE, the Australian Academy of Technology and Engineering (ATSE) and the Royal Society of New South Wales (RSN) and a Member of the German Academy of Sciences Leopoldina. He is also an ACM Distinguished Lecturer and an IEEE Distinguished Visitor.
Google Sites
Report abuse