Abstract
Establishing properties of binary programs by proof is a desirable goal when the properties of interest are crucial, such as those that arise in safety- and security-critical applications. Practical development of proofs for binary programs requires a substantial infrastructure to disassemble the program, define the machine semantics, and actually undertake the required proofs. At the center of these infrastructure requirements is the need to document semantics in a formal language. In this paper we present a work-in-progress proof infrastructure for binary programs based on AdaCore and Altran’s integrated development and verification environment, SPARKPro. We illustrate the infrastructure with proof of a security property.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
The binary analyzer uses a combination of objdump and IDA Pro.
References
Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis, Bath (2012)
Erlingsson, U., Abadi, M., Vrable, M., Budiu, M., Necula, G.C.: XFI: software guards for system address spaces. In: Proceedings of the 7th Symposium on Operating Systems Design and Implementation, OSDI 2006, pp. 75–88. USENIX Association, Berkeley (2006)
Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 243–258. Springer, Heidelberg (2010)
Jager, I., Brumley, D.: Efficient directionless weakest preconditions (cmu-cylab-10-002). CyLab, p. 27 (2010)
Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: AUSPICE: automatic safety property verification for unmodified executables. In: Gurfinkel, A., et al. (eds.) VSTTE 2015. LNCS, vol. 9593, pp. 202–222. Springer, Heidelberg (2016). doi:10.1007/978-3-319-29613-5_12
Zhao, L., Li, G., De Sutter, B., Regehr, J.: ARMor: fully verified software fault isolation. In: Proceedings of the Ninth ACM International Conference on Embedded Software, EMSOFT 2011, pp. 289–298, NY. ACM, New York (2011)
Acknowledgments
This research was developed with funding from the Defense Advanced Research Projects Agency (DARPA) under contract W31P4Q–14-C–0086. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government. The authors thank the software engineers of AdaCore, in particular, Yannick Moy for providing support.
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
Hocking, A.B., Rodes, B.D., Knight, J.C., Davidson, J.W., Coleman, C.L. (2016). A Proof Infrastructure for Binary Programs. In: Rayadurgam, S., Tkachuk, O. (eds) NASA Formal Methods. NFM 2016. Lecture Notes in Computer Science(), vol 9690. Springer, Cham. https://doi.org/10.1007/978-3-319-40648-0_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-40648-0_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40647-3
Online ISBN: 978-3-319-40648-0
eBook Packages: Computer ScienceComputer Science (R0)