Abstraction-Carrying Code: a Model for Mobile Code Safety |
| |
Authors: | Elvira Albert Germán Puebla Manuel Hermenegildo |
| |
Affiliation: | (1) DSIC, Complutense University of Madrid, Avda. Complutense s/n, E-28040 Madrid, Spain;(2) Technical University of Madrid (UPM), E-28660, Boadilla del Monte, Madrid, Spain;(3) Technical University of Madrid, Spain and CS/EECE Depts., University of New Mexico, Albuquerque, New Mexico, USA |
| |
Abstract: | 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 “untrusted” 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 procedure on the 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 safety 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 the 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.
|
| |
Keywords: | Logic Programming Static Analysis Abstract Interpretation Program Verification Mobile Code Safety |
本文献已被 SpringerLink 等数据库收录! |
|