Large 00012

Can We Make Trusted Systems Trustworthy? - Part 1

Prof. Gernot Heiser (University of New South Wales, Australia)

Recorded 20 September 2012 in Lausanne, Vaud, Switzerland

Event: ntass 2012 - Nano-Tera/Artist Summer School 2012


The complexity of computer hardware and software continues to increase, while at the same time we are increasingly dependent on them functioning correctly – a recipe for disaster. Clearly, a change of approach is needed.

This lecture covers NICTA's approach, which is about constructing systems so that their dependability can be assured. Fundamentally we have to structure systems in a way that simplifies the critical components to the point where it is possible to prove that they function as required. Critical to such an approach is a trusted computing base (TCB), which is itself provably trustworthy, and at the same time general enough to support efficient construction of the systems of interest. In our case, the TCB is based on the seL4 microkernel, which has been formally verified to be implemented according to specification, the first (and to date only) operating-system kernel with such a high degree of assurance. The lecture will examine the implications of our approach on system structure, design and implementation, report on progress to date in verifying functional and non-functional properties of the TCB, and the approach taken to enable full-system guarantees.

Watched 624 times.