Reduced certificates for abstraction-carrying code

Albert Albiol, Elvira; Arenas Sánchez, Purificación; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2006). Reduced certificates for abstraction-carrying code. En: "22nd International Conference, ICLP 2006", August 17-20, 2006, Seattle, WA, USA. ISBN 978-3-540-36635-5.

Descripción

Título: Reduced certificates for 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: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: 22nd International Conference, ICLP 2006
Fechas del Evento: August 17-20, 2006
Lugar del Evento: Seattle, WA, USA
Título del Libro: Logic Programming
Fecha: 2006
ISBN: 978-3-540-36635-5
Volumen: 4079
Materias:
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 (960kB) | Vista Previa

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 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 (fixedpoint) abstraction to the code consumer is that its validity is checked in a single pass of an abstract interpretation-based checker. A main challenge is to reduce the size of certificates as much as possible while at the same time not increasing checking time. 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 the information relevant to the checker. We also provide a correct checking algorithm together with sufficient conditions for ensuring its completeness. The experimental results within the CiaoPP system show that our proposal is able to greatly reduce the size of certificates in practice.

Más información

ID de Registro: 14349
Identificador DC: http://oa.upm.es/14349/
Identificador OAI: oai:oa.upm.es:14349
URL Oficial: http://link.springer.com/chapter/10.1007%2F11799573_14
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 24 Ene 2013 07:27
Ultima Modificación: 21 Abr 2016 13:58
  • 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