Full text
Preview |
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
Albert Albiol, Elvira, Hermenegildo, Manuel V. ORCID: https://orcid.org/0000-0002-7583-323X and Puebla Sánchez, Alvaro Germán
(2008).
Abstraction-carrying code: a model for mobile code safety.
"New generation computing", v. 26
(n. 2);
pp. 171-204.
ISSN 0288-3635.
https://doi.org/10.1007/s00354-008-0039-7.
Title: | Abstraction-carrying code: a model for mobile code safety |
---|---|
Author/s: |
|
Item Type: | Article |
Título de Revista/Publicación: | New generation computing |
Date: | 2008 |
ISSN: | 0288-3635 |
Volume: | 26 |
Subjects: | |
Freetext Keywords: | Logic Programming, Static Analysis, Abstract Interpretation, Programación lógica, Análisis estático, Interpretación abstracta |
Faculty: | Facultad de Informática (UPM) |
Department: | Inteligencia Artificial |
Creative Commons Licenses: | Recognition - No derivative works - Non commercial |
Preview |
PDF
- Requires a PDF viewer, such as GSview, Xpdf or Adobe Acrobat Reader
Download (1MB) | Preview |
Proof-Carrying Code (PCC) is a general approach to mobile
code safety in which programs are augmented with a certificate (or proof).
The intended benefit is that the program consumer can locally validate the
certificate w.r.t. the "untrustcd" program by means of a certificate checker a
process which should be much simpler, efficient, and automatic than generating
the original proof. The practical uptake of PCC greatly depends on the
existence of a variety of enabling technologies which allow both proving programs
correct and replacing a costly verification process by an efficient checking
proceduri on th( consumer side. In this work we propose Abstraction-
Carrying Code (ACC), a novel approach which uses abstract interpretation
as enabling technology. We argue that the large body of applications of abstract
interpretation to program verification is amenable to the overall PCC
scheme. In particular, we rely on an expressive class of safely policies which
can be defined over different abstract domains. We use an abstraction (or
abstract model) of the program computed by standard static analyzers as a
certificate. The validity of the abstraction on ihe consumer side is checked
in a single pass by a very efficient and specialized abstract-interpreter. We
believe that ACC brings the expressiveness, flexibility and automation which
is inherent in abstract interpretation techniques to the area of mobile code
safety.
Item ID: | 11150 |
---|---|
DC Identifier: | https://oa.upm.es/11150/ |
OAI Identifier: | oai:oa.upm.es:11150 |
DOI: | 10.1007/s00354-008-0039-7 |
Official URL: | http://www.springerlink.com/content/4167x1l1621441... |
Deposited by: | Biblioteca Facultad de Informatica |
Deposited on: | 25 Sep 2012 07:03 |
Last Modified: | 20 Apr 2016 19:19 |