Gernot Heiser

Orcid: 0000-0002-7069-0831

Affiliations:
  • University of New South Wales, Sydney, Australia


According to our database1, Gernot Heiser authored at least 120 papers between 1986 and 2024.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2014, "For contributions demonstrating that provably correct operating systems are feasible and suitable for real-world use.".

IEEE Fellow

IEEE Fellow 2016, "For contributions to security and safety of operating systems".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
fence.t.s: Closing Timing Channels in High-Performance Out-of-Order Cores through ISA-Supported Temporal Partitioning.
CoRR, 2024

2023
Systematic Prevention of On-Core Timing Channels by Full Temporal Partitioning.
IEEE Trans. Computers, May, 2023

Proving the Absence of Microarchitectural Timing Channels.
CoRR, 2023

Pancake: Verified Systems Programming Made Sweeter.
Proceedings of the 12th Workshop on Programming Languages and Operating Systems, 2023

AutoCC: Automatic Discovery of Covert Channels in Time-Shared Hardware.
Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, 2023

Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems.
Proceedings of the Formal Methods - 25th International Symposium, 2023

Tutorial: Using the seL4 Microkernel.
Proceedings of the 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2023

Verified Value Chains, Innovation and Competition.
Proceedings of the IEEE International Conference on Cyber Security and Resilience, 2023

First steps in verifying the seL4 Core Platform.
Proceedings of the 14th ACM SIGOPS Asia-Pacific Workshop on Systems, 2023

2022
Can We Put the "S" Into IoT?
Proceedings of the 8th IEEE World Forum on Internet of Things, 2022

Property-Based Testing: Climbing the Stairway to Verification.
Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering, 2022

2021
Microarchitectural Timing Channels and their Prevention on an Open-Source 64-bit RISC-V Core.
Proceedings of the Design, Automation & Test in Europe Conference & Exhibition, 2021

2020
Towards Provable Timing-Channel Prevention.
ACM SIGOPS Oper. Syst. Rev., 2020

Benchmarking Flaws Undermine Security Research.
IEEE Secur. Priv., 2020

Prevention of Microarchitectural Covert Channels on an Open-Source 64-bit RISC-V Core.
CoRR, 2020

seL4 in Australia: from research to real-world trustworthy systems.
Commun. ACM, 2020

2019
Can We Prove Time Protection?
Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

Time Protection: The Missing OS Abstraction.
Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, 2019

SoK: Benchmarking Flaws in Systems Security.
Proceedings of the IEEE European Symposium on Security and Privacy, 2019

Fault Tolerance Through Redundant Execution on COTS Multicores: Exploring Trade-Offs.
Proceedings of the 49th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, 2019

2018
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware.
J. Cryptogr. Eng., 2018

Roundtable: Machine Learning for Embedded Systems: Hype or Lasting Impact?
IEEE Des. Test, 2018

For Safety's Sake: We Need a New Hardware-Software Contract!
IEEE Des. Test, 2018

Benchmarking Crimes: An Emerging Threat in Systems Security.
CoRR, 2018

A Formal Approach to Constructing Secure Air Vehicle Software.
Computer, 2018

Formally verified software in the real world.
Commun. ACM, 2018

Scheduling-context capabilities: a principled, light-weight operating-system mechanism for managing time.
Proceedings of the Thirteenth EuroSys Conference, 2018

No Security Without Time Protection: We Need a New Hardware-Software Contract.
Proceedings of the 9th Asia-Pacific Workshop on Systems, 2018

The Jury Is In: Monolithic OS Design Is Flawed: Microkernel-based Designs Improve Security.
Proceedings of the 9th Asia-Pacific Workshop on Systems, 2018

2017
High-assurance timing analysis for a high-assurance real-time operating system.
Real Time Syst., 2017

Technical Perspective: Proving file systems meet expectations.
Commun. ACM, 2017

The Cogent Case for Property-Based Testing.
Proceedings of the 9th Workshop on Programming Languages and Operating Systems, 2017

A Performance Evaluation of Rump Kernels as a Multi-server OS Building Block on seL4.
Proceedings of the 8th Asia-Pacific Workshop on Systems, Mumbai, India, September 2, 2017, 2017

2016
L4 Microkernels: The Lessons from 20 Years of Research and Deployment.
ACM Trans. Comput. Syst., 2016

State of the Journal.
IEEE Trans. Computers, 2016

Report on the Asia-Pacific Systems Workshop 2015 (APSys'15).
ACM SIGOPS Oper. Syst. Rev., 2016

It's Time: OS Mechanisms for Enforcing Asymmetric Temporal Integrity.
CoRR, 2016

Do Hardware Cache Flushing Operations Actually Meet Our Expectations?
CoRR, 2016

An Evaluation of Coarse-Grained Locking for Multicore Microkernels.
CoRR, 2016

Complete, High-Assurance Determination of Loop Bounds and Infeasible Paths for WCET Analysis.
Proceedings of the 2016 IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS), 2016

