Invited talks

June Andronick, NICTA

The L4.verified Project and Its Next Steps

Last year, the NICTA L4.verifed project produced the world's first formally proven correct general-purpose microkernel. The next big step in the challenge of building truly trustworthy systems is to provide a framework to develop secure systems on top of seL4. In this talk, we will give an overview of seL4's correctness proof, together with its main implications and assumptions, as well as our approach to provide formal security guarantees for large, complex systems. This involves a formal model of the access control enforced by seL4, and will be illustrated by an example system for which information flow properties have been proved.

Kim G. Larsen, Aalborg University

Timing Analysis of Embedded Software Systems

Embedded software is often applied in safety-criticial systems, e.g. the braking system of a car or the steering gear of an airplane. Many of these safety-critical systems are also time-critical, meaning that the calculations performed by the tasks of the embedded system need not only be functionally correct but must be carried out in a timely fashion. In this talk we show how real-time model checking using the verification tool UPPAAL (www.uppaal.com) may be used to give such timing guarantees.

Francesco Logozzo, Microsoft Research

Clousot: Language agnostic static contract checking via abstract interpretation

Code Contracts provide a language-agnostic way to express coding assumptions in .NET programs. CodeContracts take the form of preconditions, postconditions, and object invariants expressed as library calls. In the talk, I will introduce and demo CodeContracts, the runtime checker, and I will describe the static checker (Clousot), and the rationale behind its design. The CodeContracts API is part of .NET 4.0. The tools can be downloaded here.

FoVeOOS 2010 acknowledges kind support from Microsoft Research.