See recent updates and contact information at: https://unsat.cs.washington.edu/projects/hyperkernel/
This is a playground with kernel designs and ideas for formal verification. Don't use it for production.
How to run hv6
We have tested running hv6 with the following setup:
- Linux Ubuntu 17.10
- Binutils 2.29.1
- GCC 7.2.0
- QEMU 2.10.1
Install these packages before proceeding. Other platforms or versions may not work.
To run in QEMU:
Try a few commands in shell:
ls ps pstree readylist wttr
By default a web server starts on boot. Point your browser to http://localhost:10080/sh.html.
To run on real hardware, make sure your machine has VT-x (VMX) and VT-d (IOMMU) support and compatible devices (for E1000 we tested using Intel I217-LM). To get an ISO:
You can use it for PXE booting or creating a bootable USB.
How to verify hv6
We have tested verification with the following setup:
- Linux Ubuntu 17.10
- LLVM 5.0.0
- Z3 4.5.0
- Python 2.7.10
Runs the verification scripts for the hv6 kernel. This includes building the kernel
into LLVM IR, translating the kernel to Python using Irpy, and invoking
Individual tests can be run, for example, to run just the
sys_set_runnable test, invoke:
make hv6-verify -- -v --failfast HV6.test_sys_set_runnable
Runs the Irpy test suite, which compares symbolic execution results to running the C code
The proof guarantees that the system call handlers are a refinement
of our state-machine specification in
hv6/spec/. It also shows
that the state-machine specification satisfies certain high-level
properties, such as process isolation or the correctness of reference
This does not mean that the kernel is guaranteed to have zero bugs.
There can be bugs in unverified code (e.g., initialization and glue
code), the specification (or things not modeled in the specification),
or the verification toolchain including
irpy/ and Z3.
The current verification time is roughly 30 min on our test machine (quad-core i7-7700K). This is longer than the number reported in the paper, as we have added more lemmas since then, and several lemmas are unnecessarily proved more than once (the verifier is not smart enough to cache the results).
Contains the implementation of the hv6 kernel
Contains the specification for the hv6 kernel
Contains the implementation of the IR -> Python compiler used for
Contains the Python library and resources for performing symbolic
execution over Python generated by the Irpy compiler
A few quick pointers:
- state-machine specification:
- declarative specification:
- kernel configuration:
Code borrowed from other sources keeps the original copyright and license.
Files we created are licensed under the Apache License, Version 2.0, viewable at http://www.apache.org/licenses/LICENSE-2.0, and are marked as such.
In the copyright notices where we refer to "Hyperkernel Authors", we mean Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang.
hv6 borrows code from the following sources:
xv6: many of the source files in the hv6/ directory
lwIP: files under hv6/user/lwip/ (and user/lwip/)
ISOLINUX: binaries under boot/isolinux/
Linux binaries statically linked with uClibc
- Dune's bench: hv6/user/linux/bench_linux
- sparse's compile: hv6/user/linux/compile
- gzip: hv6/user/linux/gzip
- lua (patched with Linenoise): hv6/user/linux/lua
- sha1sum: hv6/user/linux/sha1sum
- tcc: hv6/user/linux/tcc
Terminus font: hv6/user/linux/ter-x16n.psf
- D3.js: web/d3.v4.min.js
- jQuery: web/jquery.min.js