Abstract
We present a method for analyzing assembly programs obtained by compilation and checking safety properties on compiled programs. It proceeds by analyzing the source program, translating the invariant obtained at the source level, and then checking the soundness of the translated invariant with respect to the assembly program. This process is especially adapted to the certification of assembly or other machine-level kinds of programs. Furthermore, the success of invariant checking enhances the level of confidence in the results of both the compilation and the static analysis. From a practical point of view, our method is generic in the choice of an abstract domain for representing sets of stores, and the process does not interact with the compilation itself. Hence a certification tool can be interfaced with an existing analyzer and designed so as to work with a class of compilers that do not need to be modified. Finally, a prototype was implemented to validate the approach.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Alt M, Ferdinand C, Martin F, Wilhelm R (1996) Cache behavior prediction by abstract interpretation. In: Proceedings of the static analysis symposium (SAS’96), September 1996. Lecture notes in computer science, vol 1996. Springer, Berlin Heidelberg New York, pp 51–66
Appel AW (2001) Foundational proof-carrying code. In: Proceedings of the 16th symposium on logics in computer science (LICS’01), Boston, June 2001, pp 247–256
Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2002) Design and implementation of a special-purpose static program analyzer for safety-critical real-time embedded software, invited chapter. In: The essence of computation: complexity, analysis, transformation. Essays dedicated to Neil D. Jones. Lecture notes in computer science, vol 2566. Springer, Berlin Heidelberg New York, pp 85–108
Blanchet B, Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, Rival X (2003) A static analyzer for large safety critical software. In: Proceedings of the ACM SIGPLAN 2003 conference on programming languages, design and implementation (PLDI’03), San Diego, October 2003. Lecture notes in computer science, vol 2566. Springer, Berlin Heidelberg New York, pp 85–108
Bertot Y (1998) A certified compiler for an imperative language. Technical Report RR-3488, INRIA, 1998
Bourdoncle F (1993) Efficient chaotic iteration strategies with widenings. Lecture notes in computer science, vol 735. Springer, Berlin Heidelberg New York, pp 128–141
Cousot P (1981) Semantic foundations of program analysis. In: Program flow analysis: theory and applications, chap 10. Prentice-Hall, Englewood Cliffs, NJ, pp 303–342
Cousot P (1997) Constructive design of a hierarchy of semantics of a transition system by abstract interpretation. Electron Notes Theor Comput Sci vol 6. Available at: http://www.elsevier.nl/locate/entcs/volume6.html
Cousot P (1999) The calculational design of a generic abstract interpreter. In: Calculational system design. NATO ASI Series F. IOS Press, Amsterdam
Cousot P, Cousot R (1977) Abstract Interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference record of the 4th symposium on principles of programming languages (POPL’77), Los Angeles, January 1977, pp 238–252
Cousot P, Cousot R (1979) Systematic design of program analysis frameworks. In: Conference Record of the 6th symposium on principles of programming languages (POPL’79), San Antonio, TX, January 1979. ACM Press, New York, pp 269–282
Cousot P, Cousot R (1992) Abstract interpretation frameworks. J Logic Comput 2(4):511–547
Cousot P, Cousot R (2002) Systematic design of program transformation frameworks by abstract interpretation. In: Proceedings of the 29th symposium on principles of programming languages (POPL’02), Portland, OR, January 2002. ACM Press, New York, pp 178–190
Cousot P, Halbwachs N (1978) Automatic discovery of linear restraints among variables of a program. In: Proceedings of the 5th symposium on principles of programming languages (POPL’78), Tucson, AZ, January 1978, pp 84–97
Granger P (1989) Static analysis of arithmetical congruences. Int J Comput Math 30:165–190
Handjieva M, Tzolovski S (1998) Refining static analayses by trace-based partitioning using control flow. In: Proceedings of the 5th static analysis symposium (SAS’98), Pisa, Italy, September 1998. Lecture notes in computer science, vol 1503. Springer, Berlin Heidelberg New York, pp 200–214
Karr M (1976) Affine relationships among variables of a program. Acta Inf 1976, pp 133–151
Miné A (2001) A new numerical abstract domain based on difference-bound matrices. In: Proceedings of the conference on programs as data objects (PADO II), Aahrus, Denmark, May 2001. Lecture notes in computer science, vol 2053. Springer, Berlin Heidelberg New York, pp 155–172
Morrisett G, Tarditi D, Cheng P, Stone C, Harper R, Lee P (1996) The TIL/ML compiler: performance and safety through types. In: Proceedings of the workshop on compiler support for systems software, Tucson, AZ, February 1996
Morrisett G, Crary K, Glew N, Grossman D, Samuels R, Smith F, Walker D (1999) TALx86: A realistic typed assembly language. In: Proceedings of the 1999 ACM SIGPLAN workshop on compiler support for system software, Atlanta, GA, May 1999, pp 25–35
Motorola (1997) PowerPC microprocessor family: the programming environments for 32-Bit microprocessors, Publication no. G522-0290-01, revised 02/21/00
Necula GC (1997) Proof-carrying code. In: Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on principles of programming langauges (POPL’97), Paris, January 1997, pp 106–119
Necula GC (2000) Translation validation for an optimizing compiler. In: Proceedings of the 2000 ACM SIGPLAN conference on programming language design and implementation (PLDI’00), Vancouver, BC, Canada, June 2000, pp 83–94
Necula GC, Lee P (1998) The design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 98 conference on programming languages, design and implementation (PLDI’98), Montréal, June 1998, pp 333–344
Pnueli A, Shtrichman O, Siegel M (1998) Translation validation for synchronous languages. In: Prooceedings of the 25th international colloquium on automata, languages and programming (ICALP’98), Aahrus, Denmark, July 1998. Lecture notes in computer science, vol 1443. Springer, Berlin Heidelberg New York, pp 235–246
Rival X (2003) Abstract interpretation-based certification of assembly code. In: Proceedings of the 4th international conference on verification, model checking and abstract interpretation (VMCAI’03), New York, January 2003, pp 41–55
Strecker M (2002) Formal verification of a Java compiler in Isabelle. In: Proceedings of the conference on automated deduction (CADE), Copenhagen, Denmark, July 2002. Lecture notes in computer science, vol 2392. Springer, Berlin Heidelberg New York, pp 63–77
Tarditi D, Morrisett G, Cheng P, Stone C, Harper R, Lee P (1996) TIL: A type-directed optimizing compiler for ML. In: Proceedings of the ACM SIGPLAN’96 conference on programming language design and implementation, May 1996, pp 181–192
Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pacific J Math 5:285–309
Theiling H, Ferdinand C (1998) Combining abstract interpretation and ILP for microarchitecture modelling and program path analysis. In: Proceedings of the 19th IEEE real-time systems symposium, Madrid, Spain, pp 144–153
Theiling H, Ferdinand C, Wilhelm R (2000) Fast and precise WCET prediction by separate cache and path analyses. Real-Time Sys 18:157–179
Zuck L, Pnueli A, Fang Y, Goldberg B (2002) VOC: A translation validator for optimizing compilers. In: Electronic notes in theoretical computer science, vol 65. Elsevier, Amsterdam
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Rival, X. Certification of compiled assembly code by invariant translation. Int J Softw Tools Technol Transfer 6, 15–37 (2004). https://doi.org/10.1007/s10009-003-0125-6
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-003-0125-6