Scaling symbolic evaluation for automated verification of systems code with Serval

Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, Xi Wang
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 15 October 2019

Proceedings of the 27th ACM Symposium on Operating Systems Principles (SOSP)
Topic(s): os security tools verification
Note(s): operating systems, information flow, Rosette solver, LLVM compiler, RISCV architecture, symbolic evaluation, symbolic execution, binary analysis
Papers: nelson:sosp:2017, sigurbjarnarson:osdi:2016, sigurbjarnarson:osdi:2018, demoura:tacas:2008, torlak:pldi:2014

This paper continues the theme of “push-button automation” from the UNSAT group’s earlier work on Hyperkernel, Yggadrisil and Nickel. Like the earlier work, they are using the Z3 SMT solver to verify systems code automatically and they are avoiding adding annotations (“auto-active verification”) to help the verification by restricting the code they verify to “finite interfaces” so that all loops are bounded. The big difference is that the earlier works wrote specifications in Python using the Z3Py library whereas this paper uses Rosette’s symbolic execution support.

They demonstrate the approach by porting Komodo and CertiKOS to RISC-V, rewriting the specs in Serval and reverifying their functional correctness and security properties on the binaries. This process took an impressive 4 person-weeks each! In addition, they created partial specifications of Linux BPF and the Keystone TEE and found bugs both in the artifacts they were verifying and in processors and other RISC-V specs. (They also reveal that the CertiKOS verification excluded verification of the ELF loader. Interesting omission.)

The basic idea in Serval is to write an interpreter for an instruction set (eg RISC-V, BPF, …) and then lift this interpreter to create a symbolic execution engine (requires some annotations and performance tuning). This symbolic execution engine generates SMT that is fed to Z3. Serval includes libraries for specifying non-interference and state-machine refinement.

Serval is impressively small: 4400 lines for Serval + RISC-V (subset) + x86-32 (subset) + LLVM (subset) + BPF. That is tiny!

Auto active verification, Bounded model-checking, Non-interference, Rosette solver, Serval solver-based verifier, Symbolic evaluation, Symbolic execution

  • Komodo: Using verification to disentangle secure-enclave hardware from software [ferraiuolo:sosp:2017]
  • A lightweight symbolic virtual machine for solver-aided host languages [torlak:pldi:2014]