Abstract
Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The practical uptake of PCC greatly depends on the existence of a variety of enabling technologies which allow both to prove programs correct and to replace a costly verification process by an efficient checking procedure on the consumer side. In this work we propose Abstraction-Carrying Code (ACC), a novel approach which uses abstract interpretation as enabling technology. We argue that the large body of applications of abstract interpretation to program verification is amenable to the overall PCC scheme. In particular, we rely on an expressive class of safety policies which can be defined over different abstract domains. We use an abstraction (or abstract model) of the program computed by standard static analyzers as a certificate. The validity of the abstraction on the consumer side is checked in a single-pass by a very efficient and specialized abstract-interpreter. We believe that ACC brings the expressiveness, flexibility and automation which is inherent in abstract interpretation techniques to the area of mobile code safety. We have implemented and benchmarked ACC within the Ciao system preprocessor. The experimental results show that the checking phase is indeed faster than the proof generation phase, and that the sizes of certificates are reasonable.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Aspinall, D., Gilmore, S., Hofmann, M., Sannella, D., Stark, I.: Mobile resource guarantees for smart devices. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 1–26. Springer, Heidelberg (2005)
Bruynooghe, M.: A Practical Framework for the Abstract Interpretation of Logic Programs. Journal of Logic Programming 10, 91–124 (1991)
Bueno, F., Cabeza, D., Carro, M., Hermenegildo, M., López-García, P., Puebla, G.: The Ciao System. Reference Manual (v1.10). Technical University of Madrid (UPM) (May 2004), Available at http://clip.dia.fi.upm.es/Software/Ciao
Charatonik, W.: Directional Type Checking for Logic Programs: Beyond Discriminative Types. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 72–87. Springer, Heidelberg (2000)
Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL 1977, pp. 238–252 (1977)
Dart, P.W., Zobel, J.: A Regular Type Language for Logic Programs. In: Types in Logic Programming, pp. 157–187. MIT Press, Cambridge (1992)
Früwirth, T., Shapiro, E., Vardi, M.Y., Yardeni, E.: Logic programs as types for logic programs. In: Proc. LICS 1991, pp. 300–309 (1991)
Hermenegildo, M., Puebla, G., Bueno, F., López-García, P.: Program Development Using Abstract Interpretation (and The Ciao System Preprocessor). In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 127–152. Springer, Heidelberg (2003)
Hermenegildo, M., Puebla, G., Marriott, K., Stuckey, P.: Incremental Analysis of Constraint Logic Programs. ACM TOPLAS 22(2), 187–223 (2000)
Jaffar, J., Maher, M.J.: Constraint Logic Programming: A Survey. Journal of Logic Programming 19/20, 503–581 (1994)
Leroy, X.: Java bytecode verification: algorithms and formalizations. Journal of Automated Reasoning 30(3-4), 235–269 (2003)
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification. Addison-Wesley, Reading (1997)
Morrisett, G., Walker, D., Crary, K., Glew, N.: From system F to typed assembly language. ACM TOPLAS 21(3), 527–568 (1999)
Muthukumar, K., Hermenegildo, M.: Combined Determination of Sharing and Freeness of Program Variables Through Abstract Interpretation. In: 1991 International Conference on Logic Programming, June 1991, pp. 49–63. MIT Press, Cambridge (1991)
Necula, G.: Proof-Carrying Code. In: Proc. of POPL 1997, pp. 106–119. ACM Press, New York (1997)
Necula, G., Lee, P.: The Design and Implementation of a Certifying Compiler. In: Proc. of PLDI 1998, ACM Press, New York (1998)
Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: Proceedings of POPL 2001, pp. 142–154. ACM Press, New York (2001)
Puebla, G., Bueno, F., Hermenegildo, M.: An Assertion Language for Constraint Logic Programs. In: Deransart, P., Małuszyński, J. (eds.) DiSCiPl 1999. LNCS, vol. 1870, pp. 23–61. Springer, Heidelberg (2000)
Rose, K., Rose, E.: Lightweight bytecode verification. In: OOPSALA Workshop on Formal Underpinnings of Java (1998)
Sekar, R., Venkatakrishnan, V.N., Basu, S., Bhatkar, S., Du Varney, D.: Modelcarrying code: A practical approach for safe execution of untrusted applications. In: Proc. of SOSP 2003, pp. 15–28. ACM Press, New York (2003)
Vaucheret, C., Bueno, F.: More precise yet efficient type inference for logic programs. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 102–116. Springer, Heidelberg (2002)
Wildmoser, M., Nipkow, T.: Certifying Machine Code Safety: Shallow Versus Deep Embedding. In: Slind, K., Bunker, A., Gopalakrishnan, G.C. (eds.) TPHOLs 2004. LNCS, vol. 3223, pp. 305–320. Springer, Heidelberg (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Albert, E., Puebla, G., Hermenegildo, M. (2005). Abstraction-Carrying Code. In: Baader, F., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2005. Lecture Notes in Computer Science(), vol 3452. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-32275-7_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-32275-7_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25236-8
Online ISBN: 978-3-540-32275-7
eBook Packages: Computer ScienceComputer Science (R0)