|
Descripción
|
|
|---|---|
| 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 (or abstract model of the program) whose validity entails compliance with a prede?ned safety policy. The abstraction plays thus the role of safety certi?cate and its generation is carried out automatically by a ?xpoint analyzer. The advantage of providing a (?x- point) abstraction to the code consumer is that its validity is checked in a single pass (i.e., one iteration) of an abstract interpretation-based checker. A main challenge to make ACC useful in practice is to reduce the size of certi?cates as much as possible while at the same time not increasing checking time. The intuitive idea is to only include in the certi?cate information that the checker is unable to reproduce without iterating. We in- troduce the notion of reduced certi?cate which characterizes the subset of the abstraction which a checker needs in order to validate (and re-construct) the full certi?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. Interestingly, the fact that the reduced certi?cate omits (parts of) the abstraction has implications in the design of the checker. We provide the su?cient conditions which allow us to ensure that 1) if the checker succeeds in validating the certi?cate, then the certi?cate is valid for the program (correctness) and 2) the checker will succeed for any reduced certi?cate which is valid (completeness). Our approach has been implemented and benchmarked within the CiaoPP system. The experimental results show that our proposal is able to greatly reduce the size of certi?cates in practice. | |
|
Internacional
|
Si |
|
JCR del ISI
|
Si |
|
Título de la revista
|
Theory And Practice of Logic Programming |
|
ISSN
|
1471-0684 |
|
Factor de impacto JCR
|
0,667 |
|
Información de impacto
|
|
|
Volumen
|
12 |
|
DOI
|
|
|
Número de revista
|
3 |
|
Desde la página
|
283 |
|
Hasta la página
|
318 |
|
Mes
|
SIN MES |
|
Ranking
|
|