Export or edit this event...

Galois Tech Talk: The L4.verified Project

Galois, Inc
421 SW 6th Ave. Suite 300
Portland, OR 97204, US (map)



The L4.verified Project Presented by Dr. Gerwin Klein.

Last year, the NICTA L4.verifed project produced a formal machine-checked Isabelle/HOL proof that the C code of the seL4 OS microkernel correctly implements its abstract implementation. This talk will give an overview of the proof together with its main implications and assumptions, and will show in which kinds of systems this formally verified kernel can be used for gaining assurance on overall system security.