Certificate translation for specification-preserving advices

9 years 3 months ago
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....
Gilles Barthe, César Kunz
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FOAL
Authors Gilles Barthe, César Kunz
Comments (0)