Gernot Heiser

Last updated

Gernot Heiser
GH 29 crop.jpg
Gernot Heiser speaking at the UNSW CSE Research Expo October 25 2022
Born1957 (age 66–67)
Nationality German, Australian
Education University of Freiburg, BSc
Brock University, MSc
ETH Zurich, PhD
Known for Operating system teaching, research, commercialising
Awards Leopoldina Member (2023)
RSN Fellow (2022)
ACM SIGOPS Hall of Fame Award (2019)
ATSE Fellow (2016)
IEEE Fellow (2016)
ACM Fellow (2014)
Scientific career
Fields Computer science
Institutions University of New South Wales (Scientia Professor and John Lions Chair of Operating Systems)
NICTA (research group leader)
Open Kernel Labs (founder, former CTO, director)
Website gernot-heiser.org

Gernot Heiser (born 1957) is a Scientia Professor and the John Lions Chair for operating systems at UNSW Sydney, where he leads the Trustworthy Systems group (TS).

Contents

Life

In 1991, Heiser joined the School of Computer Science and Engineering of UNSW Sydney, originally as a lecturer, reaching the rank of full professor in 2002, a position he retains to date.

Also in 2002 he joined the newly created research organisation NICTA as one of its initial Program Leaders, in charge of the Embedded, Real-Time and Operating Systems (ERTOS) program. After a re-organisation in 2011 ERTOS became the Software Systems Research Group (SSRG) which he led. When NICTA was absorbed into CSIRO in 2016, Heiser stepped back from management of the group, which was then called Trustworthy Systems (TS). In 2021 CSIRO abandoned TS, [1] at which time Heiser took the group back to UNSW and re-assumed its leadership.

Since April 2020, Heiser serves as the Founding Chairman of the seL4 Foundation.

Research

Heiser's research focuses on microkernels, microkernel-based systems, and virtual machines, and emphasizes performance and reliability.

His group produced Mungi, a single address space operating system, [2] for clusters of 64-bit computers, and implementations of the L4 microkernel with very fast inter-process communication. [3] His Gelato@UNSW team was a founding member of the Gelato Federation, and focused on performance and scalability of Linux on Itanium. They established theoretical and practical performance limits of message passing inter-process communication (IPC) on Itanium. [4]

After joining NICTA at its creation in 2002, his research shifted away from high-end computing platforms, and toward embedded systems, with the aim of improving security, safety, and reliability via use of microkernel technology. [5] This led to the development of a new microkernel, called seL4, and its formal verification, claimed to be the first-ever complete proof of the functional correctness of a general-purpose OS kernel. [6]

His work on virtualization was motivated by the need to provide a complete OS environment on his microkernels. His Wombat project followed the approach taken with the L4Linux project at Dresden, but was a multi-architecture paravirtualized Linux running on x86, ARM and MIPS hardware. The Wombat work later formed the basis for the OKL4 hypervisor of his company Open Kernel Labs (OK Labs). The desire to reduce the engineering effort of paravirtualization led to the development of the soft layering approach of automated paravirtulization which was demonstrated on x86 and Itanium hardware. [7] His work on virtual non-uniform memory access (vNUMA) demonstrated a hypervisor which presents a distributed system as a shared-memory multiprocessor as a possible model for many-core chips with large numbers of processor cores. [8]

Device drivers are another focus of his work, including the first demonstration of user-mode drivers with a performance overhead of less than 10%, [9] an approach to driver development that eliminates most typical driver bugs by design, [10] device drivers produced from device test benches, [11] and a demonstration of the feasibility of generating device drivers automatically from formal specifications. [12] He also conducted research on operating-system-level energy management. [13]

Since leaving OK Labs in 2010 he focussed almost exclusively on seL4 and high-assurance seL4-based systems, both in research and in technology transfer. Notable research achievements include sound and complete worst-case execution-time (WCET) analysis of seL4, claimed to be the first ever such analysis for a protected-mode OS kernel. [14] [15] His work on extending seL4’s functionality to support mixed-criticality systems (MCS) led to making time a first-class resource in seL4’s capability system. [16]

Focussing on microarchitectural timing channels, he demonstrated in 2015 the first practical cross-core timing side channel attack. [17] This led to work on the systematic prevention of timing-channel leakage, and the proposal of a set of mechanisms for achieving this, collectively referred as time protection. [18]

In the past, he also worked on semiconductor device simulation, where he pioneered use of multi-dimensional modeling to optimize silicon-based solar cells. [19]

Awards and honours

Related Research Articles

<span class="mw-page-title-main">Microkernel</span> Kernel that provides fewer services than a traditional kernel

