
Certifying assembly programs with trails
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.
Certifying assembly code / control flow / partial correctness
[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
CrossRef
Google scholar
|
[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
CrossRef
Google scholar
|
[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
CrossRef
Google scholar
|
[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
|
/
〈 |
|
〉 |