In 7th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), July 2015.
Jiaqi Tan, Hui Jun Tay, Rajeev Gandhi, Priya Narasimhan
Dept. Electrical & Computer Engineering
Carnegie Mellon University
Pittsburgh, PA 15213
Verification of machine-code programs using program logic has focused on functional correctness, and proofs have required manually-provided program specifications. Fortunately, the verification of shallow safety properties such as memory and control-flow safety can be easier to automate, but past techniques for automatically verifying machine-code safety have required post-compilation transformations, which can change program behavior. In this work, we automatically verify safety properties for unmodified machine-code programs without requiring user-supplied specifications. We present our novel logic framework, AUSPICE, for automatic safety property verification for unmodified executables, which extends an existing trustworthy Hoare logic for local reasoning, and provides a novel proof tactic for selective composition. We demonstrate our fully automated proof technique on synthetic and realistic programs, and our verification completes in 6 hours for a realistic 533-instruction string search algorithm, demonstrating the feasibility of our approach.
FULL PAPER: pdf