In computer science, a microkernel is the near-minimum amount of software that can provide the mechanisms needed to implement an operating system (OS). These mechanisms include low-level address space management, thread management, and inter-process communication (IPC).

Mach is a kernel developed at Carnegie Mellon University by Richard Rashid and Avie Tevanian to support operating system research, primarily distributed and parallel computing. Mach is often considered one of the earliest examples of a microkernel. However, not all versions of Mach are microkernels. Mach's derivatives are the basis of the operating system kernel in GNU Hurd and of Apple's XNU kernel used in macOS, iOS, iPadOS, tvOS, and watchOS.

The trusted computing base (TCB) of a computer system is the set of all hardware, firmware, and/or software components that are critical to its security, in the sense that bugs or vulnerabilities occurring inside the TCB might jeopardize the security properties of the entire system. By contrast, parts of a computer system that lie outside the TCB must not be able to misbehave in a way that would leak any more privileges than are granted to them in accordance to the system's security policy.

L4 is a family of second-generation microkernels, used to implement a variety of types of operating systems (OS), though mostly for Unix-like, Portable Operating System Interface (POSIX) compliant types.

<span class="mw-page-title-main">Isabelle (proof assistant)</span> Higher-order logic (HOL) automated theorem prover

The Isabelle automated theorem prover is a higher-order logic (HOL) theorem prover, written in Standard ML and Scala. As an LCF-style theorem prover, it is based on a small logical core (kernel) to increase the trustworthiness of proofs without requiring — yet supporting — explicit proof objects.

<span class="mw-page-title-main">XNU</span> Computer operating system kernel

XNU is the computer operating system (OS) kernel developed at Apple Inc. since December 1996 for use in the Mac OS X operating system and released as free and open-source software as part of the Darwin OS, which in addition to macOS is also the basis for the Apple TV Software, iOS, iPadOS, watchOS, visionOS, and tvOS OSes.

<span class="mw-page-title-main">Jochen Liedtke</span> German computer scientist

Jochen Liedtke was a German computer scientist, noted for his work on microkernel operating systems, especially in creating the L4 microkernel family.

In computer science, a single address space operating system is an operating system that provides only one globally shared address space for all processes. In a single address space operating system, numerically identical logical addresses in different processes all refer to exactly the same byte of data.

A hybrid kernel is an operating system kernel architecture that attempts to combine aspects and benefits of microkernel and monolithic kernel architectures used in operating systems.

<span class="mw-page-title-main">PikeOS</span> Real-time operating system

PikeOS is a commercial hard real-time operating system (RTOS) which features a separation kernel-based hypervisor. This hypervisor supports multiple logical partition types for various operating systems (OS) and applications, each referred to as a GuestOS. PikeOS is designed to facilitate the development of certifiable smart devices for the Internet of Things (IoT) by adhering to high standards of quality, safety, and security across different industries. In instances where memory management units (MMU) are not present but memory protection units (MPU) are available on controller-based systems, PikeOS for MPU is designed for critical real-time applications and provides up-to-standard safety and security.

A separation kernel is a type of security kernel used to simulate a distributed environment. The concept was introduced by John Rushby in a 1981 paper. Rushby proposed the separation kernel as a solution to the difficulties and problems that had arisen in the development and verification of large, complex security kernels that were intended to "provide multilevel secure operation on general-purpose multi-user systems." According to Rushby, "the task of a separation kernel is to create an environment which is indistinguishable from that provided by a physically distributed system: it must appear as if each regime is a separate, isolated machine and that information can only flow from one machine to another along known external communication lines. One of the properties we must prove of a separation kernel, therefore, is that there are no channels for information flow between regimes other than those explicitly provided."

<span class="mw-page-title-main">Kernel (operating system)</span> Core of a computer operating system

The kernel is a computer program at the core of a computer's operating system and generally has complete control over everything in the system. The kernel is also responsible for preventing and mitigating conflicts between different processes. It is the portion of the operating system code that is always resident in memory and facilitates interactions between hardware and software components. A full kernel controls all hardware resources via device drivers, arbitrates conflicts between processes concerning such resources, and optimizes the utilization of common resources e.g. CPU & cache usage, file systems, and network sockets. On most systems, the kernel is one of the first programs loaded on startup. It handles the rest of startup as well as memory, peripherals, and input/output (I/O) requests from software, translating them into data-processing instructions for the central processing unit.

Open Kernel Labs is a privately owned company that develops microkernel-based hypervisors and operating systems for embedded systems. The company was founded in 2006 by Steve Subar and Gernot Heiser as a spinout from NICTA. It was headquartered in Chicago, while research and development was located in Sydney, Australia. The company was acquired by General Dynamics in September 2012.

