Certificate size reduction in abstraction-carrying code

Albert Albiol, Elvira; Arenas Sánchez, Purificación; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2010). Certificate size reduction in abstraction-carrying code. "CoRR", v. abs/10 ;

Descripción

Título: Certificate size reduction in abstraction-carrying code
Autor/es:
  • Albert Albiol, Elvira
  • Arenas Sánchez, Purificación
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Artículo
Título de Revista/Publicación: CoRR
Fecha: 13 Octubre 2010
Volumen: abs/10
Materias:
Palabras Clave Informales: Proof-carrying code, Abstraction-carrying code, Static analysis, Reduced certificates, Código con demostración, Análisis estático, Certificados reducidos.
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 - Se necesita un visor de ficheros PDF, como GSview, Xpdf o Adobe Acrobat Reader
Descargar (2MB) | Vista Previa

Localizaciones alternativas

URL Oficial: http://arxiv.org/abs/1010.4533

Resumen

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 fall 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 t h a t our proposal is able to greatly reduce the size of certificates in practice. To appear in Theory and Practice of Logic Programming (TPLP).

Más información

ID de Registro: 14826
Identificador DC: http://oa.upm.es/14826/
Identificador OAI: oai:oa.upm.es:14826
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 11 Abr 2013 06:18
Ultima Modificación: 21 Abr 2016 14:40
  • 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