Experiments in abstract interpretation-based code certification for pervasive systems

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

Description

Title: Experiments in abstract interpretation-based code certification for pervasive systems
Author/s:
  • Albert Albiol, Elvira
  • Puebla Sánchez, Alvaro Germán
  • Hermenegildo, Manuel V.
Item Type: Presentation at Congress or Conference (Article)
Event Title: Systems, Man and Cybernetics, 2004 IEEE International Conference on
Event Dates: 10-13 Oct. 2004
Title of Book: Systems, Man and Cybernetics, 2004 IEEE International Conference on
Date: 2004
ISBN: 0780385667
Volume: 2
Subjects:
Freetext Keywords: Logic programming, Abstract interpretation, Mobile safety, Proof-carrying code, Programación lógica, Interpreatción de resúmenes, seguridad móvil.
Faculty: Facultad de Informática (UPM)
Department: Inteligencia Artificial
Creative Commons Licenses: Recognition - No derivative works - Non commercial

Full text

[img]
Preview
PDF - Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (610kB) | Preview

Abstract

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

More information

Item ID: 14366
DC Identifier: http://oa.upm.es/14366/
OAI Identifier: oai:oa.upm.es:14366
Official URL: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=1399773
Deposited by: Biblioteca Facultad de Informatica
Deposited on: 26 Jan 2013 07:07
Last Modified: 21 Apr 2016 14:00
  • Logo InvestigaM (UPM)
  • Logo GEOUP4
  • Logo Open Access
  • Open Access
  • Logo Sherpa/Romeo
    Check whether the anglo-saxon journal in which you have published an article allows you to also publish it under open access.
  • Logo Dulcinea
    Check whether the spanish journal in which you have published an article allows you to also publish it under open access.
  • Logo de Recolecta
  • Logo del Observatorio I+D+i UPM
  • Logo de OpenCourseWare UPM