Gernot Heiser: Difference between revisions

Add links
From Wikipedia, the free encyclopedia
Browse history interactively
← Previous edit
Content deleted Content added
VisualWikitext
Bot: Removing Commons:File:GH 29 crop.jpg (en). It was deleted on Commons by Krd (No license since 17 November 2022).
Tag: Reverted
m added "Category:Kernel programmers"
 
(23 intermediate revisions by 10 users not shown)
Line 1: Line 1:
{{Short description|Australian computer scientist}}
{{Short description|Australian computer scientist}}
{{Cleanup bare URLs|date=August 2022}}
{{Use dmy dates|date=April 2022}}
{{Use dmy dates|date=April 2022}}
{{Infobox scientist
{{Infobox scientist
Line 6: Line 5:
| native_name =
| native_name =
| native_name_lang =
| native_name_lang =
| image =
| image = GH 29 crop.jpg
| alt =
| alt =
| caption = Gernot Heiser speaking at the UNSW CSE Research Expo October 25 2022
| caption = Gernot Heiser speaking at the UNSW CSE Research Expo October 25 2022
Line 32: Line 31:
| influences =
| influences =
| influenced =
| influenced =
| awards = [[List of Fellows of the Association for Computing Machinery|ACM Fellow]] (2014)
| awards = [[German National Academy of Sciences Leopoldina|Leopoldina Member]] (2023)<br /> [[Royal Society of New South Wales|RSN Fellow]] (2022)<br /> [[ACM SIGOPS|ACM SIGOPS Hall of Fame Award]] (2019)<br /> [[Australian Academy of Technology and Engineering|ATSE Fellow]] (2016)<br /> [[Institute of Electrical and Electronics Engineers|IEEE Fellow]] (2016)<br /> [[List of Fellows of the Association for Computing Machinery|ACM Fellow]] (2014)
| spouse = <!-- or | spouses = -->
| spouse = <!-- or | spouses = -->
| partner = <!-- or | partners = -->
| partner = <!-- or | partners = -->
Line 38: Line 37:
| signature = <!-- Filename only -->
| signature = <!-- Filename only -->
| signature_alt =
| signature_alt =
| website = {{URL|gernot-heiser.org}}
| website = {{URL|https://gernot-heiser.org}}
| footnotes =
| footnotes =
}}
}}
'''Gernot Heiser''' (born 1957) is a Scientia [[Professor]] and the [[John Lions]] Chair for [[operating system]]s at the [[University of New South Wales]] (UNSW). He is also leader of the [http://ssrg.nicta.com.au/ Software Systems Research Group (SSRG)] at [[NICTA]]. In 2006, he cofounded [[Open Kernel Labs]] (OK Labs, acquired in 2012 by [[General Dynamics]]) to commercialise his [[L4 microkernel]] technology.
'''Gernot Heiser''' (born 1957) is a Scientia [[Professor]] and the [[John Lions]] Chair for [[operating system|operating systems]] at [[University of New South Wales|UNSW Sydney]], where he leads the [https://trustworthy.systems Trustworthy Systems] group (TS).


== Life ==
== Life ==
In 1991, Heiser joined the [[UNSW School of Computer Science and Engineering|School of Computer Science and Engineering]] of [[University of New South Wales|UNSW Sydney]], originally as a lecturer, reaching the rank of full professor in 2002, a position he retains to date.
Heiser was born in 1957. He earned a BSc studying physics at the German [[University of Freiburg]], an MSc at the Canadian [[Brock University]], and a PhD at the Swiss [[ETH Zurich]].

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,<ref>[https://www.innovationaus.com/data61-dumps-world-class-sel4-security-team/ ''Data61 drops world-class seL4 security team'', 21 May 2021, InnovationAus.com ]</ref> 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 [https://sel4.foundation seL4 Foundation].


== Research ==
== Research ==
Heiser's research focuses on [[microkernel]]s, microkernel-based systems, and [[virtual machine]]s, and emphasizes performance and reliability.
Heiser's research focuses on [[microkernel|microkernels]], microkernel-based systems, and [[virtual machine|virtual machines]], and emphasizes performance and reliability.


His group produced ''Mungi'', a [[single address space operating system]],<ref>{{cite journal
His group produced ''Mungi'', a [[single address space operating system]],<ref>{{cite journal
Line 74: Line 77:
| url = http://ieeexplore.ieee.org/xpl/RecentCon.jsp?punumber=4643
| url = http://ieeexplore.ieee.org/xpl/RecentCon.jsp?punumber=4643
}}</ref>
}}</ref>
His [http://gelato.unsw.edu.au/ 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.<ref>
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.<ref>
{{cite conference
{{cite conference
| last1 = Gray| first1=Charles| last2=Chapman| first2=Matthew| last3=Chubb| first3=Peter| last4=Mosberger-Tang| first4=David| last5=Heiser| first5=Gernot
| last1 = Gray
| first1 = Charles
| date = April 2005
|last2=Chapman |first2=Matthew |last3=Chubb |first3=Peter |last4=Mosberger-Tang |first4=David |last5=Heiser |first5=Gernot
|date=April 2005
| title = Itanium: a system implementor's tale
| title = Itanium: a system implementor's tale
| url = https://www.usenix.org/legacy/event/usenix05/tech/general/gray/gray.pdf
| book-title = Proceedings of the 2005 USENIX Annual Technical Conference
| book-title = Proceedings of the 2005 USENIX Annual Technical Conference
| location = Anaheim, CA, USA
| location = Anaheim, CA, USA
}}</ref>
}}</ref>


Since 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.<ref>
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.<ref>
{{cite journal
{{cite journal
| last1 = Heiser
| last1 = Heiser
| first1 = Gernot
| first1 = Gernot
|last2=Elphinstone |first2=Kevin |last3=Kuz |first3=Ihor |last4=Klein |first4=Gerwin |last5=Petters |first5=Stefan M.
| last2=Elphinstone |first2=Kevin |last3=Kuz |first3=Ihor |last4=Klein |first4=Gerwin |last5=Petters |first5=Stefan M.
|date=July 2007
| date=July 2007
| title = Towards trustworthy computing systems: Taking microkernels to the next level
| title = Towards trustworthy computing systems: Taking microkernels to the next level
| journal = ACM Operating Systems Review
| journal = ACM Operating Systems Review
Line 96: Line 98:
| volume = 41
| volume = 41
| issue = 4
| issue = 4
| pages = 3–11
| pages = 3–11
| hdl = 1959.4/39906
| hdl = 1959.4/39906
| s2cid = 9036194
| s2cid = 9036194
| url = https://unsworks.unsw.edu.au/fapi/datastream/unsworks:4547/SOURCE1?view=true
| url = https://unsworks.unsw.edu.au/fapi/datastream/unsworks:4547/SOURCE1?view=true
| hdl-access = free
}}</ref>
}}</ref>
This led to the development of a new microkernel called
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 (operating system)|kernel]].<ref name="sel4">
[http://ertos.nicta.com.au/research/sel4/ seL4], and its
[https://web.archive.org/web/20090822042016/http://ertos.nicta.com.au/research/l4.verified/ formal verification],
claimed to be the first-ever complete proof of the functional correctness of a general-purpose OS [[Kernel (operating system)|kernel]].<ref>
{{cite conference
{{cite conference
| last1 = Klein
| last1 = Klein
Line 116: Line 116:
}}</ref>
}}</ref>


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 University of Technology|Dresden]], but was a multi-architecture [[Paravirtualization|paravirtualized]] Linux running on [[x86]], [[ARM architecture|ARM]] and [[MIPS architecture|MIPS]] hardware. The Wombat work later formed the basis for the OKL4 [[hypervisor]] of his company [[Open Kernel Labs]] (OK Labs).
His work on virtualization was motivated by the need to provide a
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.<ref>
complete OS environment on his microkernels. His Wombat project
followed the approach taken with the
[http://os.inf.tu-dresden.de/L4/LinuxOnL4/ L4Linux] project at
[[Dresden University of Technology|Dresden]], but was a
multi-architecture [[Paravirtualization|paravirtualized]] Linux
running on [[x86]], [[ARM architecture|ARM]] and [[MIPS architecture|MIPS]] hardware. The Wombat work later formed the basis for the ''OKL4'' [[hypervisor]] of his company [[Open Kernel 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.<ref>
{{cite conference
{{cite conference
|last1 = LeVasseur| first1=Joshua| last2=Uhlig| first2=Volkmar| last3=Yang| first3=Yaowei| last4=Chapman| first4=Matthew| last5=Chubb| first5=Peter| last6=Leslie| first6=Ben| last7=Heiser| first7=Gernot
|last1 = LeVasseur
|first1 = Joshua
| date = August 2008
|last2=Uhlig |first2=Volkmar |last3=Yang |first3=Yaowei |last4=Chapman |first4=Matthew |last5=Chubb |first5=Peter |last6=Leslie |first6=Ben |last7=Heiser |first7=Gernot
|date=August 2008
| title = Pre-virtualization: Soft layering for virtual machines
| title = Pre-virtualization: Soft layering for virtual machines
| url = https://trustworthy.systems/publications/nicta_full_text/1064.pdf
| book-title = 13th IEEE Asia-Pacific Computer Systems Architecture Conference
| book-title = 13th IEEE Asia-Pacific Computer Systems Architecture Conference
| location = Hsinchu, Taiwan
| location = Hsinchu, Taiwan
}}</ref>
}}</ref>
His vNUMA work 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.<ref>
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.<ref>
{{cite conference
{{cite conference
|last1 = Chapman
| last1 = Chapman| first1=Matthew| last2=Heiser| first2=Gernot
|first1 = Matthew
| date = June 2009
|last2=Heiser |first2=Gernot
|date=June 2009
| title = vNUMA: A virtual shared-memory multiprocessor
| title = vNUMA: A virtual shared-memory multiprocessor
| url = https://trustworthy.systems/publications/nicta_full_text/1642.pdf
| book-title = USENIX Annual Technical Conference
| book-title = USENIX Annual Technical Conference
| location = San Diego, CA, USA
| location = San Diego, CA, USA
Line 165: Line 155:
|last1=Ryzhyk |first1=Leonid |author2=Chubb, Peter |author3=Kuz, Ihor |author4=Heiser, Gernot
|last1=Ryzhyk |first1=Leonid |author2=Chubb, Peter |author3=Kuz, Ihor |author4=Heiser, Gernot
| title = Dingo: Taming device drivers
| title = Dingo: Taming device drivers
| url = https://trustworthy.systems/publications/nicta_full_text/1527.pdf
| book-title = 4th EuroSys Conference
| book-title = 4th EuroSys Conference
|date=April 2009
| date=April 2009
| location = Nuremberg, Germany
| location = Nuremberg, Germany
}}</ref>
}}</ref>
device drivers produced from device test benches,<ref>
device drivers produced from device test benches,<ref>
{{cite conference
{{cite conference
| last1=Ryzhyk| first1=Leonid| last2=Keys| first2=John| last3=Mirla| first3=Balachandra| last4=Raghunath| first4=Arun| last5=Vij| first5=Mona| last6=Heiser| first6=Gernot
|last1=Ryzhyk |first1=Leonid
| date = March 2011
|last2=Keys |first2=John |last3=Mirla |first3=Balachandra |last4=Raghunath |first4=Arun |last5=Vij |first5=Mona |last6=Heiser |first6=Gernot
|date=March 2011
| title = Improved device driver reliability through hardware verification reuse
| title = Improved device driver reliability through hardware verification reuse
| url = https://trustworthy.systems/publications/nicta_full_text/4136.pdf
| book-title = 16th International Conference on Architectural Support for Programming Languages and Operating Systems
| book-title = 16th International Conference on Architectural Support for Programming Languages and Operating Systems
| location = Newport Beach, CA, USA
| location = Newport Beach, CA, USA
Line 180: Line 171:
and a demonstration of the feasibility of generating device drivers automatically from formal specifications.<ref>
and a demonstration of the feasibility of generating device drivers automatically from formal specifications.<ref>
{{cite conference
{{cite conference
|last1=Ryzhyk |first1=Leonid
| last1=Ryzhyk |first1=Leonid
|last2=Chubb |first2=Peter |last3=Kuz |first3=Ihor |last4=Le Sueur |first4=Etienne |last5=Heiser |first5=Gernot
| last2=Chubb |first2=Peter |last3=Kuz |first3=Ihor |last4=Le Sueur |first4=Etienne |last5=Heiser |first5=Gernot
|date=October 2009
| date = October 2009
| title = Automatic device driver synthesis with Termite
| title = Automatic device driver synthesis with Termite
| book-title = 22nd ACM Symposium on Operating System Principles
| book-title = 22nd ACM Symposium on Operating System Principles
Line 188: Line 179:
| url = http://www.sigops.org/sosp/sosp09/papers/ryzhyk-sosp09.pdf
| url = http://www.sigops.org/sosp/sosp09/papers/ryzhyk-sosp09.pdf
}}</ref>
}}</ref>
Recent research also includes power management.<ref>
He also conducted research on operating-system-level energy management.<ref>
{{cite conference
{{cite conference
| last1 = Snowdon| first1 = David C.| last2=Le Sueur| first2=Etienne| last3=Petters| first3=Stefan M.| last4=Heiser| first4=Gernot
| last1 = Snowdon
| first1 = David C.
|last2=Le Sueur |first2=Etienne |last3=Petters |first3=Stefan M. |last4=Heiser |first4=Gernot
|date=April 2009
| title = Koala: A platform for OS-level power management
| title = Koala: A platform for OS-level power management
| url = https://trustworthy.systems/publications/nicta_full_text/1528.pdf
| date = April 2009
| book-title = 4th EuroSys Conference
| book-title = 4th EuroSys Conference
| location = Nuremberg, Germany
| location = Nuremberg, Germany
}}</ref>

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|worst-case execution-time]] (WCET) analysis of seL4, claimed to be the first ever such analysis for a [[CPU modes|protected-mode]] OS kernel.<ref>
{{cite conference
| last1 = Blackham |first1=Bernard |last2=Heiser |first2=Gernot
| title = Sequoll: a framework for model checking binaries
| url = https://trustworthy.systems/publications/nicta_full_text/6405.pdf
| book-title = IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)
| date = April 2013
| location = Philadelphia, USA
}}</ref><ref>
{{cite conference
| last1 = Sewell| first1=Thomas| last2=Kam| first2=Felix| last3=Heiser| first3=Gernot
| title = Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis
| url = https://trustworthy.systems/publications/nicta_full_text/9118.pdf
| book-title = IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS)
| date = April 2016
| location = Vienna, Austria
}}</ref>
His work on extending seL4’s functionality to support [[Mixed criticality|mixed-criticality systems]] (MCS) led to making time a first-class resource in seL4’s [[Capability-based security|capability]] system.<ref>
{{cite conference
| last1 = Lyons| first1=Anna| last2=McLeod| first2=Kent| last3=Almatary| first3=Hesham| last4=Heiser| first4=Gernot
| title = Scheduling-Context Capabilities: A Principled, Light-Weight OS Mechanism for Managing Time
| url = https://trustworthy.systems/publications/full_text/Lyons_MAH_18.pdf
| book-title = EuroSys Conference
| date = April 2018
| location = Porto, Portugal
}}</ref>

Focussing on [[Microarchitecture|microarchitectural]] [[Covert_channel#Timing_channels|timing channels]], he demonstrated in 2015 the first practical cross-core timing side channel attack.<ref>
{{cite conference
| last1 = Liu |first1=Fangfei |last2=Yarom |first2=Yuval |last3=Ge |first3=Qian |last4=Heiser |first4=Gernot |last5=Lee |first5=Ruby B
| title = Last-Level Cache Side-Channel Attacks are Practical
| url = https://trustworthy.systems/publications/nicta_full_text/8432.pdf
| book-title = IEEE Symposium on Security and Privacy
| date = May 2015
| location = San Jose, CA, USA
}}</ref>
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''.<ref>
{{cite conference
| last1 = Ge |first1=Qian |last2=Yarom |first2=Yuval |last3=Chothia |first3=Tom |last4=Heiser |first4=Gernot
| title = Time Protection: the Missing OS Abstraction
| url = https://trustworthy.systems/publications/full_text/Ge_YCH_19.pdf
| book-title = EuroSys Conference
| date = March 2019
| location = Dresden, Germany
}}</ref>
}}</ref>


Line 213: Line 249:
}}</ref>
}}</ref>


== Operating system projects ==
== Awards and honours ==
* [[German National Academy of Sciences Leopoldina]] (Leopoldina) (Member) (2023)<ref>[https://www.leopoldina.org/en/members/list-of-members/list-of-members/member/Member/show/gernot-heiser/ Member of Leopoldina]</ref>
* [http://ertos.nicta.com.au/research/sel4/ seL4] 3rd-generation microkernel
* The [[Royal Society of New South Wales]] (RSN) (Fellow) (2022)<ref>[https://royalsoc.org.au/images/fellows-pages/RSN-H-Fellows.html#fellow-heiser-gernot Fellows of the Royal Society of NSW]</ref>
* [https://web.archive.org/web/20090822042016/http://ertos.nicta.com.au/research/l4.verified/ L4.verified] formal verification of seL4
* [[Association for Computing Machinery]] (ACM) Distinguished Speaker (2021)<ref>[https://speakers.acm.org/speakers ACM Distinguished Speakers list]</ref>
* [http://ertos.nicta.com.au/research/drivers/ Dingo and Termite] frameworks for reliable device drivers
* [[ACM SIGOPS]] Together with his co-authors (he was 3rd author) Heiser received the Hall of Fame Award (2019),<ref>[https://www.sigops.org/awards/hof/ ACM SIGOPS Hall of Fame Award]</ref> for the paper ''"seL4: Formal Verification of an OS Kernel"'' <ref name="sel4" />
* [http://ertos.nicta.com.au/research/power/ Koala] framework for OS-level energy management
* [[Australian Academy of Technology and Engineering]] (ATSE) Fellow (2016)<ref>[https://www.atse.org/content/publications/media-releases-2016-atse-names-25-new-fellows.aspx ATSE Fellow]</ref>
* [http://ertos.nicta.com.au/research/virtualisation/vnuma.pml vNUMA], a hypervisor providing shared virtual memory on a cluster
* [[Institute of Electrical and Electronics Engineers]] (IEEE) Fellow (2016) ''"For contributions to security and safety of operating systems"'' <ref>[https://www.computer.org/press-room/2015-news/cs-fellows-2016 Fellow of the IEEE]</ref>
* [http://www.ertos.nicta.com.au/research/mungi/ Mungi] and [http://www.ertos.nicta.com.au/iguana/ Iguana] [[single address space operating system]]s
* [[Australian Computer Society]] (ACS) ICT Researcher of the Year (2015)<ref>[https://www.engineering.unsw.edu.au/computer-science-engineering/news/cses-professor-gernot-heiser-named-ict-researcher-of-the-year-2015 ACS ICT Researcher of the Year 2015]</ref>
* [http://www.ertos.nicta.com.au/wombat/ Wombat] portable [[Linux]] on [[L4 microkernel]]
* [[Association for Computing Machinery]] (ACM) Fellow (2014) ''"For contributions demonstrating that provably correct operating systems are feasible and suitable for real-world use"'' <ref>[http://awards.acm.org/award_winners/heiser_2552925.cfm ACM Fellows 2014]</ref>
* [http://gelato.unsw.edu.au/ Gelato@UNSW] performance and scalability of [[Linux]] on [[Itanium]]
* Scientia Professor of the [[University of New South Wales]]
* [http://www.cse.unsw.edu.au/~disy/L4/MIPS/ L4/MIPS] 64-bit L4 microkernel on MIPS architecture
* 2010 Innovation Hero of [[The Warren Centre for Advanced Engineering]] at the [[University of Sydney]]

* NSW Scientist of the Year 2009 Category Engineering, Mathematics and Computer Sciences<ref>[https://www.chiefscientist.nsw.gov.au/events/nsw-premiers-prizes-for-science-and-engineering/previous-winners NSW Premier's Prizes for Science & Engineering]</ref>
== Teaching ==
* Best Paper at the 22nd ACM SIGOPS Symposium on Operating Systems Principles, 2009
* [http://www.cse.unsw.edu.au/~cs9242 Advanced Operating Systems] at UNSW

== Awards ==
* [[Australian Academy of Technology and Engineering]] (ATSE) Fellow (2016).<ref>https://www.atse.org/content/publications/media-releases-2016-atse-names-25-new-fellows.aspx</ref>
* [[Institute of Electrical and Electronics Engineers]] (IEEE) Fellow (2016) ''"For contributions to security and safety of operating systems"''.
* [[Australian Computer Society]] (ACS) ICT Researcher of the Year (2015).<ref>[https://www.engineering.unsw.edu.au/computer-science-engineering/news/cses-professor-gernot-heiser-named-ict-researcher-of-the-year-2015 ACS ICT Researcher of the Year 2015]</ref>
* [[Association for Computing Machinery]] (ACM) Fellow (2014) ''"For contributions demonstrating that provably correct operating systems are feasible and suitable for real-world use"''.<ref>[http://awards.acm.org/award_winners/heiser_2552925.cfm Gernot Heiser ACM Fellows 2014]</ref>
* [http://www.hr.unsw.edu.au/employee/acad/scientia.html Scientia Professor] of the [[University of New South Wales]]
* [https://web.archive.org/web/20110101170811/http://sydney.edu.au/warrencentre/IHA/2010.html 2010 Innovation Hero] of [[The Warren Centre for Advanced Engineering]] at the [[University of Sydney]]
* [https://web.archive.org/web/20091216225611/http://www.osmr.nsw.gov.au/science_communication/science_promotion/scientist_of_the_year/announcement_2009 NSW Scientist of the Year 2009] Category Engineering, Mathematics and Computer Sciences
* [http://www.sigops.org/sosp/sosp09/program.html#session6 Best Paper] at the 22nd ACM SIGOPS Symposium on Operating Systems Principles, 2009
* Best Paper at the 13th IEEE Asia-Pacific Computer Systems Architecture Conference, 2008
* Best Paper at the 13th IEEE Asia-Pacific Computer Systems Architecture Conference, 2008
* Best Student Paper at the 2005 USENIX Annual Technical Conference
* Best Student Paper at the 2005 USENIX Annual Technical Conference
Line 243: Line 269:


== External links ==
== External links ==
* {{Official website|gernot-heiser.org}}
* {{Official website|https://gernot-heiser.org}}
* [https://microkerneldude.wordpress.com/ Gernot Heiser's blog]
* [https://microkerneldude.org Gernot Heiser's blog]
* [https://ts.data61.csiro.au/people/?cn=Gernot+Heiser Bio] at [[CSIRO]] with full publication list
* [https://trustworthy.systems/people/?cn=Gernot+Heiser Bio] at [[University of New South Wales|UNSW]] with full publication list


{{Microkernel}}
{{Microkernel}}
Line 256: Line 282:
[[Category:German computer scientists]]
[[Category:German computer scientists]]
[[Category:Computer systems researchers]]
[[Category:Computer systems researchers]]
[[Category:University of New South Wales faculty]]
[[Category:Academic staff of the University of New South Wales]]
[[Category:Fellows of the Australian Academy of Technological Sciences and Engineering]]
[[Category:Fellows of the Australian Academy of Technological Sciences and Engineering]]
[[Category:Kernel programmers]]

Latest revision as of 12:43, 6 March 2024

Gernot Heiser
Gernot Heiser speaking at the UNSW CSE Research Expo October 25 2022
Born1957 (age 66–67)
NationalityGerman, Australian
EducationUniversity of Freiburg, BSc
Brock University, MSc
ETH Zurich, PhD
Known forOperating system teaching, research, commercialising
AwardsLeopoldina Member (2023)
RSN Fellow (2022)
ACM SIGOPS Hall of Fame Award (2019)
ATSE Fellow (2016)
IEEE Fellow (2016)
ACM Fellow (2014)
Scientific career
FieldsComputer science
InstitutionsUniversity of New South Wales (Scientia Professor and John Lions Chair of Operating Systems)
NICTA (research group leader)
Open Kernel Labs (founder, former CTO, director)
Websitegernot-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).

Life[edit]

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[edit]

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[edit]

References[edit]

  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. ^ a b 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

External links[edit]

Retrieved from "https://en.wikipedia.org/w/index.php?title=Gernot_Heiser&oldid=1212166703"