Search For:

Displaying 1-23 out of 23 total
It's Time for Trustworthy Systems
Found in: IEEE Security and Privacy
By Gernot Heiser,Toby Murray,Gerwin Klein
Issue Date:March 2012
pp. 67-70
The time has arrived for truly trustworthy systems, backed by machine-checked proofs of security and reliability. Research demonstrates that formal whole-system analysis that applies to the C and binary implementation level is feasible, including proofs of...
 
Components + Security = OS Extensibility
Found in: Australasian Computer Systems Architecture Conference
By Antony Edwards, Gernot Heiser
Issue Date:January 2001
pp. 27
Component-based programming systems have shown themselves to be a natural way of constructing extensible software. Well-defined interfaces, encapsulation, late binding and polymorphism promote extensibility, yet despite this synergy, components have not be...
 
Fast Address-Space Switching on the StrongARM SA-1100 Processor
Found in: Australasian Computer Architecture Conference
By Adam Wiggins, Gernot Heiser
Issue Date:February 2000
pp. 97
The StrongARM SA-1100 is a high-speed low-power processor aimed at embedded and portable applications. Its architecture features virtual caches and TLBs which are not tagged by an address-space identifier. Consequently, context switches on that processor a...
 
Sequoll: A framework for model checking binaries
Found in: 2013 IEEE 19th Real-Time and Embedded Technology and Applications Symposium (RTAS)
By Bernard Blackham,Gernot Heiser
Issue Date:April 2013
pp. 97-106
Multi-criticality real-time systems require protected-mode operating systems with bounded interrupt latencies and guaranteed isolation between components. A tight WCET analysis of such systems requires trustworthy information about loop bounds and infeasib...
 
Timing Analysis of a Protected Operating System Kernel
Found in: Real-Time Systems Symposium, IEEE International
By Bernard Blackham,Yao Shi,Sudipta Chattopadhyay,Abhik Roychoudhury,Gernot Heiser
Issue Date:December 2011
pp. 339-348
Operating systems offering virtual memory and protected address spaces have been an elusive target of static worst-case execution time (WCET) analysis. This is due to a combination of size, unstructured code and tight coupling with hardware. As a result, h...
 
Comprehensive formal verification of an OS microkernel
Found in: ACM Transactions on Computer Systems (TOCS)
By Gernot Heiser, Gerwin Klein, June Andronick, Kevin Elphinstone, Rafal Kolanski, Thomas Sewell, Toby Murray
Issue Date:February 2014
pp. 1-70
We present an in-depth coverage of the comprehensive machine-checked formal verification of seL4, a general-purpose operating system microkernel. We discuss the kernel design we used to make its verification tractable. We then describe the functional corre...
     
