Repository files navigation

See recent updates and contact information at:https://unsat.cs.washington.edu/projects/hyperkernel/

This is a playground with kernel designs and ideas for formalverification. Don't use it for production.

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 orversions may not work.

To compile:

make

To run in QEMU:

make qemu

Try a few commands in shell:

lspspstreereadylistwttr

By default a web server starts on boot. Point your browser tohttp://localhost:10080/sh.html.

To run on real hardware, make sure your machine has VT-x (VMX) andVT-d (IOMMU) support and compatible devices (for E1000 we testedusing Intel I217-LM). To get an ISO:

make iso

You can use it for PXE booting or creating a bootable USB.

We have tested verification with the following setup:

• Linux Ubuntu 17.10
• LLVM 5.0.0
• Z3 4.5.0
• Python 2.7.10

make hv6-verify:Runs the verification scripts for the hv6 kernel. This includes building the kernelinto LLVM IR, translating the kernel to Python using Irpy, and invokinghv6/spec/main.py.Individual tests can be run, for example, to run just thesys_set_runnable test, invoke:make hv6-verify -- -v --failfast HV6.test_sys_set_runnable

make irpy/test:Runs the Irpy test suite, which compares symbolic execution results to running the C codedirectly.

The proof guarantees that the system call handlers are a refinementof our state-machine specification inhv6/spec/. It also showsthat the state-machine specification satisfies certain high-levelproperties, such as process isolation or the correctness of referencecounters.

This does not mean that the kernel is guaranteed to have zero bugs.There can be bugs in unverified code (e.g., initialization and gluecode), the specification (or things not modeled in the specification),or the verification toolchain includingirpy/ 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 inthe paper, as we have added more lemmas since then, and severallemmas are unnecessarily proved more than once (the verifier is notsmart enough to cache the results).

hv6/:Contains the implementation of the hv6 kernel

hv6/spec/:Contains the specification for the hv6 kernel

irpy/compiler/:Contains the implementation of the IR -> Python compiler used forsymbolic execution

irpy/libirpy/:Contains the Python library and resources for performing symbolicexecution over Python generated by the Irpy compiler

A few quick pointers:

• syscalls:hv6/syscall.c
• state-machine specification:hv6/spec/kernel/spec/specs.py
• declarative specification:hv6/spec/kernel/spec/top.py
• kernel configuration:kernel/config.h

Code borrowed from other sources keeps the original copyright and license.

Files we created are licensed under the Apache License, Version 2.0,viewable athttp://www.apache.org/licenses/LICENSE-2.0, and aremarked 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

• sv6

  • hv6/user/ns.c
  • kernel/tsc.c

• FreeBSD

  • include/uapi/assym.h
  • kernel/intel_iommu.c
  • kernel/intel_iommu.h
  • kernel/svm.c
  • kernel/svm.h
  • kernel/vmx.c
  • kernel/vmx.h
  • lib/stdlib.c
  • lib/string.c
  • scripts/genassym.sh

• Linux

  • include/uapi/machine/trap_support.h

• NetBSD

  • hv6/user/fs/nvmedisk.c
  • include/uapi/nvme.h
  • include/uapi/pcireg.h
  • include/uapi/queue.h

• QEMU

  • include/uapi/e1000.h

• 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

• JavaScript libraries

  • D3.js: web/d3.v4.min.js
  • jQuery: web/jquery.min.js