Export or edit this event...

Galois Tech talk: Verifying seL4-based Systems

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



Presented by Simon Winwood.

In 2009 the NICTA L4.verified project completed the machine-checked correctness proof of the seL4 microkernel. The natural next step is then to use this verified kernel to construct verified systems.

In this talk I give an overview of the ongoing work into systems verification in the Trustworthy Embedded Systems project. In particular, I will focus on the use of access control results to reason about the properties of systems in the presence of large untrusted components, such as a Linux kernel.