A distributed operating system is system software over a collection of independent software, networked, communicating, and physically separate computational nodes. They handle jobs which are serviced by multiple CPUs. Each individual node holds a specific software subset of the global aggregate operating system. Each subset is a composite of two distinct service provisioners. The first is a ubiquitous minimal kernel, or microkernel, that directly controls that node's hardware. Second is a higher-level collection of system management components that coordinate the node's individual and collaborative activities. These components abstract microkernel functions and support user applications.

<span class="mw-page-title-main">Device driver synthesis and verification</span>

Device drivers are programs which allow software or higher-level computer programs to interact with a hardware device. These software components act as a link between the devices and the operating systems, communicating with each of these systems and executing commands. They provide an abstraction layer for the software above and also mediate the communication between the operating system kernel and the devices below.

In computing, Wombat is an operating system, a high-performance virtualised Linux embedded operating system marketed by Open Kernel Labs, a spin-off of National ICT Australia's Embedded, Real Time, Operating System Program.

<span class="mw-page-title-main">Rump kernel</span> Software run in userspace that offers kernel functionality

The NetBSD rump kernel is the first implementation of the "anykernel" concept where drivers either can be compiled into or run in the monolithic kernel or in user space on top of a light-weight kernel. The NetBSD drivers can be used on top of the rump kernel on a wide range of POSIX operating systems, such as the Hurd, Linux, NetBSD, DragonFly BSD, Solaris kernels and even Cygwin, along with the file system utilities built with the rump libraries. The rump kernels can also run without POSIX directly on top of the Xen hypervisor, an L4 microkernel using the Genode OS Framework or even on "OS-less" bare metal.

<span class="mw-page-title-main">Unikernel</span> Specialised, single address space machine images

A unikernel is a computer program statically linked with the operating system code on which it depends. Unikernels are built with a specialized compiler that identifies the operating system services that a program uses and links it with one or more library operating systems that provide them. Such a program requires no separate operating system and can run instead as the guest of a hypervisor.

<span class="mw-page-title-main">ACM SIGOPS</span> ACMs Special Interest Group on Operating Systems

ACM SIGOPS is the Association for Computing Machinery's Special Interest Group on Operating Systems, an international community of students, faculty, researchers, and practitioners associated with research and development related to operating systems. The organization sponsors international conferences related to computer systems, operating systems, computer architectures, distributed computing, and virtual environments. In addition, the organization offers multiple awards recognizing outstanding participants in the field, including the Dennis M. Ritchie Doctoral Dissertation Award, in honor of Dennis Ritchie, co-creator of the C programming language and Unix operating system.

<span class="mw-page-title-main">Genode</span> Free and open-source software operating system

Genode is a free and open-source software operating system (OS) framework consisting of a microkernel abstraction layer and a set of user space components. The framework is notable as one of the few open-source operating systems not derived from a proprietary OS, such as Unix. The characteristic design philosophy is that a small trusted computing base is of primary concern in a security-oriented OS.

