This page is part of an archival collection and is no longer actively maintained.

It may contain outdated information and may not meet current or future WCAG accessibility standards. We provide this content, its subpages, and associated links for historical reference only. If you need assistance, please contact support@cs.washington.edu

UNSAT: Hyperkernel

Hyperkernel

Hyperkernel explores a push-button approach to building provably correct OS kernels.

Applications and extensions

  • Several systems extend or reuse the Hyperkernel verifier:
    • CertiQ is a verification framework for the Qiskit quantum compiler.
    • Nickel is a verification framework for information flow control systems.
    • Serval implements the reference-counting encoding used in Hyperkernel.

Download

Publications

  • Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. Hyperkernel: Push-Button Verification of an OS Kernel. In Proc. of the 26th SOSP, Oct 2017. [pdf] [slides]

  • Dylan Johnson. Porting Hyperkernel to the ARM Architecture. Technical Report UW-CSE-17-08-02, University of Washington, Aug 2017. [pdf]