A method for certifying code in trust-by-policy-adherence

作者：Zeng Guo Sun^*; Li Li

来源：Journal of Computers, 2011, 6(8): 1691-1698.

DOI：10.4304/jcp.6.8.1691-1698

• Alternating temporal logic
• Alternating time temporal logic
• Aspect-oriented
• Liveness
• Model security
• Policy adherence
• Security policy
• Semantic framework
• Trust
• Verification process

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, includingb 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.

• 出版日期2011
• 单位同济大学