Abstract
This paper presents a mechanised Hoare-style programming logic framework for assembly level programs. The framework has been designed to fit on top of operational semantics of realistically modelled machine code. Many ad hoc restrictions and features present in real machine-code are handled, including finite memory, data and code in the same memory space, the behavior of status registers and hazards of corrupting special purpose registers (e.g. the program counter, procedure return register and stack pointer). Despite accurately modeling such low level details, the approach yields concise specifications for machine-code programs without using common simplifying assumptions (like an unbounded state space). The framework is based on a flexible state representation in which functional and resource usage specifications are written in a style inspired by separation logic. The presented work has been formalised in higher-order logic, mechanised in the HOL4 system and is currently being used to verify ARM machine-code implementations of arithmetic and cryptographic operations.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Appel, A.W.: Foundational proof-carrying code. In: Proc. 16th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, Los Alamitos (2001)
Arbib, M.A., Alagic, S.: Proof rules for gotos. Acta Informatica 11, 139–148 (1979)
Bevier, W.R.: A verified operating system kernel. PhD thesis, University of Texas at Austin (1987)
Boyer, R.S., Yu, Y.: Automated proofs of object code for a widely used microprocessor. J. ACM 43(1), 166–192 (1996), doi.acm.org/10.1145/227595.227603
Clutterbuck, D.L.: The verification of low-level code. Software Engineering Journal 3, 97–111 (1988)
The HOL4 System (Description), http://hol.sourceforge.net/documentation.html
Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Manolios, P., Wilding, M. (eds.) Sixth International Workshop on the ACL2 Theorem Prover and Its Applications (2006)
Klein, G., Tuch, H., Norrish, M.: Types, bytes, and separation logic. To appear in: Hofmann, M., Felleisen, M. (eds.) Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL) (2007)
Maurer, W.D.: Proving the correctness of a flight-director program for an airborne minicomputer. In: Proceedings of the ACM SIGMINI/SIGPLAN interface meeting on Programming systems in the small processor environment, ACM Press, New York (1976), doi.acm.org/10.1145/800236.807101
Fox, A.C.J., Gordon, M.J.C., Myreen, M.O.: Hoare Logic for ARM Machine Code. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 272–286. Springer, Heidelberg (2007)
Necula, G.C.: Proof-carrying code. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), ACM Press, New York (1997), http://doi.acm.org/10.1145/263699.263712
Yang, H., O’Hearn, P.W., Reynolds, J.C.: Local Reasoning about Programs that Alter Data Structures. In: Fribourg, L. (ed.) CSL 2001 and EACSL 2001. LNCS, vol. 2142, Springer, Heidelberg (2001)
Reynolds, J.: Separation logic: A logic for shared mutable data structures. In: Proceedings of 17th IEEE Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press, Los Alamitos (2002), citeseer.ist.psu.edu/reynolds02separation.html
Saabas, A., Uustalu, T.: A compositional natural semantics and hoare logic for low-level languages. Electronic Notes in Theoretical Computer Science 156(1), 151–168 (2006)
Seal, D.: ARM Architecture Reference Manual. Addison-Wesley, Reading (2000)
Tan, G., Appel, A.W.: A compositional logic for control flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Myreen, M.O., Gordon, M.J.C. (2007). Hoare Logic for Realistically Modelled Machine Code. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_44
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_44
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)