Computing Verified Machine Address Bounds During Symbolic Exploration of Code

• J Strother Moore
Chapter
Part of the NASA Monographs in Systems and Software Engineering book series (NASA)

Abstract

When operational semantics is used as the basis for mechanized verification of machine code programs it is often necessary for the theorem prover to determine whether one expression denoting a machine address is unequal to another. For example, this problem arises when trying to determine whether a read at the address given by expression a is affected by an earlier write at the address given by b. If it can be determined that a and b are definitely unequal, the write does not affect the read. Such address expressions are typically composed of “machine arithmetic function symbols” such as +, *, mod, ash, logand, logxor, etc., as well as numeric constants and values read from other addresses. In this chapter we present an abstract interpreter for machine address expressions that attempts to produce a bounded natural number interval guaranteed to contain the value of the expression. The interpreter has been proved correct by the ACL2 theorem prover and is one of several key technologies used to do fast symbolic execution of machine code programs with respect to a formal operational semantics. We discuss the interpreter, what has been proved about it by ACL2, and how it is used in symbolic reasoning about machine code.

Keywords

Function Symbol Machine Code Output Interval Common Lisp Abstract Interpreter
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Notes

Acknowledgements

I would especially like to thank Warren Hunt for his invaluable help during the development of Ainni. Warren developed the definitions and proved many of the basic rewrite rules for the byte addressed read and write functions, R, and !R. He also provided an ACL2 formalization of a realistic ISA and implemented the DES algorithm in ACL2. We then compiled the DES algorithm into the instructions of the ISA thus obtaining an interesting symbolic evaluation challenge for ACL2. I would also like to thank Matt Kaufmann, who gave me some strategic advice on lemma development to prove the correctness of one of the metafunctions here as well as his usual extraordinary efforts to maintain ACL2 while I pursue topics such as this one. This work was partially supported by ForrestHunt, Inc.

References

1. 1.
Bevier, W.R., Hunt Jr., W.A., Moore, J.S., Young, W.D.: Special issue on system verification. J. Autom. Reason. 5(4), 409–530 (1989)Google Scholar
2. 2.
Boyer, R.S., Moore, J.S.: A Computational Logic. Academic Press, New York (1979)
3. 3.
Boyer, R.S., Moore, J.S.: Metafunctions: Proving them correct and using them efficiently as new proof procedures. Technical Report CSL-108, SRI International (1979)Google Scholar
4. 4.
Boyer, R.S., Moore, J.S.: Metafunctions: Proving them correct and using them efficiently as new proof procedures. The Correctness Problem in Computer Science. Academic Press, London (1981)Google Scholar
5. 5.
Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, New York (1997)
6. 6.
Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166–192 (1996)
7. 7.
Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD’96). LNCS, vol. 1166, pp. 275–293. Springer, Heidelberg (1996). https://www.cs.utexas.edu/users/moore/publications/bkm96.pdf
8. 8.
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, pp. 238–252. ACM Press, New York (1977)Google Scholar
9. 9.
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min, A., Monniaux, D., Rival, X.: The astre analyser. In: Sagiv, M. (ed.) European Symposium on Programming (ESOP 2005). LNCS, vol. 3444, pp. 21–30. Springer, New York (2005)Google Scholar
10. 10.
Goel, S., Hunt, W.A., Kaufmann, M.: Simulation and formal verification of x86 machine-code programs that make system calls. In: Claessen, K., Kuncak, V. (eds.) FMCAD’14: Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design, pp. 91–98. EPFL, Switzerland (2014)Google Scholar
11. 11.
Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Press, Boston (2000)Google Scholar
12. 12.
Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Press, Boston (2000)Google Scholar
13. 13.
Kaufmann, M., Moore, J.S.: An industrial strength theorem prover for a logic based on common lisp. IEEE Trans. Softw. Eng. 23(4), 203–213 (1997)
14. 14.
Kaufmann, M., Moore, J.S.: The ACL2 home page. Department of Computer Sciences, University of Texas at Austin (2014). http://www.cs.utexas.edu/users/moore/acl2/
15. 15.
Kaufmann, M., Moore, J.S.: Well-formedness guarantees for ACL2 metafunctions and clause processors. In: Design and Implementation of Formal Tools and Systems (DIFTS) (2015)Google Scholar
16. 16.
Liu, H., Moore, J.S.: Java program verification via a JVM deep embedding in ACL2. In: Slind, K., Bunker, A., Gopalakrishnan, G. (eds.) 17th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2004. Lecture Notes in Computer Science, vol. 3223, pp. 184–200. Springer, New York (2004)
17. 17.
Moore, J.S., Martinez, M.: A mechanically checked proof of the correctness of the Boyer-Moore fast string searching algorithm. In: Engineering Methods and Tools for Software Safety and Security (Proceedings of the Martoberdorf Summer School, 2008), pp. 267–284. IOS Press (2009)Google Scholar
18. 18.
Slobodova, A., Davis, J., Swords, S., Hunt Jr., W.: A flexible formal verification framework for industrial scale validation. In: Singh, S. (ed.) 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 89–97. IEEE (2011)Google Scholar
19. 19.
Steele Jr., G.L.: Common Lisp The Language, 2nd edn, p. 01803. Digital Press, Burlington (1990)
20. 20.
Toibazarov, E.: An ACL2 proof of the correctness of the preprocessing for a variant of the Boyer-Moore fast string searching algorithm. Honors thesis, Computer Science Dept., University of Texas at Austin (2013). See www.cs.utexas.edu/users/moore/publications/toibazarov-thesis.pdf
21. 21.
Wilding, M.: A mechanically verified application for a mechanically verified environment. In: Courcoubetis, C. (ed.) Computer-Aided Verification – CAV ’93. Lecture Notes in Computer Science, vol. 697. Springer, Heidelberg (1993)Google Scholar