An Abstract Interpretation-based Approach to Mobile Code Safety

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 (or proof) checker --a process which should be much simpler, efficient, and automatic than generating the original proof. We herein introduce 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 slice of the abstract interpretation-based static analysis results which is especially useful as a certificate. We propose an algorithm for checking the validity of the certificate on the consumer side which is itself in fact a very simplified and efficient specialized abstract-interpreter. Our ideas are illustrated through an example implemented in the CiaoPP system. Though further experimentation is still required, we believe the proposed approach is of interest for bringing the automation and expressiveness which is inherent in the abstract interpretation techniques to the area of mobile code safety.

Keywords: Mobile Code Safety, Certifying Compilation, Proof-Carrying Code, Abstract Interpretation, Static Analysis.