Making trusted systems trustworthy
Prof. Gernot Heiser
Recorded 12 September 2013 in Lausanne, Vaud, Switzerland
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 to trustworthy systems, which aims to constructing systems such that their dependability can be proved. Fundamentally our approach is based on strong isolation of components, combined with strictly controlled communication channels which are subject to system-wide security policies. Isolation and communication are provided by a secure microkernel, seL4. We ensure that it provides safety and security by proving that its API enforces the correct isolation properties (confidentiality and integrity), that its implementation is correct with respect to its specification (i.e. API), and that the binary is a correct translation of the C implementation. We also perform a complete and sound timing analysis, in order to guarantee real-time performance. For the approach to work in practice, we must also ensure that seL4 is efficient, meaning it does not impose undue overheads on systems built on top.
Having achieved all this, we are now focussing on building complete systems on top of seL4, and proving that the overall system satisfies its safety or security requirements. One of these is an autonomous aerial vehicle developed by a consortium of NICTA, Rockwell Collins, Galois and Boeing under the DARPA HACMS program.
Watched 674 times.Watch