Scaling symbolic evaluation for automated verification of systems code with Serval
Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019•dl.acm.org
This paper presents Serval, a framework for developing automated verifiers for systems
software. Serval provides an extensible infrastructure for creating verifiers by lifting
interpreters under symbolic evaluation, and a systematic approach to identifying and
repairing verification performance bottlenecks using symbolic profiling and optimizations.
Using Serval, we build automated verifiers for the RISC-V, x86--32, LLVM, and BPF
instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems …
software. Serval provides an extensible infrastructure for creating verifiers by lifting
interpreters under symbolic evaluation, and a systematic approach to identifying and
repairing verification performance bottlenecks using symbolic profiling and optimizations.
Using Serval, we build automated verifiers for the RISC-V, x86--32, LLVM, and BPF
instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems …
This paper presents Serval, a framework for developing automated verifiers for systems software. Serval provides an extensible infrastructure for creating verifiers by lifting interpreters under symbolic evaluation, and a systematic approach to identifying and repairing verification performance bottlenecks using symbolic profiling and optimizations.
Using Serval, we build automated verifiers for the RISC-V, x86--32, LLVM, and BPF instruction sets. We report our experience of retrofitting CertiKOS and Komodo, two systems previously verified using Coq and Dafny, respectively, for automated verification using Serval, and discuss trade-offs of different verification methodologies. In addition, we apply Serval to the Keystone security monitor and the BPF compilers in the Linux kernel, and uncover 18 new bugs through verification, all confirmed and fixed by developers.
ACM Digital Library