Certifying assembly programs with trails

Abstract

In this paper, we introduce a new way of certifying assembly programs. Unlike previous program logics, we extract the control-flow information from the code and generate an intermediate trail between the specification and the real code. Trails are auxiliary specifications and treated as modules in the certification process. We define a simple modular program logic called trail-based certified assembly programming (TCAP) to certify and link different parts of a program using the corresponding trails. Because the control flow information in trails is explicit, the rules are easier to design. We show that our logic is powerful enough to prove partial correctness of assembly programs with features including stack-based abstractions and self-modifying code. We also provide a semantics for TCAP and prove that the logic is sound with respect to the semantics.

Keywords

Certifying assembly code / control flow / partial correctness

References

[1] Necula G. Proof-carrying code. In: Proceedings of 24th ACM Symposium on Principles of Programming Languages. 1997, 106–119

[2] Hoare C A R. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10): 576–580

[3] Necula G. Compiling with proofs. Dissertation for the Doctoral Degree. Pittsburgh: Carnegie Mellon University, 1998

[4] Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In: Proceedings of 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1998, 85–97

[5] Appel A W. Foundational proof-carrying code. In: Proceedings of 2001 Symposium on Logic in Computer Science. 2001, 247–258

[6] Ni Z, Shao Z. Certified assembly programming with embedded code pointers. In: Proceedings of 33rd ACM Symposium on Principles of Programming Languages. 2006, 320–333

[7] Glew N, Morrisett G. Type-safe linking and modular assembly language. In: Proceedings of 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1999, 250–261

[8] Feng X, Shao Z, Vaynberg A, Xiang S, Ni Z. Modular verification of assembly code with Stack-based control abstractions. In: Proceedings of 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2006, 401–414

[9] The Coq Development Team. The Coq proof assistant reference manual, The Coq release v8.0, http://coq.inria.fr/10. Cai H, Shao Z, Vaynberg A. Certified self-modifying code. In: Proceedings of 2007 ACM SIGPLAN Conference on Programming Language Design and Implementation. 2007, 66–77

[10] Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D, Weirich S, Zdancewic S. TALx86: a realistic typed assembly language. In: Proceedings of 1999 ACM SIGPLAN Workshop on Compiler Support for System Software. 1999, 25–35

[11] Jones C B. Tentative steps toward a development method for interfering programs. ACM Transactions on Programming Languages and Systems, 1983, 5(4): 596–619

[12] Calcagno C, O’hearn P W, Yang H. Local action and abstract separation logic. In: Proceedings of 22nd Annual IEEE Symposium on Logic in Computer Science. 2007, 366–378

[13] Shivers O. Control-flow analysis of higher-order languages. Dissertation for the Doctoral Degree. Pittsburgh: Carnegie-Mellon University, 1991

[14] Vardoulakis D, Shivers O. CFA2: a context-free approach to control-flow analysis. In: Proceedings of European Symposium on Programming. 2010, 570–589

[15] Tan G, Appel A W. A compositional logic for control flow. In: Proceedings of 7th International Conference on Verification, Model Checking and Abstract Interpretation. 2006, 80–94

Acknowledgements

We thank Prof. Zhong Shao (Yale University), Prof. Xinyu Feng, University of Science and Technology of China, and anonymous referees for their suggestions and comments on the earlier versions of this paper. Our research was supported by the National Natural Science Foundation of China (Grant Nos. 60928004, 61073040 and 61003043) and the Natural Science Foundation of Jiangsu Province, China (BK2008181).

RIGHTS & PERMISSIONS

2014 Higher Education Press and Springer-Verlag Berlin Heidelberg