Tuesday, January 11, 2011
Speaker: Gernot Heiser
Venue: IST Austria
Computer systems are routinely deployed in life- andmission- critical situations, yet in most cases theirsecurity, safety or dependability cannot be assured to thedegree warranted by the appli- cation. In other words,trusted computer systems are rarely really trustworthy.
We believe that this is highly unsatisfactory, and have embarked on alarge research program aimed at bringing reality in linewith expectations. In this talk describes NICTA’s researchagenda for achieving true trustworthiness in systems. Thefirst pahse has been concluded, with the world’s firstformal proof of functional correctness of a complete OSmicrokernel. The second phase, in progress, aims at makingdependability guarantees for complete real-world systems,comprising millions of lines of code.
Gernot Heiser holds the position of Scientia Professro andJohn Lions Chair of Operating Systems at theUniversity of New South Wales (UNSW), and leads the TrustworthyEmbedded Systems (ERTOS) group at NICTA, Australia’sNational Centre of Excellence for ICT Research. He joined NICTA at its creation in 2002, and before that was afull-time member of academic staff at UNSW from 1991. Hispast work included the Mungi single-address-spaceoperating system, several un-broken records in IPCperformance, and the best-ever reported performance foruser-level device drivers.
In 2006, Gernot with a number of his students founded OpenKernel Labs, now the market leader in secureoperating-systems and virtualization technology for mobilewireless devices. The company’s OKL4 operating system, adescendent of L4 kernels developed by his group at UNSWand NICTA, is deployed in more than a billion mobilephones. This includes the Motorola Evoke, the first (andto date only) mobile phone running a high-level OS (Linux)and a modem stack on the same processor core.
In a former life, Gernot developed semiconductor devicesimulators and models of device physics for suchsimulators, and pioneered the use of three-dimensionaldevice simulation for the characterisation andoptimisation of high-performance silicon solar cells.