Search For:

Displaying 1-13 out of 13 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...
 
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...
     
Towards a verified component platform
Found in: Proceedings of the Seventh Workshop on Programming Languages and Operating Systems (PLOS '13)
By Gerwin Klein, Ihor Kuz, June Andronick, Matthew Fernandez
Issue Date:November 2013
pp. 1-7
This paper describes ongoing work on a new technique for reducing the cost of assurance of large software systems by building on a verified component platform. From a component architecture description, we automatically derive a formal model of the system ...
     
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 ...
     
Translation validation for a verified OS kernel
Found in: Proceedings of the 34th ACM SIGPLAN conference on Programming language design and implementation (PLDI '13)
By Gerwin Klein, Magnus O. Myreen, Thomas Arthur Leck Sewell
Issue Date:June 2013
pp. 471-482
We extend the existing formal verification of the seL4 operating system microkernel from 9500 lines of C source code to the binary level. We handle all functions that were part of the previous verification. Like the original verification, we currently omit...
     
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...
     
capDL: a language for describing capability-based systems
Found in: Proceedings of the first ACM asia-pacific workshop on Workshop on systems (APSys '10)
By Adam Walker, Corey Lewis, Gerwin Klein, Ihor Kuz
Issue Date:August 2010
pp. 31-36
Capabilities provide an access control model that can be used to construct systems where safety of protection can be precisely determined. However, in order to be certain of the security provided by such systems it is necessary to verify that their capabil...
     
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...
     
Experience report: seL4: formally verifying a high-performance microkernel
Found in: Proceedings of the 14th ACM SIGPLAN international conference on Functional programming (ICFP '09)
By Gerwin Klein, Kevin Elphinstone, Philip Derrin
Issue Date:August 2009
pp. 91-96
We report on our experience using Haskell as an executable specification language in the formal verification of the seL4 microkernel. The verification connects an abstract operational specification in the theorem prover Isabelle/HOL to a C implementation o...
     
Types, bytes, and separation logic
Found in: Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL '07)
By Gerwin Klein, Harvey Tuch, Michael Norrish
Issue Date:January 2007
pp. 949-984
We present a formal model of memory that both captures the low-level features of C's pointers and memory, and that forms the basis for an expressive implementation of separation logic. At the low level, we do not commit common oversimplifications, but corr...
     
Running the manual: an approach to high-assurance microkernel development
Found in: Proceedings of the 2006 ACM SIGPLAN workshop on Haskell (Haskell '06)
By David Cock, Gerwin Klein, Kevin Elphinstone, Manuel M. T. Chakravarty, Philip Derrin
Issue Date:September 2006
pp. 60-71
We propose a development methodology for designing and prototyping high assurance microkernels, and describe our application of it. The methodology is based on rapid prototyping and iterative refinement of the microkernel in a functional programming langua...
     
A machine-checked model for a Java-like language, virtual machine, and compiler
Found in: ACM Transactions on Programming Languages and Systems (TOPLAS)
By Gerwin Klein, Tobias Nipkow
Issue Date:July 2006
pp. 619-695
We introduce Jinja, a Java-like programming language with a formal semantics designed to exhibit core features of the Java language architecture. Jinja is a compromise between the realism of the language and the tractability and clarity of its formal seman...
     
 1