Serval is a framework for developing automated verifiers for systems software. It is based on three key strategies: lifting interpreters into verifiers under symbolic evaluation, employing symbolic profiling to identify verification performance bottlenecks, and performing symbolic optimizations to produce solver-friendly constraints. Using Serval, we build automated verifiers for RISC-V, LLVM IR, BPF, and x86-32. Below are a few results of applying the Serval verifiers.
- Linux kernel’s BPF JIT
- Keystone: #19, #20
- RISC-V ports of CertiKOS and Komodo (coming soon)
Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Serval: scaling symbolic evaluation for automated verification of systems code. In Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP), Oct 2019.