A Proof Infrastructure for Binary Programs
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.
KeywordsSecurity Property Subject Program Hoare Logic Binary Program Jump Instruction
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.
- 1.Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis, Bath (2012)Google Scholar
- 2.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)Google Scholar
- 4.Jager, I., Brumley, D.: Efficient directionless weakest preconditions (cmu-cylab-10-002). CyLab, p. 27 (2010)Google Scholar
- 6.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)Google Scholar