Serval

Serval is 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, Arm, LLVM, and BPF instruction sets.

Applications

• Jitterbug for writing and verifying just-in-time compilers
• Keystone enclave framework: #19, #20
• SCFTL for verifying a snapshot-consistent flash translation layer

Download

• Serval development repository

• SOSP’19 artifact: it contains a snapshot of the version of Serval used to verify the security monitors, but is not actively developed.

Articles

• Scaling symbolic evaluation for automated verification of systems code with Serval, The Morning Paper, by Adrian Colyer.

Documentation

• SOSP’19 tutorial

Publications

• Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. Specification and verification in the field: Applying formal methods to BPF just-in-time compilers in the Linux kernel. In Proc. of the 14th OSDI, Nov 2020. [pdf] [slides]

• Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. Noninterference specifications for secure systems. ACM SIGOPS Operating Systems Review, 54(1), Aug 2020. [pdf]

• Luke Nelson and Xi Wang. Developing security monitors on RISC-V: Case studies on HiFive Unleashed. Technical Report UW-CSE-2019-11-01, University of Washington, Nov 2019. [pdf]

• Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. Scaling symbolic evaluation for automated verification of systems code with Serval. In Proc. of the 27th SOSP, Oct 2019. [pdf] [slides] Best paper award Distinguished artifact award