Real-Time and Real Trustworthiness: Timing Analysis of a Protected OS Kernel

Add to your list(s) Download to your calendar using vCal

• Bernard Blackham (NICTA)
• Monday 21 November 2011, 15:00-16:00
• FW26, Computer Laboratory, William Gates Builiding.

If you have a question about this talk, please contact Eiko Yoneki.

This talk is cancelled.

Protected operating systems have been an elusive target of static worst-case execution time (WCET) analysis, due to a combination of their size, unstructured code and tight coupling with hardware. As a result, critical hard real-time systems are usually developed without memory protection, in order to provide guarantees on their response time.

In this talk, I will explore a WCET analysis of seL4, a third-generation microkernel. seL4 is the world’s first formally-verified operating-system kernel, featuring machine-checked correctness proofs of its complete functionality. This makes seL4 an ideal platform for security-critical systems. Adding temporal guarantees makes seL4 also a compelling platform for safety- and timing-critical systems. It enables hard real-time systems with less critical time-sharing components to be integrated on the same processor, supporting enhanced functionality while keeping hardware and development costs low.

The talk will focus on the more interesting aspects of the analysis, and in particular, properties of the seL4 code base which made life easier in the process.

This work was presented at: Real-time Systems Symposium 2011 (Vienna, Austria)

Bio: Bernard is a PhD candidate at the University of New South Wales and NICTA in Sydney, Australia. His PhD relates to real-time aspects of the seL4 microkernel. Bernard’s research interests include static analysis, process checkpointing, and generally messing with anything executable. Bernard also trains the Australian team for the International Olympiad in Informatics.

This talk is part of the Computer Laboratory Systems Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• CL's SRG seminar
• Cambridge Centre for Data-Driven Discovery (C2D3)
• Cambridge talks
• Chris Davis' list
• Computer Laboratory Security Seminar
• Computer Laboratory Systems Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• FW26, Computer Laboratory, William Gates Builiding
• Interested Talks
• School of Technology
• Security-related talks
• Trust & Technology Initiative - interesting events
• bld31
• ndk22's list
• ob366-ai4er
• rp587

Note that ex-directory lists are not shown.