Abstract interpretation-based code certification for pervasive systems: Preliminary experiments

Albert Albiol, Elvira; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2004). Abstract interpretation-based code certification for pervasive systems: Preliminary experiments. En: "Workshop on Software Analysis and Development for Pervasive Systems", August 24, 2004, Verona, Italy.

Descripción

Título: Abstract interpretation-based code certification for pervasive systems: Preliminary experiments
Autor/es:
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Tipo de Documento: Ponencia en Congreso o Jornada (Artículo)
Título del Evento: Workshop on Software Analysis and Development for Pervasive Systems
Fechas del Evento: August 24, 2004
Lugar del Evento: Verona, Italy
Título del Libro: SONDA'04 Proceedings
Fecha: Agosto 2004
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 (644kB) | Vista Previa

Resumen

Proof carrying code is a general methodology for certifying that the execution of an untrusted mobile code is safe, according to a predefined safety policy. The basic idea is that the code supplier attaches a certifícate (or proof) to the mobile code which, then, the consumer checks in order to ensure that the code is indeed safe. The potential benefit is that the consumer's task is reduced from the level of proving to the level of checking, a much simpler task. Recently, the abstract interpretation techniques developed in logic programming have been proposed as a basis for proof carrying code [1]. To this end, the certifícate is generated from an abstract interpretation-based proof of safety. Intuitively, the verification condition is extracted from a set of assertions guaranteeing safety and the answer table generated during the analysis. Given this information, it is relatively simple and fast to verify that the code does meet this proof and so its execution is safe. This extended abstract reports on experiments which illustrate several issues involved in abstract interpretation-based code certification. First, we describe the implementation of our system in the context of CiaoPP: the preprocessor of the Ciao multi-paradigm (constraint) logic programming system. Then, by means of some experiments, we show how code certification is aided in the implementation of the framework. Finally, we discuss the application of our method within the área of pervasive systems which may lack the necessary computing resources to verify safety on their own. We herein illustrate the relevance of the information inferred by existing cost analysis to control resource usage in this context. Moreover, since the (rather complex) analysis phase is replaced by a simpler, efficient checking process at the code consumer side, we believe that our abstract interpretation-based approach to proof-carrying code becomes practically applicable to this kind of systems.

Más información

ID de Registro: 14612
Identificador DC: http://oa.upm.es/14612/
Identificador OAI: oai:oa.upm.es:14612
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 09 Mar 2013 08:25
Ultima Modificación: 21 Abr 2016 14:21
  • 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