CATalyst: Defeating last-level cache side channel attacks in cloud computing.
Proceedings of the 2016 IEEE International Symposium on High Performance Computer Architecture, 2016

CoGENT: Verifying High-Assurance File System Implementations.
Proceedings of the Twenty-First International Conference on Architectural Support for Programming Languages and Operating Systems, 2016

2015
Mapping the Intel Last-Level Cache.
IACR Cryptol. ePrint Arch., 2015

Last-Level Cache Side-Channel Attacks are Practical.
Proceedings of the 2015 IEEE Symposium on Security and Privacy, 2015

For a Microkernel, a Big Lock Is Fine.
Proceedings of the 6th Asia-Pacific Workshop on Systems, 2015

2014
A Scalable Lock Manager for Multicores.
ACM Trans. Database Syst., 2014

Comprehensive formal verification of an OS microkernel.
ACM Trans. Comput. Syst., 2014

File systems deserve verification too!
ACM SIGOPS Oper. Syst. Rev., 2014

Mobile multicores: use them or waste them.
ACM SIGOPS Oper. Syst. Rev., 2014

Unifying DVFS and offlining in mobile multicores.
Proceedings of the 20th IEEE Real-Time and Embedded Technology and Applications Symposium, 2014

Trickle: Automated infeasible path detection using all minimal unsatisfiable subsets.
Proceedings of the 20th IEEE Real-Time and Embedded Technology and Applications Symposium, 2014

The Last Mile: An Empirical Study of Timing Channels on seL4.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

2013
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013

Sequoll: A framework for model checking binaries.
Proceedings of the 19th IEEE Real-Time and Embedded Technology and Applications Symposium, 2013

Code optimizations using formally verified properties.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications, 2013

The von Neumann Architecture Is Due for Retirement.
Proceedings of the 14th Workshop on Hot Topics in Operating Systems, 2013

RapiLog: reducing system complexity through verification.
Proceedings of the Eighth Eurosys Conference 2013, 2013

The systems hacker's guide to the galaxy energy usage in a modern smartphone.
Proceedings of the Asia-Pacific Workshop on Systems, 2013

2012
It's Time for Trustworthy Systems.
IEEE Secur. Priv., 2012

Improving interrupt response time in a verifiable protected microkernel.
Proceedings of the European Conference on Computer Systems, 2012

Trustworthy Real-Time Systems.
Proceedings of the Advances in Real-Time Systems (to Georg Färber on the occasion of his appointment as Professor Emeritus at TU München after leading the Lehrstuhl für Realzeit-Computersysteme for 34 illustrious years)., 2012

To preempt or not to preempt, that is the question.
Proceedings of the Asia-Pacific Workshop on Systems, 2012

Correct, fast, maintainable: choose any three!
Proceedings of the Asia-Pacific Workshop on Systems, 2012

2011
Architecture optimisation with currawong.
Comput. Commun. Rev., 2011

Slow Down or Sleep, That Is the Question.
Proceedings of the 2011 USENIX Annual Technical Conference, 2011

Timing Analysis of a Protected Operating System Kernel.
Proceedings of the 32nd IEEE Real-Time Systems Symposium, 2011

What If You Could Actually Trust Your Kernel?
Proceedings of the 13th Workshop on Hot Topics in Operating Systems, 2011

Virtualizing embedded systems: why bother?
Proceedings of the 48th Design Automation Conference, 2011

Low-overhead virtualization of mobile platforms.
Proceedings of the 14th International Conference on Compilers, 2011

Improved device driver reliability through hardware verification reuse.
Proceedings of the 16th International Conference on Architectural Support for Programming Languages and Operating Systems, 2011

Hardware-supported virtualization on ARM.
Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

Protected hard real-time: the next frontier.
Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

Static analysis of device drivers: we can do better!
Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

2010
seL4: formal verification of an operating-system kernel.
Commun. ACM, 2010

An Analysis of Power Consumption in a Smartphone.
Proceedings of the 2010 USENIX Annual Technical Conference, 2010

The case for active device drivers.
Proceedings of the 1st ACM SIGCOMM Asia-Pacific Workshop on Systems, 2010

The OKL4 microvisor: convergence point of microkernels and hypervisors.
Proceedings of the 1st ACM SIGCOMM Asia-Pacific Workshop on Systems, 2010

Improved Device Driver Reliability Through Verification Reuse.
Proceedings of the Sixth Workshop on Hot Topics in System Dependability, 2010

The road to trustworthy systems.
Proceedings of the fifth ACM workshop on Scalable trusted computing, 2010

2009
vNUMA: A Virtual Shared-Memory Multiprocessor.
Proceedings of the 2009 USENIX Annual Technical Conference, 2009

Automatic device driver synthesis with termite.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

