|
Abstract:
Recent approaches to mobile code safety, like "proof-carrying code", involve associating safety information to programs. The code supplier provides a program and also includes with it a certificate (or "proof") whose validity
entails compliance with a predefined safety policy. 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. This talk presents a novel approach to mobile code safety which follows a similar scheme, but which is based throughout on the use of abstract
interpretation techniques. In our framework the safety policy is specified by using an expressive assertion language defined over abstract domains. We identify a particular subset of the abstract interpretation-based static
analysis results which is especially useful as a certificate. The validity of the certificate on the consumer side is checked by a very simplified and efficiently specialized abstract-interpreter. The resulting scheme has been
implemented and benchmarked within the CiaoPP system, which will be demonstrated during the talk.
|