Abstraction-carrying code: a model for mobile code safety

Albert Albiol, Elvira and Puebla Sánchez, Alvaro Germán and Hermenegildo, Manuel V. (2005). Abstraction-carrying code: a model for mobile code safety. Monografía (Technical Report). Facultad de Informática (UPM), Madrid, España.

Description

Title: Abstraction-carrying code: a model for mobile code safety
Author/s:
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Monograph (Technical Report)
Date: 2005
Subjects:
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (324kB) | Preview

Abstract

Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can locally validate the certificate w.r.t. the “untrusted” program by means of a certificate checker—a process which should be much simpler, efficient, and automatic than generating the original 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. While our approach is general, we develop it for concreteness in the context of constraint logic programming. 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. Moreover, the preprocessor is based on compiletime (and run-time) tools for the certification of CLP programs with resource consumption assurances. Indeed, as an application of ACC we illustrate that, thanks to the fact that abstract interpretation techniques allow inferring very rich information, our technique can be used to generate certificates which specify complex program properties including traditional safety issues but also resource-related properties like, for example, the kind of load the code is going to pose.

More information

Item ID: 55480
DC Identifier: http://oa.upm.es/55480/
OAI Identifier: oai:oa.upm.es:55480
Official URL: http://cliplab.org/papers/ai-safety-journal.pdf
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 18 Jun 2019 10:28
Last Modified: 18 Jun 2019 10:28
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM