Reduced certificates for abstraction-carrying code

Albert Albiol, Elvira; Arenas Sánchez, Purificación; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2005). Reduced certificates for abstraction-carrying code. Monografía (Informe Técnico). Facultad de Informática (UPM) [antigua denominación], Madrid, Spain.


Título: Reduced certificates for abstraction-carrying code
  • Albert Albiol, Elvira
  • Arenas Sánchez, Purificación
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Monográfico (Informes, Documentos de trabajo, etc.) (Informe Técnico)
Fecha: Octubre 2005
Escuela: Facultad de Informática (UPM) [antigua denominación]
Departamento: Inteligencia Artificial
Licencias Creative Commons: Reconocimiento - Sin obra derivada - No comercial

Texto completo

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


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 certifícate and its generation is carried out automatically by a fixed-point analyzer. The advantage of providing a (fixed-point) 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 certifícate information that the checker is unable to reproduce without iterating. We introduce the notion of reduced certifícate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certifícate in a single pass. Based on this notion, we instrument a generic analysis algorithm with the necessary extensions in order to identify information which can be reconstructed by the single-pass checker. Finally, we study what the effects of reduced certificates are on the correctness and completeness of the checking process. We provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. Our ideas are illustrated through a running example, implemented in the context of constraint logic programs, which shows that our approach improves state-of-the-art techniques for reducing the size of certificates.

Más información

ID de Registro: 14745
Identificador DC:
Identificador OAI:
URL Oficial:
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 05 Abr 2013 07:06
Ultima Modificación: 21 Abr 2016 14:33
  • GEO_UP4
  • 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
  • InvestigaM
  • Observatorio I+D+i UPM
  • OpenCourseWare UPM