Abstract
It is customary to write performance-critical parts of arithmetic functions in assembly: this enables finely-tuned algorithms that use specialized processor instructions. However, such optimizations make formal verification of arithmetic functions technically challenging, mainly because of many bit-level manipulations of data. In this paper, we propose an approach for formal verification of arithmetic functions in assembly. It consists in the implementation in the Coq proof assistant of (1) a Hoare logic for assembly programs augmented with loops and (2) a certified translator to ready-to-run assembly with jumps. To properly handle formal verification of bit-level manipulations of data, we propose an original encoding of machine integers. For concreteness, we use the SmartMIPS assembly language, an extension of the MIPS instruction set for smartcards, and we explain the formal verification of an optimized implementation of the Montgomery multiplication, a de facto-standard for the implementation of many cryptosystems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–585 (1969)
Montgomery, P.L.: Modular multiplication without trial division. Mathematics of Computation 44(170), 519–521 (1985)
Various contributors. The Coq Proof assistant. http://coq.inria.fr
Koc, C.K., Acar, T., Kaliski Jr, B.S.: Analyzing and Comparing Montgomery Multiplication Algorithms. IEEE Micro 16(3), 23–26 (1996)
MIPS Technologies. MIPS32 4KS Processor Core Family Software User’s Manual MIPS Technologies, Inc., 1225 Charleston Road, Mountain View, CA 94043-1353
Reynolds, J.C.: Separation Logic: A Logic for Shared Mutable Data Structures. In: LICS 2002. 17th IEEE Symposium on Logic in Computer Science, pp. 55–74 (2002)
Hamid, N.A., Shao, Z., Trifonov, V., Monnier, S., Ni, Z.: A Syntactic Approach to Foundational Proof-Carrying Code. In: LICS 2002. 7th IEEE Symposium on Logic In Computer Science, pp. 89–100 (2002)
Yu, D., Hamid, N.A., Shao, Z.: Building Certified Libraries for PCC: Dynamic Storage Allocation. In: Degano, P. (ed.) ESOP 2003 and ETAPS 2003. LNCS, vol. 2618, pp. 363–379. Springer, Heidelberg (2003)
Hamid, N.A., Shao, Z.: Interfacing Hoare Logic and Type Systems for Foundational Proof-Carrying Code. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 118–135. Springer, Heidelberg (2004)
Weber, T.: Towards Mechanized Program Verification with Separation Logic. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol. 3210, Springer, Heidelberg (2004)
Babić, D., Musuvathi, M.: Modular Arithmetic Decision Procedure. Microsoft Research Technical Report. MSR-TR-2005-114
Saabas, A., Uustalu, T.: A Compositional Natural Semantics and Hoare Logic for Low-Level Languages. Electronic Notes in Theoretical Computer Science 156, 151–168 (2006)
Tan, G., Appel, A.W.: A Compositional Logic for Control Flow. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 80–94. Springer, Heidelberg (2005)
Leroy, X.: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant. In: POPL 2006. 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 42–65
Chlipala, A.J.: Modular development of certified program verifiers with a proof assistant. In: ICFP 2006. 11th ACM SIGPLAN International Conference on Functional Programming, pp. 160–171 (2006)
Marti, N., Affeldt, R., Yonezawa, A.: Formal Verification of the Heap Manager of an Operating System using Separation Logic. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 400–419. Springer, Heidelberg (2006)
Affeldt, R., Marti, N.: An Approach to Formal Verification of Arithmetic Functions in Assembly|Proof Scripts, http://staff.aist.go.jp/reynald.affeldt/seplog/asian2006
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Affeldt, R., Marti, N. (2007). An Approach to Formal Verification of Arithmetic Functions in Assembly. In: Okada, M., Satoh, I. (eds) Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues. ASIAN 2006. Lecture Notes in Computer Science, vol 4435. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77505-8_27
Download citation
DOI: https://doi.org/10.1007/978-3-540-77505-8_27
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77504-1
Online ISBN: 978-3-540-77505-8
eBook Packages: Computer ScienceComputer Science (R0)