Abstract
A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. Since in general certificates cannot be generated automatically, there is an interest in developing methods to reuse certificates. This article formalises in the setting of abstract interpretation a method to transform certificates of program correctness along program transformations.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Albert, E., Puebla, G., Hermenegildo, M.V.: Abstraction-carrying code. In: Baader, F., Voronkov, A. (eds.) LPAR 2004. LNCS (LNAI), vol. 3452, pp. 380–397. Springer, Heidelberg (2005)
Bannwart, F.Y., Müller, P.: A program logic for bytecode. In: Spoto, F. (ed.) Electronic Notes in Theoretical Computer Science, vol. 141, pp. 255–273. Elsevier, Amsterdam (2005)
Barthe, G., Grégoire, B., Kunz, C., Rezk, T.: Certificate translation for optimizing compilers. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, Springer, Heidelberg (2006)
Barthe, G., Rezk, T., Saabas, A.: Proof obligations preserving compilation. In: Dimitrakos, T., Martinelli, F., Ryan, P.Y.A., Schneider, S. (eds.) FAST 2005. LNCS, vol. 3866, pp. 112–126. Springer, Heidelberg (2006)
Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: Jones, N.D., Leroy, X. (eds.) Principles of Programming Languages, pp. 14–25. ACM Press, New York (2004)
Besson, F., Jensen, T., Pichardie, D., Turpin, T.: Result certification for relational program analysis. Technical report, IRISA (2007)
Chaieb, A.: Proof-producing program analysis. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 287–301. Springer, Heidelberg (2006)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages, pp. 238–252 (1977)
Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Principles of Programming Languages, pp. 269–282 (1979)
Müller, P., Nordio, M.: Proof-transforming compilation of programs with abrupt termination. Technical Report 565, ETH Zurich (2007)
Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106–119. ACM Press, New York (1997)
Rival, X.: Abstract Interpretation-Based Certification of Assembly Code. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) VMCAI 2003. LNCS, vol. 2575, pp. 41–55. Springer, Heidelberg (2002)
Rival, X.: Symbolic Transfer Functions-based Approaches to Certified Compilation. In: Principles of Programming Languages, pp. 1–13. ACM Press, New York (2004)
Saabas, A., Uustalu, T.: Type systems for optimizing stack-based code. In: Huisman, M., Spoto, F. (eds.) Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol. 190(1), pp. 103–119. Elsevier, Amsterdam (2007)
Seo, S., Yang, H., Yi, K.: Automatic Construction of Hoare Proofs from Abstract Interpretation Results. In: Ohori, A. (ed.) APLAS 2003. LNCS, vol. 2895, pp. 230–245. Springer, Heidelberg (2003)
Wildmoser, M., Chaieb, A., Nipkow, T.: Bytecode analysis for proof carrying code. In: Spoto, F. (ed.) Bytecode Semantics, Verification, Analysis and Transformation. Electronic Notes in Theoretical Computer Science, vol. 141, Elsevier, Amsterdam (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barthe, G., Kunz, C. (2008). Certificate Translation in Abstract Interpretation. In: Drossopoulou, S. (eds) Programming Languages and Systems. ESOP 2008. Lecture Notes in Computer Science, vol 4960. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-78739-6_28
Download citation
DOI: https://doi.org/10.1007/978-3-540-78739-6_28
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-78738-9
Online ISBN: 978-3-540-78739-6
eBook Packages: Computer ScienceComputer Science (R0)