Mobile multicores: use them or waste them
Found in: Proceedings of the Workshop on Power-Aware Computing and Systems (HotPower '13)
By Gernot Heiser, Aaron Carroll
Issue Date:November 2013
pp. 1-5
Energy management is a primary consideration in the design of modern smartphones, made more interesting by the recent proliferation of multi-core processors in this space. We investigate how core offlining and DVFS can be used together on these systems to ...
     
File systems deserve verification too!
Found in: Proceedings of the Seventh Workshop on Programming Languages and Operating Systems (PLOS '13)
By Gabriele Keller, Gernot Heiser, Gerwin Klein, Leonid Ryzhyk, Liam O'Connor, Sidney Amani, Toby Murray, Zilin Chen
Issue Date:November 2013
pp. 1-7
File systems are too important, and current ones are too buggy, to remain unverified. Yet the most successful verification methods for functional correctness remain too expensive for current file system implementations --- we need verified correctness but ...
     
From L3 to seL4 what have we learnt in 20 years of L4 microkernels?
Found in: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles (SOSP '13)
By Gernot Heiser, Kevin Elphinstone
Issue Date:November 2013
pp. 133-150
The L4 microkernel has undergone 20 years of use and evolution. It has an active user and developer community, and there are commercial versions which are deployed on a large scale and in safety-critical systems. In this paper we examine the lessons learnt...
     
Code optimizations using formally verified properties
Found in: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications (OOPSLA '13)
By Gernot Heiser, Yao Shi, Bernard Blackham
Issue Date:October 2013
pp. 427-442
Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are then ...
     
Improving interrupt response time in a verifiable protected microkernel
Found in: Proceedings of the 7th ACM european conference on Computer Systems (EuroSys '12)
By Bernard Blackham, Gernot Heiser, Yao Shi
Issue Date:April 2012
pp. 323-336
Many real-time operating systems (RTOSes) offer very small interrupt latencies, in the order of tens or hundreds of cycles. They achieve this by making the RTOS kernel fully preemptible, permitting interrupts at almost any point in execution except for som...
     
The road to trustworthy systems
Found in: Proceedings of the fifth ACM workshop on Scalable trusted computing (STC '10)
By Gernot Heiser, Gerwin Klein, Ihor Kuz, June Andronick, Kevin Elphinstone, Leonid Ryzhyk
Issue Date:October 2010
pp. 3-10
Computer systems are routinely deployed in life- and mission-critical situations, yet their security, safety or dependability can in most cases not be assured to the degree warranted by the application. In other words, trusted computer systems are rarely r...
     
The case for active device drivers
Found in: Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys '10)
By Gernot Heiser, Leonid Ryzhyk, Yanjin Zhu
Issue Date:August 2010
pp. 25-30
We revisit the device-driver architecture supported by the majority of operating systems, where a driver is a passive object that does not have its own thread of control and is only activated when an external thread invokes one of its entry points. This ar...
     
The OKL4 microvisor: convergence point of microkernels and hypervisors
Found in: Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys '10)
By Ben Leslie, Gernot Heiser
Issue Date:August 2010
pp. 19-24
We argue that recent hypervisor-vs-microkernel discussions completely miss the point. Fundamentally, the two classes of systems have much in common, and provide similar abstractions. We assert that the requirements for both types of systems can be met with...
     
Architecture optimisation with Currawong
Found in: Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys '10)
By Gernot Heiser, Ihor Kuz, Nicholas FitzRoy-Dale
Issue Date:August 2010
pp. 7-12
We describe Currawong, a tool to perform system software architecture optimisation. Currawong is an extensible tool which applies optimisations at the point where an application invokes framework or library code. Currawong does not require source code to p...
     
seL4: formal verification of an operating-system kernel
Found in: Communications of the ACM
By David Cock, Dhammika Elkaduwe, Gernot Heiser, Gerwin Klein, Harvey Tuch, June Andronick, Kai Engelhardt, Kevin Elphinstone, Michael Norrish, Philip Derrin, Rafal Kolanski, Simon Winwood, Thomas Sewell
Issue Date:June 2010
pp. 120-ff
New algorithms provide the ability for robust but scalable image search.
     
seL4: formal verification of an OS kernel
Found in: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09)
By David Cock, Dhammika Elkaduwe, Gernot Heiser, Gerwin Klein, Harvey Tuch, June Andronick, Kai Engelhardt, Kevin Elphinstone, Michael Norrish, Philip Derrin, Rafal Kolanski, Simon Winwood, Thomas Sewell
Issue Date:October 2009
pp. 207-220
Complete formal verification is the only known way to guarantee that a system is free of programming errors. We present our experience in performing the formal, machine-checked verification of the seL4 microkernel from an abstract specification down to its...
     
Automatic device driver synthesis with termite
Found in: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles (SOSP '09)
By Etienne Le Sueur, Gernot Heiser, Ihor Kuz, Leonid Ryzhyk, Peter Chubb
Issue Date:October 2009
pp. 73-86
Faulty device drivers cause significant damage through down time and data loss. The problem can be mitigated by an improved driver development process that guarantees correctness by construction. We achieve this by synthesising drivers automatically from f...
     
Koala: a platform for OS-level power management
Found in: Proceedings of the fourth ACM european conference on Computer systems (EuroSys '09)
By David C. Snowdon, Etienne Le Sueur, Gernot Heiser, Stefan M. Petters
Issue Date:April 2009
pp. 29-32
Managing the power consumption of computing platforms is a complicated problem thanks to a multitude of hardware configuration options and characteristics. Much of the academic research is based on unrealistic assumptions, and has, therefore, seen little p...
     
Dingo: taming device drivers
Found in: Proceedings of the fourth ACM european conference on Computer systems (EuroSys '09)
By Gernot Heiser, Ihor Kuz, Leonid Ryzhyk, Peter Chubb
Issue Date:April 2009
pp. 29-32
Device drivers are notorious for being a major source of failure in operating systems. In analysing a sample of real defects in Linux drivers, we found that a large proportion (39%) of bugs are due to two key shortcomings in the device-driver architecture ...
     
The role of virtualization in embedded systems
Found in: Proceedings of the 1st workshop on Isolation and integration in embedded systems (IIES '08)
By Gernot Heiser
Issue Date:April 2008
pp. 11-16
System virtualization, which enjoys immense popularity in the enterprise and personal computing spaces, is recently gaining significant interest in the embedded domain. Starting from a comparison of key characteristics of enterprise systems and embedded sy...
     
Formalising device driver interfaces
Found in: Proceedings of the 4th workshop on Programming languages and operating systems (PLOS '07)
By Gernot Heiser, Ihor Kuz, Leonid Ryzhyk
Issue Date:October 2007
pp. 1-1
The lack of well-defined protocols for interaction with the operating system is a common source of defects in device drivers. In this paper we investigate the use of a formal language to define these protocols unambiguously. We present a language that allo...
     
Fault tolerance and avoidance in biomedical systems
Found in: Proceedings of the 10th workshop on ACM SIGOPS European workshop: beyond the PC (EW10)
By Gernot Heiser, Shane Stephens
Issue Date:July 2002
pp. 198-200
It is important for a variety of reasons that biomedical systems execute without errors. One useful approach towards error-free software is to design a range of fault tolerant properties into applications software. In addition, by restricting the behaviour...
     
 1