Journal of Computers, Vol 6, No 8 (2011), 1691-1698, Aug 2011
doi:10.4304/jcp.6.8.1691-1698

A Method for Certifying Code in Trust-By-Policy-Adherence

Zeng Guo-Sun, Li Li

Abstract


    This paper proposes and details the notion of trust by policy adherence (TBPA), meaning that code can be certified on the basis of its security-related behaviors rather than its origins and integrity. We describe the overall life cycle of code in this setting, and propose a detailed method whereby a program’s policy adherence can be verified. We suggest enforcing security policies over code by means of aspect-oriented programming (AOP). Based on the characteristics of AOP programs, we model security policies and a verification process using alternating temporal logic. This method can be used to verify whether a given program complies with a wide range of security policies, including both safety and liveness policies. It can also verify whether the original program is affected by policy execution. We argue that TBPA provides a suitable semantic framework for certifying code, and represents a step forward from trusted code toward trustworthy code.


Keywords


Trust, policy adherence, Aspect-oriented programming, Alternating Time Temporal Logic

References


TCG Specification Architecture Overview Specification Revision 1.4. https://www.trustedcomputinggroup.org/specs/IWG. 2007

Kiczales Gregor, Lamping J., Medhdhekar Anurag et al. “Aspect-Oriented Programming,” In: Proceedings of the 11th European Conference on Object-Oriented Programming, Finland. 1997, 1241pp.220–242.

Fred B. Schneider. “Enforceable security policies,” ACM Transactions on Information and Systems Security, 2000, vol. 3, pp.30–50.
http://dx.doi.org/10.1145/353323.353382

J. Ligatti, L. Bauer, D. Walker, “Run-Time Enforcement of Non-safety Policies,” ACM Transactions on Information and Systems Security, 2009, vol. 12, pp.19:1-19:41.

úlfar Erlingsson. “The Inlined Reference Monitor Approach to Security Policy Enforcement,” PhD thesis, Cornell University, Ithaca, New York. 2004.

Kevin W. Hamlen, Greg Morrisett, Fred B. Schneider. “Computability classes for enforcement mechanisms,” ACM Transactions on Programming Languages and Systems, 2006, vol. 28, pp.175–205.
http://dx.doi.org/10.1145/1111596.1111601

úlfar Erlingsson, Fred B. Schneider. “SASI enforcement of security policies: A retrospective,” In: Proceedings of the New Security Paradigms Workshop. Caledon Hills, Ontario, Canada, 1999, pp. 87–95.

Moonjoo Kim, Mahesh Viswanathan, Sampath Kannan etc. “Java-MaC: A run-time assurance approach for Java programs,” Formal Methods in System Design. 2004, vol.24, pp.129–155.
http://dx.doi.org/10.1023/B:FORM.0000017719.43755.7c

Irem Aktug, Katsiaryna Naliuka. “ConSpec: A formal language for policy specification,” In: Proceedings of the 1st International 18 Workshop on Run Time Enforcement for Mobile and Distributed Systems, Lecture Notes in Theoretical Computer Science, Dresden, Germany. 2007, pp. 45–58.

Chirs Allan, Paval Avgustinov, Aske Simon, etc. “Adding trace matching with free variable to AspectJ,” In: Proceedings of the 20th annual ACM SIGPLAN conference on Object oriented programming systems languages and applications (OOPSLA’5), 2005,40(10)

Lujo Bauer, Jay Ligatti, David Walker. “Composing security policies with Polymer,” In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. 2005, pp.305–314.

Oliveira, A.S.D., Wang, E.K., Kirchner, C., and Kirchner, H. “Weaving Rewrite-Based Access Control Policies,” 5th ACM Workshop on Formal Methods in Security Engineering. 2007, pp.71-80
http://dx.doi.org/10.1145/1314436.1314446

Kevin W. Hamlen, Micah Jones. “Aspect-Oriented In-lined Reference Monitors,” In: Proceedings of the ACM Workshop on Programming Languages and Analysis for Security, Tucson, Arizona, USA. 2008, pp.11-20.

Kiczales Gregor, Hilsdale E., hugunin J., kersten M., palm J., Griswold W. “An overview of AspectJ,” In Proc. of the European Conference on Object-Oriented Programming. 2001, pp.327–353.

Shriram krishnamurithi, kathi fisler. “Foundations of Incremental Aspect model-checking,” ACM Transactions on Software Engineering and Methodology, 2007, vol. 16, Article 7. Devereux B. “Compositional reasoning about aspects using alternating-time logic,” In Foundations of Aspect-Oriented Lang. 2003.

Rajeev. Alur, Thomas A. Henzinger, Orrna Kupferman. “Alternating-Time Temporal Logic,” Journal of the ACM. 2002, vol.49, pp.672–713.
http://dx.doi.org/10.1145/585265.585270

Rajeev. Alur, L.de Alfaro, R. Grosuz etc. “JMOCHA: A Model Checking Tool that Exploits Design Structure,” In: Proceedings of the 23rd International Conference on Software Engineering. 2001(ICSE’01), pp.8-35

Necula G. “Proof-Carrying code,” In:Jones N, Lee P, eds. proc of the POPL’97. New York: ACM Press, 1997, pp.106-119.

Necula, G P. Lee, “The design and implementation of a certifying compiler,” In: SIGPLAN, 2004, pp. 612–625.

Kevin W. Hamlen, Greg Morrisett, and Fred B. Schneider. “Certified in-lined reference monitoring on. NET,” In: Proceedings of the 1st ACM Workshop on Programming Languages and Analysis for Security, Ottawa, Canada. june 2006, pp. 7–15.

Irem Aktug, Mads Dam, Dilian Gurov. “Provably correct runtime monitoring,” Elsevier: The Journal of Logic and Algebraic Programming. 2009, vol. 78, pp.304–339.
http://dx.doi.org/10.1016/j.jlap.2008.12.002


Full Text: PDF


Journal of Computers (JCP, ISSN 1796-203X)

Copyright @ 2006-2012 by ACADEMY PUBLISHER – All rights reserved.