AUSPICE: Automatic safety property verification for unmodified executables

Abstract

Verification of machine-code programs using program logic has focused on functional correctness, and proofs have required manuallyprovided program specifications. Fortunately, the verification of shallow safety properties such as memory isolation 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. Our novel logic framework, AUSPICE, for automatic safety property verification for unmodified executables, extends an existing trustworthy Hoare logic for local reasoning, and provides a novel proof tactic for selective composition. We demonstrate our automated proof technique on synthetic and realistic programs. Our verification completes in 6 h for a realistic 533-instruction string search algorithm, demonstrating the feasibility of our approach.