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!