This repository contains the code and experiments for the SOSP'19 paper Scaling symbolic evaluation for automated verification of systems code with Serval.
Serval is a tool for building automated verifiers for systems code.
This file describes the high-level structure of the code,
see EXPERIMENTS.md for details on how to run the experiments yourself.
serval/: The source of the Serval verification package.
serval/serval/lib/: Core Serval functionality, including
memory model and unit testing libraries.
serval/serval/riscv/: Verifier for RISC-V programs,
including objdump parser, instruction encoder, and symbolic
interpreter.
serval/serval/x32/: Verifier for i386 programs.
serval/serval/spec/: Library for writing system specifications.
serval/serval/llvm.rkt: Verifier for LLVM programs.
serval/serval/doc: API reference documentation
monitors/: Implementation and specifications
of security monitors.
monitors/*/verif/: Specifications and verification infrastructure
for security monitors.
monitors/komodo/: Our port of Komodo.
monitors/certikos/: Our port of CertiKOS.
monitors/keystone/: Our port of Keystone.
monitors/toymon/: A toy security monitor for testing.
kernel/: Common kernel functionality.
bios/: M-mode boot code.
include/: Kernel / security monitor headers.
bpf/jit/riscv64.rkt: Linux BPF to RV64 JIT.
bpf/jit/x32.rkt: Linux BPF to i386 JIT.
racket/test/: Code for testing Serval functionality.
racket/llvm-rosette/: Utility for compiling LLVM IR to
Racket structures.
Code in this repository is licensed under the GPLv2 license, found in the LICENSE file.
Some code in kernel/, bpf/ and include/ is adapted from the Linux kernel.
monitors/komodo/monitor.c is based on the original Komodo implementation.
racket/test/riscv-tests is adapted from the RISC-V test suite.