Artifact for the CAV 2018 Paper: Symbolic Liveness Analysis of Real-World Software

Abstract

Liveness violation bugs are notoriously hard to detect, especially due to the difficulty inherent in applying formal methods to real-world programs. We present a generic and practically useful liveness property which defines a program as being live as long as it will eventually either consume more input or terminate. We show that this property naturally maps to many different kinds of real-world programs.

To demonstrate the usefulness of our liveness property, we also present an algorithm that can be efficiently implemented to dynamically find lassos in the target program’s state space during Symbolic Execution. This extends Symbolic Execution, a well known dynamic testing technique, to find a new class of program defects, namely liveness violations, while only incurring a small runtime and memory overhead, as evidenced by our evaluation. The implementation of our method found a total of five previously undiscovered software defects in BusyBox and the GNU Coreutils. All five defects have been confirmed and fixed by the respective maintainers after shipping for years, most of them well over a decade.

Artifact

To get started, import the VM and increase its memory allowance as high as reasonable on your system before booting the VM. You can find all our artifact files in /home/cav/Desktop/Evaluation/ (a directory placed on the desktop), including our documentation, which is named README.pdf (alternatively available as README.md markdown document). The documentation is also linked from the desktop.

Additional information about the VM image is available in the accompanying text document (cav18-SymbolicLivenessAnalysis.txt).

Project Repository

https://github.com/COMSYS/SymbolicLivenessAnalysis