Certificate translation for specification-preserving advices

Aspect Oriented Programming (AOP) has 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. The purpose of this article is to explore a PCC architecture that accommodates an incremental development process. We extend our earlier work on certificate translation, and show in the context of a very simple AOP 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, and provide a verification method for programs with specification-preserving advices. Categories and Subject Descriptors D....

• Type: Conference
• Year: 2008
• Where: FOAL
• Authors: Gilles Barthe, César Kunz
• Keywords: FOAL 2008, Incremental Development Process, Natural Language Processing, Simple Aop Language, Specification-preserving Advices