Please wait a minute...
Frontiers of Computer Science

ISSN 2095-2228

ISSN 2095-2236(Online)

CN 10-1014/TP

Postal Subscription Code 80-970

2018 Impact Factor: 1.129

Front Comput Sci Chin    0, Vol. Issue () : 472-485    https://doi.org/10.1007/s11704-011-0166-z
RESEARCH ARTICLE
Certifying assembly programs with trails
Wei WANG1,2()
1. Department of Computer Science & Technology, University of Science & Technology of China, Hefei 230027, China; 2. Suzhou Institute for Advanced Study, University of Science & Technology of China, Suzhou 215123, China
 Download: PDF(339 KB)   HTML
 Export: BibTeX | EndNote | Reference Manager | ProCite | RefWorks
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     
Corresponding Author(s): WANG Wei,Email:wqsh@mail.ustc.edu.cn   
Issue Date: 05 December 2011
 Cite this article:   
Wei WANG. Certifying assembly programs with trails[J]. Front Comput Sci Chin, 0, (): 472-485.
 URL:  
https://academic.hep.com.cn/fcs/EN/10.1007/s11704-011-0166-z
https://academic.hep.com.cn/fcs/EN/Y0/V/I/472
Fig.1  Possible end points
Fig.2  Syntax of target machine TM
Fig.3  Registers
Fig.4  Small-step operational semantics
Fig.5  Predefined logic operators and relations
Fig.6  Inference rules for TCAP
Fig.7  Assembly code of factorial function
Fig.8  An understanding of factorial program example
Fig.9  Actions for factorial program example
Fig.10  Example code with exceptions
Fig.11  Actions and generated trails for the exception example
Fig.12  Well-formed trails of GTCAP rules
Fig.13  Example code with dynamic code modifying
Fig.14  Actions and trails for SMC
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
doi: 10.1145/268946.268954
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
doi: 10.1145/292540.292563
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
doi: 10.1145/1133981.1134028
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
Viewed
Full text


Abstract

Cited

  Shared   
  Discussed