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: Presentation: Video: —————————————————

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

Keyword: ‘’ ‘’ ————————————————— Follow us on Social Media

Event Date: 28 Sept 2017

Speakers: Gernot Heiser

Position: Chief Research Scientist at Data61

Other Posts

Sign up. Receive Updates. Stay informed.

Sign up to our mailing list to receive updates on the latest Linaro Connect news!