Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-27T15:57:08.388Z Has data issue: false hasContentIssue false
  • English
  • Français

Certificate size reduction in abstraction-carrying code*

Published online by Cambridge University Press:  05 January 2011

ELVIRA ALBERT ,
PURI ARENAS ,
GERMÁN PUEBLA  and
MANUEL HERMENEGILDO
ELVIRA ALBERT
Affiliation:
School of Computer Science, Complutense University of Madrid, Profesor José García Santesmases, s/n, E28040-Madrid, Spain (e-mail: [email protected], [email protected])
PURI ARENAS
Affiliation:
School of Computer Science, Complutense University of Madrid, Profesor José García Santesmases, s/n, E28040-Madrid, Spain (e-mail: [email protected], [email protected])
GERMÁN PUEBLA
Affiliation:
School of Computer Science, Technical University of Madrid, E28660-Boadilla del Monte, Madrid, Spain (e-mail: [email protected], [email protected])
MANUEL HERMENEGILDO
Affiliation:
School of Computer Science, Technical University of Madrid, E28660-Boadilla del Monte, Madrid, Spain; Madrid Institute for Advanced Studies in Software Development Technology (IMDEA Software), Madrid, Spain (e-mail: [email protected])
Get access Rights & Permissions [Opens in a new window]

Abstract

Abstraction-Carrying Code (ACC) has recently been proposed as a framework for mobile code safety in which the code supplier provides a program together with an abstraction (or abstract model of the program) whose validity entails compliance with a predefined safety policy. The abstraction plays thus the role of safety certificate and its generation is carried out automatically by a fixpoint analyzer. The advantage of providing a (fixpoint) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certificates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certificate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certificate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certificate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify the information relevant to the checker. Interestingly, the fact that the reduced certificate omits (parts of) the abstraction has implications in the design of the checker. We provide the sufficient conditions which allow us to ensure that (1) if the checker succeeds in validating the certificate, then the certificate is valid for the program (correctness) and (2) the checker will succeed for any reduced certificate which is valid (completeness). Our approach has been implemented and benchmarked within the CiaoPP system. The experimental results show that our proposal is able to greatly reduce the size of certificates in practice.

Keywords

