Abstraction-carrying code: a model for mobile code safety

Albert Albiol, Elvira; Hermenegildo, Manuel V. y Puebla Sánchez, Alvaro Germán (2008). Abstraction-carrying code: a model for mobile code safety. "New generation computing", v. 26 (n. 2); pp. 171-204. ISSN 0288-3635. https://doi.org/10.1007/s00354-008-0039-7.

Descripción

Título: Abstraction-carrying code: a model for mobile code safety
Autor/es:
  • Albert Albiol, Elvira
  • Hermenegildo, Manuel V.
  • Puebla Sánchez, Alvaro Germán
Tipo de Documento: Artículo
Título de Revista/Publicación: New generation computing
Fecha: 2008
Volumen: 26
Materias:
Palabras Clave Informales: Logic Programming, Static Analysis, Abstract Interpretation, Programación lógica, Análisis estático, Interpretación abstracta
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

[img]
Vista Previa
PDF (Document Portable Format) - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (1MB) | Vista Previa

Resumen

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 "untrustcd" 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 proving programs correct and replacing a costly verification process by an efficient checking proceduri on th( 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 safely 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 ihe 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.

Más información

ID de Registro: 11150
Identificador DC: http://oa.upm.es/11150/
Identificador OAI: oai:oa.upm.es:11150
Identificador DOI: 10.1007/s00354-008-0039-7
URL Oficial: http://www.springerlink.com/content/4167x1l16214414w/fulltext.pdf
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 25 Sep 2012 07:03
Ultima Modificación: 20 Abr 2016 19:19
  • Open Access
  • Open Access
  • Sherpa-Romeo
    Compruebe si la revista anglosajona en la que ha publicado un artículo permite también su publicación en abierto.
  • Dulcinea
    Compruebe si la revista española en la que ha publicado un artículo permite también su publicación en abierto.
  • Recolecta
  • e-ciencia
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM