Abstract
We present a methodology for generating a characterization of the memory used by an assembly program, as well as a formal proof that the assembly is bounded to the generated memory regions. A formal proof of memory usage is required for compositional reasoning over assembly programs. Moreover, it can be used to prove low-level security properties, such as integrity of the return address of a function. Our verification method is based on interactive theorem proving, but provides automation by generating pre- and postconditions, invariants, control-flow, and assumptions on memory layout. As a case study, three binaries of the Xen hypervisor are disassembled. These binaries are the result of a complex build-chain compiling production code, and contain various complex and nested loops, large and compound data structures, and functions with over 100 basic blocks. The methodology has been successfully applied to 251 functions, covering 12,252 assembly instructions.
Chapter PDF
Similar content being viewed by others
References
Barrett, C., Berezin, S.: CVC Lite: A new implementation of the cooperating validity checker. In: International Conference on Computer Aided Verification. pp. 515–518. Springer (2004)
Barrett, C., Tinelli, C.: CVC3. In: International Conference on Computer Aided Verification. pp. 298–302. Springer (2007)
Baumann, C., Näslund, M., Gehrmann, C., Schwarz, O., Thorsen, H.: A high assurance virtualization platform for armv8. In: 2016 European Conference on Networks and Communications (EuCNC). pp. 210–214. IEEE (2016)
Bevier, W.R.: Kit and the short stack. Journal of Automated Reasoning 5(4), 519–530 (1989)
Bevier, W.R., Hunt, W.A., Moore, J.S., Young, W.D.: An approach to systems verification. Journal of Automated Reasoning 5(4), 411–428 (Dec1989). 10.1007/BF00243131
Bockenek, J.A., Verbeek, F., Lammich, P., Ravindran, B.: Formal verification of memory preservation of x86-64 binaries (Sep 2019)
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, Inc. (1979)
Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. Journal of the ACM 43(1), 166–192 (1996)
Brumley, D., Jager, I., Avgerinos, T., Schwartz, E.J.: BAP: A binary analysis platform. In: Gopalakrishnan, G., Qadeer, S. (eds.) International Conference on Computer Aided Verification. pp. 463–469. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). 10.1007/978-3-642-22110-1_37
Calcagno, C., Distefano, D.: Infer: An automatic program verifier for memory safety of C programs. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NASA Formal Methods. pp. 459–465. Springer Berlin Heidelberg, Berlin, Heidelberg (2011). 10.1007/978-3-642-20398-5_33, https://fbinfer.com/
Calcagno, C., Distefano, D., O’Hearn, P., Yang, H.: Compositional shape analysis by means of bi-abduction. In: Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 289–300. POPL ’09 (2009)
Carré, B.A., O’Neill, I.M., Clutterbuck, D.L., Debney, C.W.: SPADE—the southampton program analysis and development environment. In: Software Engineering Environments. Peter Peregrinus, Ltd., Stevenage (1986)
Chisnall, D.: The Definitive Guide to the Xen Hypervisor. Pearson Education (2008)
Clutterbuck, D.L., Carré, B.A.: The verification of low-level code. SoftwareEngineering Journal 3(3), 97–111 (May 1988). 10.1049/sej.1988.0012
Cowan, C., Pu, C., Maier, D., Walpole, J., Bakke, P., Beattie, S., Grier, A., Wagle, P., Zhang, Q., Hinton, H.: Stackguard: Automatic adaptive detection and prevention of buffer-overflow attacks. In: USENIX Security Symposium. vol. 98, pp. 63–78. San Antonio, TX (1998)
Dam, M., Guanciale, R., Nemati, H.: Machine code verification of a tiny ARM hypervisor. In: Proceedings of the 3rd International Workshop on Trustworthy Embedded Devices. pp. 3–12. TrustED ’13, ACM Press, New York, NY, USA (2013). 10.1145/2517300.2517302
Dawson, J., Graunke, P., Huffman, B., Klein, G., Matthews, J.: Machine words in Isabelle/HOL (Aug 2018)
Evans, D., Larochelle, D.: Improving security using extensible lightweight static analysis. IEEE Software 19(1), 42–51 (Jan 2002). 10.1109/52.976940
Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. Tech. Rep. YALEU/DCS/TR-1336, Dept. of Computer Science, Yale University, New Haven, CT (Nov 2005), http://flint.cs.yale.edu/publications/sbca.html
Feng, X., Shao, Z., Vaynberg, A., Xiang, S., Ni, Z.: Modular verification of assembly code with stack-based control abstractions. In: Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. PLDI’06, vol. 41, pp. 401–414. ACM Press, New York, NY, USA (Jun 2006)
Floyd, R.W.: Assigning meanings to programs. Mathematical Aspects of Computer Science 19(1), 19–32 (1967)
Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving. pp. 243–258. Springer Berlin Heidelberg, Berlin, Heidelberg (2010). 10.1007/978-3-642-14052-5_18
Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Damm, W., Hermanns, H. (eds.) Computer Aided Verification. pp. 519–531. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). /10.1007/978-3-540-73368-3_52
Goel, S.: Formal Verification of Application and System Programs Based on a Validated x86 ISA Model. Ph.D. thesis (2016), http://hdl.handle.net/2152/46437
Goel, S., Hunt, W.A., Kaufmann, M., Ghosh, S.: Simulation and formal verification of x86 machine-code programs that make system calls. In: 2014 Formal Methods in Computer-Aided Design (FMCAD). pp. 91–98 (Oct 2014). 10.1109/FMCAD.2014.6987600
Greenaway, D., Andronick, J., Klein, G.: Bridging the gap: Automatic verified abstraction of C. In: Beringer, L., Felty, A. (eds.) International Conference on Interactive Theorem Proving. pp. 99–115. ITP 2012, Springer-Verlag, Berlin, Heidelberg (Aug 2012)
Heule, S., Schkufza, E., Sharma, R., Aiken, A.: Stratified synthesis: Automatically learning the x86–64 instruction set. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 237–250. PLDI ’16, ACM, New York, NY, USA (2016)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (Oct 1969)
Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (Aug 1978). 10.1145/359576.359585
Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39(12),92–106 (Dec 2004). 10.1145/1052883.1052895, http://findbugs.sourceforge.net/
Klein, G., Andronick, J., Elphinstone, K., Murray, T., Sewell, T., Kolanski, R., Heiser, G.: Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems 32(1), 2:1–2:70 (Feb 2014). 10.1145/256053710.1145/2560537
Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles. pp. 207–220. ACM (2009)
Krebbers, R., Jung, R., Bizjak, A., Jourdan, J.H., Dreyer, D., Birkedal, L.: The essence of higher-order concurrent separation logic. In: European Symposium on Programming. pp. 696–723. Springer (2017)
Kruegel, C., Kirda, E., Mutz, D., Robertson, W., Vigna, G.: Automating mimicry attacks using static binary analysis. In: USENIX Security Symposium. vol. 14, pp. 11–11 (2005)
Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: A verified implementation of ML. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 179–191. POPL ’14, ACM, New York, NY, USA (2014), https://cakeml.org/
Leroy, X., Blazy, S., Kästner, D., Schommer, B., Pister, M., Ferdinand, C.: CompCert - a formally verified optimizing compiler. In: Embedded Real Time Software and Systems, 8th European Congress. ERTS 2016, SEE, HAL, Toulouse, France (Jan 2016), https://hal.inria.fr/hal-01238879
Matichuk, D., Murray, T., Wenzel, M.: Eisbach: A proof method language for Isabelle. Journal of Automated Reasoning 56(3), 261–282 (2016)
Matthews, J., Moore, J.S., Ray, S., Vroon, D.: Verification condition generation via theorem proving. In: International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. pp. 362–376. Springer-Verlag (2006)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: International conference on Tools and Algorithms for the Construction and Analysis of Systems. pp. 337–340. Springer-Verlag (2008)
Myreen, M.O., Gordon, M.J.C.: Hoare logic for realistically modelled machine code. In: Grumberg, O., Huth, M. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 568–582. Springer-Verlag, Berlin, Heidelberg (2007)
Myreen, M.O., Gordon, M.J.C., Slind, K.: Machine-code verification for multiple architectures—an application of decompilation into logic. In: 2008 Formal Methods in Computer-Aided Design. pp. 1–8. IEEE (Nov 2008)
Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic–improved. In: 2012 Formal Methods in Computer-Aided Design (FMCAD). pp. 78–81. IEEE (2012)
Necula, G.C.: Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 106–119. ACM (1997)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic, vol. 2283. Springer Science & Business Media (2002)
O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: International Workshop on Computer Science Logic. pp. 1–19. Springer (2001)
Quynh, N.A.: Capstone: Next-gen disassembly framework (Aug 2014), http://www.capstone-engine.org/, accessed June 27, 2019
Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Proceedings 17th Annual IEEE Symposium on Logic in Computer Science. pp. 55–74. IEEE (2002)
Rice, H.G.: Classes of recursively enumerable sets and their decision problems. Transactions of the American Mathematical Society 74(2), 358–366 (1953)
Roessle, I., Verbeek, F., Ravindran, B.: Formally verified big step semantics out of x86-64 binaries. In: Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs. pp. 181–195. CPP 2019, ACM, New York, NY, USA (2019)
Rushby, J.: Noninterference, Transitivity, and Channel-Control Security Policies. SRI International, Computer Science Laboratory (1992)
Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation. pp. 471–482. PLDI ’13, ACM, New York, NY, USA (2013)
Shi, J., He, J., Zhu, H., Fang, H., Huang, Y., Zhang, X.: ORIENTAIS: Formal verified OSEK/VDX real-time operating system. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 293–301 (Jul 2012)
Shi, J., Zhu, L., Fang, H., Guo, J., Zhu, H., Ye, X.: xBIL – a hardware resource oriented binary intermediate language. In: 2012 IEEE 17th International Conference on Engineering of Complex Computer Systems. pp. 211–219 (Jul 2012)
Slind, K., Norrish, M.: A brief overview of HOL4. In: International Conference on Theorem Proving in Higher Order Logics. pp. 28–32. Springer (2008)
Song, D., Brumley, D., Yin, H., Caballero, J., Jager, I., Kang, M.G., Liang, Z., Newsome, J., Poosankam, P., Saxena, P.: BitBlaze: A new approach to computer security via binary analysis. In: Proceedings of the 4th International Conference on Information Systems Security. Keynote invited paper. Hyderabad, India (Dec 2008)
Tan, J., Tay, H.J., Gandhi, R., Narasimhan, P.: Auspice: Automatic safety property verification for unmodified executables. In: VSSTE. pp. 202–222. Springer (2015)
Verbeek, F., Bockenek, J.A., Ravindran, B.: Artifact – Highly automated formal proofs over memory usage of assembly code (2020). 10.5281/zenodo.3676687
Wang, F., Shoshitaishvili, Y.: Angr – the next generation of binary analysis. In: 2017 IEEE Cybersecurity Development (SecDev). pp. 8–9. IEEE (2017)
Wenzel, M.: Isabelle/Isar—a generic framework for human-readable proof documents. From Insight to Proof—Festschrift in Honour of Andrzej Trybulec 10(23), 277–298 (2007)
Yu, Y.: Automated Proofs of Object Code for a Widely Used Microprocessor. Ph.D. thesis, University of Texas at Austin (1992)
Zhang, M., Sekar, R.: Control flow integrity for COTS binaries. In: Presented as part of the 22nd USENIX Security Symposium (USENIX Security 13). pp. 337–352 (2013)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2020 The Author(s)
About this paper
Cite this paper
Verbeek, F., Bockenek, J.A., Ravindran, B. (2020). Highly Automated Formal Proofs over Memory Usage of Assembly Code. In: Biere, A., Parker, D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2020. Lecture Notes in Computer Science(), vol 12079. Springer, Cham. https://doi.org/10.1007/978-3-030-45237-7_6
Download citation
DOI: https://doi.org/10.1007/978-3-030-45237-7_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-45236-0
Online ISBN: 978-3-030-45237-7
eBook Packages: Computer ScienceComputer Science (R0)