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: http://connect.linaro.org/resource/sfo17/sfo17-417/ Presentation: https://www.slideshare.net/linaroorg/using-math-to-prevent-linux-in-your-car-from-killing-you-the-open-source-sel4-kernel-sfo17417 Video: https://www.youtube.com/watch?v=heSmrHzHcuM —————————————————

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


Keyword: ‘http://www.linaro.org’ ‘http://connect.linaro.org’ ————————————————— Follow us on Social Media https://www.facebook.com/LinaroOrg https://twitter.com/linaroorg https://www.youtube.com/user/linaroorg?sub_confirmation=1 https://www.linkedin.com/company/1026961

Event Date: 28 Sept 2017

Speakers: Gernot Heiser

Position: Chief Research Scientist at Data61