proof-carrying codeabstraction-carrying codestatic analysisreduced certificatesmobile code
Type
Regular Papers
Information
Theory and Practice of Logic Programming , Volume 12 , Issue 3 , May 2012 , pp. 283 - 318
Copyright
Copyright © Cambridge University Press 2011

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Albert, E., Arenas, P., Puebla, G., and Hermenegildo, M. 2006. Reduced Certificates for Abstraction-Carrying Code. In 22nd International Conference on Logic Programming (ICLP 2006). LNCS, no. 4079. Springer-Verlag, New York, NY, 163–178.Google Scholar
Albert, E., Gómez-Zamalloa, M., Hubert, L. and Puebla, G. 2007. Verification of java bytecode using analysis and transformation of logic programs. In 9th International Symposium on Practical Aspects of Declarative Languages (PADL 2007). LNCS, no. 4354. Springer-Verlag, New York, NY, 124–139.Google Scholar
Albert, E., Puebla, G. and Hermenegildo, M. 2005. Abstraction-carrying code. In 11th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR 2004). LNAI, no. 3452. Springer-Verlag, New York, NY, 380–397.Google Scholar
Albert, E., Puebla, G. and Hermenegildo, M. 2008. Abstraction-carrying code: A model for mobile code safety. New Generation Computing 26, 2 (March), 171–204.CrossRefGoogle Scholar
Barras, B., Boutin, S., Cornes, C., Courant, J., Filliatre, J., Gimenez, E., Herbelin, H., Huet, G., Munoz, C., Murthy, C., Parent, C., Paulin-Mohring, C., Saibi, A. and Werner, B. 1997. The Coq Proof Assistant Reference Manual: Version 6.1, Technical rep. RT-0203. Available at citeseer.ist.psu.edu/barras97coq.htmlGoogle Scholar
Besson, F., Jensen, T. and Pichardie, D. 2006. A PCC architecture based on certified abstract interpretation. In Proceedings of First International Workshop on Emerging Applications of Abstract Interpretation (EAAI 2006), 26 March, Vienna, Austria.Google Scholar
Bruynooghe, M. 1991. A practical framework for the abstract interpretation of logic programs. Journal of Logic Programming 10, 91–124.CrossRefGoogle Scholar
Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-García, P. and Puebla-(Eds.), G. 2009. The Ciao System. Ref. Manual (v1.13), Technical rep., School of Computer Science, T.U. of Madrid (UPM). Available at http://www.ciaohome.org.Google Scholar
Cachera, D., Jensen, T., Pichardie, D. and Rusu, V. 2004. Extracting a data flow analyser in constructive logic. In The European Symposium on Programming (ESOP 2004). LNCS, no. 2986. Springer-Verlag, New York, NY, 385–400.Google Scholar
Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In ACM Symposium on Principles of Programming Languages (POPL'77), Graham, Robert M., Harrison, Michael A. and Sethi, Ravi, Eds. ACM Press, New York, NY, 238–252.CrossRefGoogle Scholar
Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D. and Rival, X. 2005. The ASTRÉE analyser. In The European Symposium on Programming (ESOP 2005). LNCS, no. 3444. Springer-Verlag, New York, NY, 21–30.Google Scholar
de la Banda, M. G., Hermenegildo, M., Bruynooghe, M., Dumortier, V., Janssens, G. and Simoens, W. 1996. Global analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 18, 5 (September), 564–615.CrossRefGoogle Scholar
Genaim, S. and Spoto, F. 2005. Information flow analysis for Java bytecode. In 6th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2005). LNCS, no. 3385. Springer-Verlag, New York, NY, 346–362.CrossRefGoogle Scholar
Harper, R., Honsell, F. and Plotkin, G. 1993. A framework for defining logics. Journal of the Association for Computing Machinery 40, 1, 143–184.CrossRefGoogle Scholar
Hermenegildo, M., Puebla, G., Bueno, F. and López-García, P. 2005. Integrated program debugging, verification, and optimization using abstract interpretation (and the ciao system preprocessor). Science of Computer Programming 58, 1–2 (October), 115–140.CrossRefGoogle Scholar
Hermenegildo, M., Puebla, G., Marriott, K. and Stuckey, P. 2000. Incremental analysis of constraint logic programs. ACM Transactions on Programming Languages and Systems 22, 2 (March), 187–223.CrossRefGoogle Scholar
Jones, N., Gomard, C. and Sestoft, P. 1993. Partial Evaluation and Automatic Program Generation. Prentice Hall, New York.Google Scholar
Kelly, A., Marriott, K., Søndergaard, H. and Stuckey, P. 1998. A practical object-oriented analysis engine for CLP. Software: Practice and Experience 28, 2, 188–224.Google Scholar
Klein, G. and Nipkow, T. 2003. Verified bytecode verifiers. Theoretical Computer Science 3 (298), 583–626.CrossRefGoogle Scholar
Le Charlier, B. and Van Hentenryck, P. 1994. Experimental evaluation of a generic abstract interpretation algorithm for prolog. ACM Transactions on Programming Languages and Systems 16 (1), 35–101.CrossRefGoogle Scholar
Leroy, X. 2003. Java bytecode verification: Algorithms and formalizations. Journal of Automated Reasoning 30, 3–4, 235–269.CrossRefGoogle Scholar
Lloyd, J. 1987. Foundations of Logic Programming. 2nd extended ed., Springer, New York.CrossRefGoogle Scholar
Marriot, K. and Stuckey, P. 1998. Programming with Constraints: An Introduction. MIT Press, Cambridge, MA.CrossRefGoogle Scholar
Méndez-Lojo, M., Navas, J. and Hermenegildo, M. 2007a. A flexible (C)LP-based approach to the analysis of object-oriented programs. In 17th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2007). LNCS, no. 4915. Springer-Verlag, New York, NY, 154–168.Google Scholar
Méndez-Lojo, M., Navas, J. and Hermenegildo, M. 2007b. An efficient, parametric fixpoint algorithm for analysis of Java bytecode. In ETAPS Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2007). Electronic Notes in Theoretical Computer Science, vol. 190. Elsevier, North Holland, 51–66.Google Scholar
Muthukumar, K. and Hermenegildo, M. 1991. Combined determination of sharing and freeness of program variables through abstract interpretation. In International Conference on Logic Programming (ICLP 1991). MIT Press, Cambridge, MA, 49–63.Google Scholar
Muthukumar, K. and Hermenegildo, M. 1992. Compile-time derivation of variable dependency using abstract interpretation. Journal of Logic Programming 13, 2/3 (July), 315–347.CrossRefGoogle Scholar
Necula, G. 1997. Proof-carrying code. In ACM Symposium on Principles of programming languages (POPL 1997). ACM Press, New York, NY, 106–119.Google Scholar
Necula, G. and Lee, P. 1998. Efficient representation and validation of proofs. In IEEE Symposium on Logic in Computer Science (LICS 1998). IEEE Computer Society, Washington, DC, 93–104.Google Scholar
Necula, G. and Rahul, S. 2001. Oracle-based checking of untrusted software. In Principles of Programming Languages (POPL 2001). ACM Press, New York, NY, 142–154.Google Scholar
Puebla, G. and Hermenegildo, M. 1996. Optimized algorithms for the incremental analysis of logic programs. In International Static Analysis Symposium (SAS 1996). LNCS, no. 1145. Springer-Verlag, New York, NY, 270–284.Google Scholar
Rose, E. 2003. Lightweight bytecode verification. Journal of Automated Reasoning 31, 303–334.CrossRefGoogle Scholar
Rose, E. and Rose, K. 1998. Lightweight bytecode verification. In OOPSLA Workshop on Formal Underpinnings of Java, 18 October, Vancouver, Canada.Google Scholar
Secci, S. and Spoto, F. 2005. Pair-sharing analysis of object-oriented programs. In Static Analysis Symposium (SAS 2005). LNCS, no. 3672. Springer-Verlag, New York, NY, 320–335.CrossRefGoogle Scholar
Vallee-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E. and Co, P. 1999. Soot – a Java optimization framework. In Proceedings of Conference of the Centre for Advanced Studies on Collaborative Research (CASCON), 8–11 November, Mississauga, Ontario, Canada. 125–135.Google Scholar