seL4: formal verification of an OS kernel.
Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Koala: a platform for OS-level power management.
Proceedings of the 2009 EuroSys Conference, Nuremberg, Germany, April 1-3, 2009, 2009

Dingo: taming device drivers.
Proceedings of the 2009 EuroSys Conference, Nuremberg, Germany, April 1-3, 2009, 2009

Hypervisors for Consumer Electronics.
Proceedings of the 6th IEEE Consumer Communications and Networking Conference, 2009

2008
The role of virtualization in embedded systems.
Proceedings of the 1st Workshop on Isolation and Integration in Embedded Systems, 2008

Operating System Verification for Real Use.
Proceedings of the 5th International Verification Workshop in connection with IJCAR 2008, 2008

Pre-virtualization: Soft layering for virtual machines.
Proceedings of the 13th Asia-Pacific Computer Systems Architecture Conference, 2008

2007
Your System Is Secure? Prove It!
login Usenix Mag., 2007

Towards trustworthy computing systems: taking microkernels to the next level.
ACM SIGOPS Oper. Syst. Rev., 2007

CAmkES: A component model for secure microkernel-based embedded systems.
J. Syst. Softw., 2007

Measurements or Static Analysis or Both?.
Proceedings of the 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis, 2007

Reboots Are for Hardware: Challenges and Solutions to Updating an Operating System on the Fly.
Proceedings of the 2007 USENIX Annual Technical Conference, 2007

Formalising device driver interfaces.
Proceedings of the 4th workshop on Programming languages and operating systems, 2007

Hype and Virtue.
Proceedings of HotOS'07: 11th Workshop on Hot Topics in Operating Systems, 2007

Towards a Practical, Verified Kernel.
Proceedings of HotOS'07: 11th Workshop on Hot Topics in Operating Systems, 2007

Accurate on-line prediction of processor and memoryenergy usage under voltage scaling.
Proceedings of the 7th ACM & IEEE International conference on Embedded software, 2007

2006
Are virtual-machine monitors microkernels done right?
ACM SIGOPS Oper. Syst. Rev., 2006

Panel: Is University Systems Teaching and Research Relevant to Industry?.
Proceedings of the 2006 USENIX Annual Technical Conference, 2006

2005
Secure Embedded Systems Need Microkernels.
login Usenix Mag., 2005

User-Level Device Drivers: Achieved Performance.
J. Comput. Sci. Technol., 2005

Itanium - A System Implementor's Tale(Awarded General Track Best Student Paper Award!).
Proceedings of the 2005 USENIX Annual Technical Conference, 2005

Implementing Transparent Shared Memory on Clusters Using Virtual Machines.
Proceedings of the 2005 USENIX Annual Technical Conference, 2005

Providing Dynamic Update in an Operating System.
Proceedings of the 2005 USENIX Annual Technical Conference, 2005

OS Verification - Now!
Proceedings of HotOS'05: 10th Workshop on Hot Topics in Operating Systems, 2005

2003
Legba: Fast Hardware Support for Fine-Grained Protection.
Proceedings of the Advances in Computer Systems Architecture, 2003

Implementation of Fast Address-Space Switching and TLB Sharing on the StrongARM Processor.
Proceedings of the Advances in Computer Systems Architecture, 2003

Variable Radix Page Table: A Page Table for Modern Architectures.
Proceedings of the Advances in Computer Systems Architecture, 2003

2002
Fault tolerance and avoidance in biomedical systems.
Proceedings of the 10th ACM SIGOPS European Workshop, Saint-Emilion, France, July 1, 2002, 2002

2001
Secure OS Extensibility Needn't Cost an Arm and a Leg.
Proceedings of HotOS-VIII: 8th Workshop on Hot Topics in Operating Systems, 2001

Components + Security = OS Extensibility.
Proceedings of the 6th Australasian Computer Systems Architecture Conference (ACSAC 2001), 2001

2000
Fast Address-Space Switching on the StrongARM SA-1100 Processor.
Proceedings of the 5th Australasian Computer Architecture Conference (ACAC 2000), 31 January, 2000

1999
Linking Programs in a Single Address Space.
Proceedings of the 1999 USENIX Annual Technical Conference, 1999

1998
The Mungi Single-Address-Space Operating System.
Softw. Pract. Exp., 1998

1997
Achieved IPC Performance.
Proceedings of The Sixth Workshop on Hot Topics in Operating Systems, 1997

1996
Supporting Persistent Object Systems in a Single Address Space.
Proceedings of the 7th Workshop on Persistent Object Systems, 1996

Libra: A Library for Reliable Distributed Applications.
Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, 1996

1991
Design and implementation of a three-dimensional, general purpose semiconductor device simulatior.
PhD thesis, 1991

Three-dimensional numerical semiconductor device simulation: algorithms, architectures, results.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst., 1991

1986
A Portable Operating System Interface and Utility Library.
IEEE Softw., 1986


  Loading...