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

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