Name
Abstract | ||
|---|---|---|
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.
|
Year | DOI | Venue |
|---|---|---|
2019 | 10.1145/3341301.3359641 | Proceedings of the 27th ACM Symposium on Operating Systems Principles |
DocType | ISBN | Citations |
Conference | 978-1-4503-6873-5 | 2 |
PageRank | References | Authors |
0.37 | 0 | 6 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Luke Nelson | 1 | 2 | 1.39 |
| James Bornholt | 2 | 93 | 7.96 |
| Ronghui Gu | 3 | 64 | 7.82 |
| Andrew Baumann | 4 | 694 | 28.49 |
| Emina Torlak | 5 | 606 | 30.70 |
| Xi Wang | 6 | 540 | 29.04 |