Certificate translation for specification-preserving advices
Authors: 
Gilles Barthe, César KunzAuthors Info & Claims
Gilles Barthe, César KunzAuthors Info & ClaimsPages 9 - 18
Abstract
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.
References
[1]
J. Aldrich. Open modules: Modular reasoning about advice. In A. P. Black, editor, ECOOP, volume 3586 of Lecture Notes in Computer Science, pages 144--168. Springer, 2005.
[2]
AspectJ Team. The AspectJ programming guide. Version 1.5.3. Available from http://eclipse.org/aspectj, 2006.
[3]
P. Avgustinov, A. S. Christensen, L. J. Hendren, S. Kuzins, J. Lhoták, O. Lhoták, O. de Moor, D. Sereni, G. Sittampalam, and J. Tibble. abc : An extensible aspectj compiler. 3880:293--334, 2006.
[4]
G. Barthe, B. Grégoire, C. Kunz, and T. Rezk. Certificate translation for optimizing compilers. In K. Yi, editor, SAS, volume 4134 of Lecture Notes in Computer Science, pages 301--317. Springer, 2006.
[5]
G. Barthe, B. Grégoire, and M. Pavlova. Preservation of proof obligations for java. Draft paper, 2008.
[6]
G. Barthe, T. Rezk, and A. Saabas. Proof obligations preserving compilation. In T. Dimitrakos, F. Martinelli, P. Y. A. Ryan, and S. A. Schneider, editors, Formal Aspects in Security and Trust, volume 3866 of Lecture Notes in Computer Science, pages 112--126. Springer, 2005.
[7]
L. Burdy and M. Pavlova. Java bytecode specification and verification. In Symposium on Applied Computing, pages 1835--1839. ACM Press, 2006.
[8]
C. Clifton. A design discipline and language features for modular reasoning in aspect-oriented programs. Ph.d. thesis, Iowa State University, 2005.
[9]
C. Clifton and G. Leavens. Spectators and assistants: Enabling modular aspect-oriented reasoning. Technical report, Iowa State University, 2002.
[10]
C. Clifton, G. T. Leavens, and J. Noble. Mao: Ownership and effects for more effective reasoning about aspects. In E. Ernst, editor, ECOOP, volume 4609 of Lecture Notes in Computer Science, pages 451--475. Springer, 2007.
[11]
D. S. Dantas and D. Walker. Harmless advice. In POPL '06: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pages 383--396, New York, NY, USA, 2006. ACM Press.
[12]
S. Djoko Djoko, R. Douence, and P. Fradet. Aspects preserving properties. In PEPM '08: Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, pages 135--145, New York, NY, USA, 2008. ACM.
[13]
R. M. Golbeck and G. Kiczales. A machine code model for efficient advice dispatch. In VMIL '07: Proceedings of the 1st workshop on Virtual machines and intermediate languages for emerging modularization mechanisms, page 2, New York, NY, USA, 2007. ACM.
[14]
M. Goldman and S. Katz. Modular generic verification of LTL properties for aspects. In Foundations of Aspect Languages Workshop (FOAL06), 2006.
[15]
S. Katz. Aspect categories and classes of temporal properties. In A. Rashid and M. Aksit, editors, T. Aspect-Oriented Software Development I, volume 3880 of Lecture Notes in Computer Science, pages 106--134. Springer, 2006.
[16]
S. Krishnamurthi, K. Fisler, and M. Greenberg. Verifying aspect advice modularly. In SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, pages 137--146, New York, NY, USA, 2004. ACM Press.
[17]
G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML Reference Manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, February 2007.
[18]
P. Müller and M. Nordio. Proof-transforming compilation of programs with abrupt termination. In SAVCBS '07: Proceedings of the 2007 conference on Specification and verification of component-based systems, pages 39--46, New York, NY, USA, 2007. ACM.
[19]
G. C. Necula. Proof-Carrying Code. In Proceedings of POPL'97, pages 106--119. ACM Press, 1997.
[20]
G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of OSDI'96, pages 229--243. Usenix, 1996.
[21]
M. Pavlova. Java bytecode verification and its applications. Thése de doctorat, spécialité informatique, Université Nice Sophia Antipolis, France, January 2007.
[22]
M. Rinard, A. Salcianu, and S. Bugrara. A classification system and analysis for aspect-oriented programs. In SIGSOFT '04/FSE-12: Proceedings of the 12th ACM SIGSOFT twelfth international symposium on Foundations of software engineering, pages 147--158, New York, NY, USA, 2004. ACM Press.
[23]
D. Walker, S. Zdancewic, and J. Ligatti. A theory of aspects. In C. Runciman and O. Shivers, editors, ICFP, pages 127--139. ACM, 2003.
[24]
J. Zhao and M. C. Rinard. Pipa: A behavioral interface specification language for aspectj. In M. Pezzè, editor, FASE, volume 2621 of Lecture Notes in Computer Science, pages 150--165. Springer, 2003.
Index Terms
- Certificate translation for specification-preserving advices
Recommendations
Awesome: an aspect co-weaving system for composing multiple aspect-oriented extensions
OOPSLA '07: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems, languages and applicationsDomain specific aspect-oriented language extensions offer unique capabilities to deal with a variety of cross cutting concerns. Ideally, one should be able to use several of these extensions together in a single program. Unfortunately, each extension ...
Quasi-controlled Experimentations on the Impact of AOP on Software Comprehensibility
CSMR '13: Proceedings of the 2013 17th European Conference on Software Maintenance and ReengineeringAspect-oriented programming (AOP) emerged as a paradigm to modularize the concerns that lead to interwoven code if implemented using traditional programming techniques. Unfortunately, the new constructs introduced by aspect-oriented (AO) languages ...
An Abstract Model of Certificate Translation
A certificate is a mathematical object that can be used to establish that a piece of mobile code satisfies some security policy. In general, certificates cannot be generated automatically. There is thus an interest in developing methods to reuse ...
Comments
Information & Contributors
Information
Published In
Copyright © 2008 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 01 April 2008
Check for updates
Author Tags
Qualifiers
- Research-article
Conference
AOSD08
Acceptance Rates
Overall Acceptance Rate 5 of 6 submissions, 83%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 105Total Downloads
- Downloads (Last 12 months)0
- Downloads (Last 6 weeks)0
Reflects downloads up to 24 Dec 2024
Other Metrics
Citations
Cited By
View allView Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in