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

• GitHub repository

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]