References

  1. ↑ Data61 drops world-class seL4 security team, 21 May 2021, InnovationAus.com
  2. ↑ Heiser, Gernot; Elphinstone, Kevin; Vochteloo, Jerry; Stephen, Russell; Jochen, Liedtke (1998). "The Mungi Single-Address-Space Operating System". Software: Practice and Experience. 28 (9): 901–928. CiteSeerX   10.1.1.146.4216 . doi:10.1002/(SICI)1097-024X(19980725)28:9<901::AID-SPE181>3.0.CO;2-7. S2CID   62189930.
  3. ↑ Liedtke, Jochen; Elphinstone, Kevin; Schönberg, Sebastian; Härtig, Hermann; Heiser, Gernot; Islam, Nayeem; Jaeger, Trent (May 1997). "Achieved IPC performance (still the foundation for extensibility)". 6th Workshop on Hot Topics in Operating Systems. Cape Cod, Massachusetts, United States: IEEE. pp. 28–31.
  4. ↑ Gray, Charles; Chapman, Matthew; Chubb, Peter; Mosberger-Tang, David; Heiser, Gernot (April 2005). "Itanium: a system implementor's tale" (PDF). Proceedings of the 2005 USENIX Annual Technical Conference. Anaheim, CA, USA.
  5. ↑ Heiser, Gernot; Elphinstone, Kevin; Kuz, Ihor; Klein, Gerwin; Petters, Stefan M. (July 2007). "Towards trustworthy computing systems: Taking microkernels to the next level". ACM Operating Systems Review. 41 (4): 3–11. doi:10.1145/1278901.1278904. hdl: 1959.4/39906 . S2CID   9036194.
  6. 1 2 Klein, Gerwin; Elphinstone, Kevin; Heiser, Gernot; Andronick, June; Cock, David; Derrin, Philip; Elkaduwe, Dhammika; Engelhardt, Kai; Kolanski, Rafal; Norrish, Michael; Sewell, Thomas; Tuch, Harvey; Winwood, Simon (October 2009). "seL4: Formal verification of an OS kernel" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA.
  7. ↑ LeVasseur, Joshua; Uhlig, Volkmar; Yang, Yaowei; Chapman, Matthew; Chubb, Peter; Leslie, Ben; Heiser, Gernot (August 2008). "Pre-virtualization: Soft layering for virtual machines" (PDF). 13th IEEE Asia-Pacific Computer Systems Architecture Conference. Hsinchu, Taiwan.
  8. ↑ Chapman, Matthew; Heiser, Gernot (June 2009). "vNUMA: A virtual shared-memory multiprocessor" (PDF). USENIX Annual Technical Conference. San Diego, CA, USA.
  9. ↑ Leslie, Ben; Chubb, Peter; Fitzroy-Dale, Nicholas; Götz, Stefan; Gray, Charles; Macpherson, Luke; Potts, Daniel; Shen, Yueting (Rita); Elphinstone, Kevin; Heiser, Gernot (September 2005). "User-level device drivers: Achieved performance". Journal of Computer Science and Technology. 20 (5): 654–664. CiteSeerX   10.1.1.59.6766 . doi:10.1007/s11390-005-0654-4. S2CID   1121537.
  10. ↑ Ryzhyk, Leonid; Chubb, Peter; Kuz, Ihor; Heiser, Gernot (April 2009). "Dingo: Taming device drivers" (PDF). 4th EuroSys Conference. Nuremberg, Germany.
  11. ↑ Ryzhyk, Leonid; Keys, John; Mirla, Balachandra; Raghunath, Arun; Vij, Mona; Heiser, Gernot (March 2011). "Improved device driver reliability through hardware verification reuse" (PDF). 16th International Conference on Architectural Support for Programming Languages and Operating Systems. Newport Beach, CA, USA.
  12. ↑ Ryzhyk, Leonid; Chubb, Peter; Kuz, Ihor; Le Sueur, Etienne; Heiser, Gernot (October 2009). "Automatic device driver synthesis with Termite" (PDF). 22nd ACM Symposium on Operating System Principles. Big Sky, MT, USA.
  13. ↑ Snowdon, David C.; Le Sueur, Etienne; Petters, Stefan M.; Heiser, Gernot (April 2009). "Koala: A platform for OS-level power management" (PDF). 4th EuroSys Conference. Nuremberg, Germany.
  14. ↑ Blackham, Bernard; Heiser, Gernot (April 2013). "Sequoll: a framework for model checking binaries" (PDF). IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). Philadelphia, USA.
  15. ↑ Sewell, Thomas; Kam, Felix; Heiser, Gernot (April 2016). "Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis" (PDF). IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). Vienna, Austria.
  16. ↑ Lyons, Anna; McLeod, Kent; Almatary, Hesham; Heiser, Gernot (April 2018). "Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time" (PDF). EuroSys Conference. Porto, Portugal.
  17. ↑ Liu, Fangfei; Yarom, Yuval; Ge, Qian; Heiser, Gernot; Lee, Ruby B (May 2015). "Last-Level Cache Side-Channel Attacks are Practical" (PDF). IEEE Symposium on Security and Privacy. San Jose, CA, USA.
  18. ↑ Ge, Qian; Yarom, Yuval; Chothia, Tom; Heiser, Gernot (March 2019). "Time Protection: the Missing OS Abstraction" (PDF). EuroSys Conference. Dresden, Germany.
  19. ↑ Aberle, Armin G; Altermatt, Pietro P.; Heiser, Gernot; Robinson, Stephen J.; Wang, Aihua; Zhao, Jianhua; Krumbein, Ulrich; Green, Martin A. (1995). "Limiting loss mechanisms in 23-percent efficient silicon solar cells". Journal of Applied Physics. 77 (7): 3491–3504. doi:10.1063/1.358643.
  20. ↑ Member of Leopoldina
  21. ↑ Fellows of the Royal Society of NSW
  22. ↑ ACM Distinguished Speakers list
  23. ↑ ACM SIGOPS Hall of Fame Award
  24. ↑ ATSE Fellow
  25. ↑ Fellow of the IEEE
  26. ↑ ACS ICT Researcher of the Year 2015
  27. ↑ ACM Fellows 2014
  28. ↑ NSW Premier's Prizes for Science & Engineering
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.