The Open-Source seL4 Kernel. Military-Grade Security Through Mathematics – SFO17-417

Session ID: SFO17-417
Session Name: Using math to prevent Linux in your car from killing you: The Open Source SEL4 kernel. – SFO17-417
Speaker: Gernot Heiser
Track: LITE

★ Session Summary ★
A run-time bug in operating system software that enables car control can
result in loss of life or limb. Safety assessors require evidence that such
software is provably free from any bugs. These proofs are inevitably a
combination of software development best practices and a lot of test coverage.
But can we be sure that it is enough ? Really really sure ? What if we used
maths to absolutely guarantee that there are zero bugs in the operating system
core ? This session presents seL4 – a military grade open source project that
uses machine checked formal verification to prove that the C language
implementation of the seL4 kernel and it’s resulting binaries are free from
bugs. This then permits running Linux safely in virtual machines on top of
seL4 – something that the Auto world demands.
★ Resources ★
Event Page:

★ Event Details ★
Linaro Connect San Francisco 2017 (SFO17)
25-29 September 2017
Hyatt Regency San Francisco Airport

Follow us on Social Media

Event Date: 28 Sept 2017

Speakers: Gernot Heiser

Position: Chief Research Scientist at Data61