Galois is pleased to host the following tech talk. These talks are open to the interested public. Please join us!
title: Verifying seL4-based Systems
presenter: Simon Winwood
time: Tuesday, 01 February 2011, 10:30am
location:Galois Inc.421 SW 6th Ave. Suite 300, Portland, OR, USA(3rd floor of the Commonwealth building)
abstract:
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.
bio:
Simon Winwood is a researcher in NICTA’s Trustworthy Embedded Systems project, investigating system-level security properties . Simon completed his PhD in the PLS group at UNSW. He also worked as a research engineer on the L4.verified project at NICTA. He is interested in software verification, type systems, and programming languages in general.