Review of Serval System Code Verification Paper

ReviewPLSE


Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Em- ina Torlak, and Xi Wang. 2019. Scaling symbolic evaluation for automated verification of systems code with Serval. In ACM SIGOPS 27th Symposium on Operating Systems Principles (SOSP ’19), October 27–30, 2019, Huntsville, ON, Canada. ACM, New York, NY, USA, 18 pages. https://doi.org/10.1145/3341301.3359641

To verify a system's correctness, the developers commonly have to write a spec of its intended behavior and make a proof. Writing such proof could be tedious and requires lots of time investment. The authors then introduce an extensible framework for conducting push-button verification, Serval, which leverages a few advantages of Rosette (hybrid approach using bounded model checking and symbolic execution). Here are how Serval overcomes three common issues with verifiers:

Serval provides a lot of utilities for verifier developer to use. For instance, state-machine refinement and noninterference properties are provided. With the help of symbolic profiler, the authors also identify a range of common optimizations for verifying low level system code:

Pros:

Question for authors