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 manually-provided program specifications. Fortunately, the verification of shal-low safety properties such as memory isolation and control-flow safety can be easier to automate, but past techniques for automatically verify-ing machine-code safety have required post-compilation transformations, which can change program behavior. In this work, we automatically ver-ify safety properties for unmodified machine-code programs without re-quiring user-supplied specifications. Our novel logic framework, AUS-PICE, for automatic safety property verification for unmodified executa-bles, 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 hours for a realistic 533-instruction string search algorithm, demonstrating the feasibility of our approach.