<html><head><style type='text/css'>p { margin: 0; }</style></head><body><div style='font-family: arial,helvetica,sans-serif; font-size: 12pt; color: #000000'><span style="font-family:"Georgia","serif";color:#1F497D"><img id="_x0000_i1025" src="cid:image001.jpg@01CC834C.F1941A30" alt="SeminarLogo.jpg" height="160" width="480"></span><div style="color:#000;font-weight:normal;font-style:normal;text-decoration:none;font-family:Helvetica,Arial,sans-serif;font-size:12pt;"><div class="WordSection1">
<p class="MsoNormal" style="text-indent:.5in;text-autospace:none"><b><span style="font-family:"Georgia","serif"">Speaker: Prof. Gernot Heiser</span></b></p>
<p class="MsoNormal" style="text-indent:.5in;text-autospace:none"><span style="font-family:"Georgia","serif""> University of New South Wales
</span></p>
<p class="MsoNormal" style="text-indent:.5in;text-autospace:none"><b><span style="font-family:"Georgia","serif"">Title: Towards Principled Temporal Isolation in the Operating System<i></i></span></b></p>
<p class="MsoNormal" style="text-indent:.5in"><b><span style="font-family:"Georgia","serif"">Date: Monday, August 10, 2015</span></b></p>
<p class="MsoNormal" style="text-indent:.5in"><b><span style="font-family:"Georgia","serif"">Time:
</span></b><span style="font-family:"Georgia","serif"">11:00 a.m.<b> </b></span><b><span style="font-size:10.0pt;font-family:"Georgia","serif""> </span></b><b><span style="font-family:"Georgia","serif""> </span></b></p>
<p class="MsoNormal" style="text-indent:.5in"><b><span style="font-family:"Georgia","serif"">Room:
</span></b><span style="font-family:"Georgia","serif"">E-Quad, Room B205</span></p>
<p class="MsoNormal" style="text-indent:.5in"><b><span style="font-family:"Georgia","serif"">Host: Prof. Ruby Lee</span></b></p>
<p class="MsoNormal" style="text-indent:.5in"><b><span style="font-family:NewCenturySchlbk"> </span></b></p>
<p class="MsoNormal"><b><span style="font-family:"Georgia","serif"">Abstract: </span></b><span style="font-family:"Georgia","serif"">Spatial isolation, i.e. controlling memory access, forms the basis of protection in operating systems. However, this is neither
sufficient for ensuring safe operation of real-time systems, nor for ensuring confidentiality. It must be complemented by temporal isolation, i.e. preventing a process from unduly influencing the execution speed of another process. Most operating systems
provide very poor temporal isolation if any. Exceptions are systems designed to support a narrow class of applications (either hard real-time systems or separation kernels for security-critical uses), which also tend to have high overheads or force low system
utilisation.</span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif""> </span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif"">The formally-verified seL4 microkernel is a general-purpose high-assurance platform that is intended to support a wide range of uses, including highly performance-sensitive mobile systems, (safety)
multi-criticality systems and (security-critical) cross-domain solutions. We are therefore after mechanisms that provide strong temporal isolation where needed, but avoid overheads where not. The talk will discuss present work in progress on simple kernel
mechanisms that will allow us to achieve those goals.</span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif""> </span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif""> </span></p>
<p class="MsoNormal"><b><span style="font-family:"Georgia","serif"">Biography: </span>
</b><span style="font-family:"Georgia","serif"">Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW, and leads the Software Systems Research Group at NICTA, Australia’s National Centre of Excellence for ICT Research. He joined
NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991. His past work included the Mungi single-address-space operating system (OS), several un-broken records in IPC performance, and the best-ever reported
performance for user-level device drivers. More recently he led the team at NICTA which produced the world’s first formal proof of functional correctness of a protected general-purpose operating-system kernel, the first published sound worst-case execution
time analysis of a protected OS kernel, and the synthesis of high-performance device drivers.
</span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif""> </span></p>
<p class="MsoNormal"><span style="font-family:"Georgia","serif"">In 2006, Gernot with a number of his students founded Open Kernel Labs, to market secure virtualization technology for embedded systems. The company’s OKL4 operating system, a descendent of L4
kernels developed by his group at UNSW and NICTA, is deployed in billions of mobile devices, and now ships on the security processor of all iOS devices. Open Kernel Labs was sold to General Dynamics in August 2012.</span></p>
<p class="MsoNormal"><b><span style="font-family:"Georgia","serif";color:#1F497D"> </span></b><br></p></div></div></div></body></html>