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.

Presented by Matthew Fernandez.

In safety- and security-critical environments software failures that are acceptable in other contexts may have expensive or even life-threatening consequences. Formal verification has the potential to provide high assurance for this software, but is regarded as being prohibitively expensive. Although significant advances have been made in this area, verification of larger systems still remains impractical. Component-based development has the potential to lower the cost of system-wide verification, bringing correctness proofs of these large scale systems within reach. This talk will discuss my work that aims to provide a component-based development environment for building systems with high assurance requirements. By providing a formal model of the platform with proven correctness properties that hold at the level of an abstract model right down to the implementation, I hope to reduce the cost of full system verification by allowing reasoning about system components in isolation.