S2W: Verification with Small and Short Worlds

FMCAD 2012 paper

This paper will appear in proceedings of 2012 Formal Methods in Computer-Aided Design (FMCAD) Conference.
The conference will be held in October, 2012 in Cambridge, UK.

Abstract
We consider the verification of safety properties in systems with large arrays and data structures. Such systems are common at the low levels of software stacks; examples are hypervisors and CPU emulators. The very large data structures in such systems (e.g., address-translation tables and other caches) make automated verification based on straightforward state-space exploration infeasible. We present \sysname, a new abstraction-based model-checking methodology to facilitate automated verification of such systems. As a first step, inductive invariant checking is performed. If that fails, we compute an abstraction of the original system by precisely modeling only a subset of state variables while allowing the rest of the state to evolve arbitrarily at each step. This subset of the state constitutes a ``small world’’ hypothesis, and is extracted from the property. Finally, we verify the safety property on the abstract model using bounded model checking. We ensure the verification is sound by first computing a bound on the reachability diameter of the abstract model. For this computation, we developed a set of heuristics that we term the ``short world’’ approach. We present several case studies, including verification of the address translation logic in the Bochs x86 emulator, and verification of security properties of several hypervisor models.

pdf

UCLID Models

We used the following UCLID models as case studies for the S2W approach.
These case studies are described in the FMCAD 2012 paper.
You can download all models together in this tarball: tar

Toy Example

- One step induction: toy_example.ucl
- Small World Abstraction: toy_example_abst_module.ucl
- Subsequence heuristic check: toy_example_abst_subsequence_ctrl.ucl
- BMC check: toy_example_abst_bmc_ctrl.ucl
- Gadget Generation: toy_example_abst_gadgetgeneration_ctrl.ucl
- Short World Check (using gadgets): toy_example_abst_gadgettest.ucl

Bochs TLB + Paging

- One step induction: bochs.ucl
- Small World Abstraction: bochs_abst_module.ucl
- Short World Check (using subsequence heuristic): bochs_abst_shortworld.ucl
- BMC check: bochs_abst_bmc.ucl

Content Addressable Memory

- One step induction: cam_induction.ucl
- Small World Abstraction: cam_abst_module.ucl
- Short World Check (using subsequence heuristic): cam_abst_shortworld.ucl
- BMC check: cam_abst_bmc.ucl

Shadow Page Table

- One step induction: spt.ucl
- Short World Check (using gadgets): spt_abst_gadgettest.ucl
- BMC check: spt_abst_bmc.ucl

SecVisor

- One step induction: secvisor_induction.ucl

sHype

- One step induction: shype_induction.ucl