Experiments in abstract interpretation-based code certification for pervasive systems

Albert Albiol, Elvira; Puebla Sánchez, Alvaro Germán y Hermenegildo, Manuel V. (2004). Experiments in abstract interpretation-based code certification for pervasive systems. En: "Systems, Man and Cybernetics, 2004 IEEE International Conference on", 10-13 Oct. 2004. ISBN 0780385667.

Descripción

Título: Experiments in abstract interpretation-based code certification for pervasive systems
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: Systems, Man and Cybernetics, 2004 IEEE International Conference on
Fechas del Evento: 10-13 Oct. 2004
Título del Libro: Systems, Man and Cybernetics, 2004 IEEE International Conference on
Fecha: 2004
ISBN: 0780385667
Volumen: 2
Materias:
Palabras Clave Informales: Logic programming, Abstract interpretation, Mobile safety, Proof-carrying code, Programación lógica, Interpreatción de resúmenes, seguridad móvil.
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 (610kB) | Vista Previa

Resumen

Proof carrying code (PCC) is a general is originally a roof in ñrst-order logic of certain vermethodology for certifying that the execution of an un- ification onditions and the checking process involves trusted mobile code is safe. The baste idea is that the ensuring that the certifícate is indeed a valid ñrst-order code supplier attaches a certifícate to the mobile code proof. which the consumer checks in order to ensure that the The main practical difñculty of PCC techniques is in code is indeed safe. The potential benefit is that the generating safety certiñeates which at the same time: i) consumer's task is reduced from the level of proving to allow expressing interesting safety properties, ii) can be the level of checking. Recently, the abstract interpre- generated automatically and, iii) are easy and efficient tation techniques developed, in logic programming have to check. In [1], the abstract interpretation techniques been proposed as a basis for PCC. This extended ab- [5] developed in logic programming1 are proposed as stract reports on experiments which illustrate several is- a basis for PCC. They offer a number of advantages sues involved in abstract interpretation-based certifica- for dealing with the aforementioned issues. In particution. First, we describe the implementation of our sys- lar, the xpressiveness of existing abstract domains will tem in the context of CiaoPP: the preprocessor of the be implicitly available in abstract interpretation-based Ciao multi-paradigm programming system. Then, by code certification to deñne a wide range of safety propermeans of some experiments, we show how code certifi- ties. Furthermore, the approach inherits the automation catión is aided in the implementation of the framework. and inference power of the abstract interpretation en- Finally, we discuss the application of our method within gines used in (Constraint) Logic Programming, (C)LP. the área, of pervasive systems

Más información

ID de Registro: 14366
Identificador DC: http://oa.upm.es/14366/
Identificador OAI: oai:oa.upm.es:14366
URL Oficial: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=1399773
Depositado por: Biblioteca Facultad de Informatica
Depositado el: 26 Ene 2013 07:07
Ultima Modificación: 21 Abr 2016 14:00
  • 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