To appear in Foundations of Aspect-Oriented Languages (FOAL), Brussels, Belgium, April 2008.

Gilles Barthe and César Kunz
INRIA Sophia-Antipolis, Project EVEREST.

Abstract. Aspect Oriented Programming (AOP) is a paradigm with significant potential to separate functionality and cross-cutting concerns. In particular, AOP supports an incremental development process, in which the expected functionality is provided by a baseline program, that is successively refined, possibly by third parties, with aspects that improve non-functional concerns, such as efficiency and security. Therefore, AOP is a natural enabler for Proof Carrying Code (PCC) scenarios that involve, in addition to the code producer and the code consumer, untrusted intermediaries that modify the code. The purpose of this article is to explore a PCC architecture that accommodates such an incremental development process. In order to support a wide range of policies, we extend our earlier work on certificate translation, and show in the context of a very simple language that it is possible to generate certificates of executable code from proofs of aspect-oriented programs. To achieve this goal, we introduce a notion of specification-preserving advice, which provides a mild generalization of the notion of harmless advice by Dantas and Walker, and provide a sound verification method for programs with specification-preserving advices.