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 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
In Hoare logic, p, q are named pre-, post-condition, but we use the terms pre-, post-state as we call the boolean conditions imposed by a branch the pre-condition.
References
The ARM-THUMB Procedure Call Standard (2000). http://infocenter.arm.com/help/topic/com.arm.doc.espc0002/ATPCS.pdf
ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition (2014)
Abadi, M., Budiu, M., Erlingsson, U., Ligatti, J.: Control-flow Integrity. In: ACM CCS (2005)
Blackham, B., Heiser, G.: Sequel: a framework for model checking binaries. In: IEEE RTAS (2013)
Chipounov, V., Candea, G.: Enabling sophisticated analyses of x86 binaries with RevGen. In: HotDep (2011)
Chlipala, A.: Mostly-automated verification of low-level programs in computational separation logic. In: PLDI (2011)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL (1977)
Erlingsson, U., Abadi, M., Vrable, M., Budiu, M., Necula, G.: XFI: software guards for system address spaces. In: OSDI (2006)
Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol. 2758, pp. 25–40. Springer, Heidelberg (2003)
Guthaus, M.R., Ringenberg, J.S., Ernst, D., Austin, T.M., Mudge, T., Brown, R.B.: Mibench: a free, commercially representative embedded benchmark suite. In: IEEE WWC Workshop (2001)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576–580 (1969)
McCamant, S., Morrisett, G.: Evaluating SFI for a CISC architecture. In: USENIX Security (2006)
Morrisett, G., Crary, K., Glew, N., Grossman, D., Samuels, R., Smith, F., Walker, D., Weirich, S., Zdancewic, S.: TALx86: a realistic typed assembly language. In: Workshop on Compiler Support for System Software (WCSSS) (1999)
Morrisett, G., Tan, G., Tassarotti, J., Tristan, J., Gan, E.: RockSalt: better, faster, stronger SFI for the x86. In: PLDI (2012)
Myreen, M.O., Fox, A.C.J., Gordon, M.J.C.: Hoare logic for ARM machine code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272–286. Springer, Heidelberg (2007)
Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 568–582. Springer, Heidelberg (2007)
Myreen, M., Gordon, M., Slind, K.: Machine-code verification for multiple architectures: an application of decompilation into logic. In: FMCAD (2008)
Ni, Z., Shao, Z.: Certified assembly programming with embedded code pointers. In: POPL (2006)
Reynolds, J.: Separation logic: a logic for shared mutable data structures. In: IEEE LICS (2002)
Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28–32. Springer, Heidelberg (2008)
Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80–94. Springer, Heidelberg (2006)
Tate, R., Chen, J., Hawblitzel, C.: Inferable object-oriented typed assembly language. In: PLDI (2010)
Thakur, A., Lim, J., Lal, A., Burton, A., Driscoll, E., Elder, M., Andersen, T., Reps, T.: Directed proof generation for machine code. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 288–305. Springer, Heidelberg (2010)
Wahbe, R., Lucco, S., Anderson, T., Graham, S.: Efficient software-based fault isolation. In: SOSP (1993)
Xu, Z., Miller, B., Reps, T.: Safety checking of machine code. In: PLDI (2000)
Yu, D., Hamid, N.A., Shao, Z.: Building certified libraries for PCC: dynamic storage allocation. In: Degano, P. (ed.) ESOP 2003. LNCS, vol. 2618, pp. 363–379. Springer, Heidelberg (2003)
Zhao, L., Li, G., Sutter, B.D., Regehr, J.: ARMor: fully verified software fault isolation. In: EMSOFT (2011)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P. (2016). AUSPICE: Automatic Safety Property Verification for Unmodified Executables. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-29613-5_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29612-8
Online ISBN: 978-3-319-29613-5
eBook Packages: Computer ScienceComputer Science (R0)