An aspect oriented approach for security hardening: Semantic foundations

Computer security is nowadays a very important field in computer science and security hardening of applications becomes of paramount importance. Aspect oriented programming (AOP) is a relatively new technology that allows separation of concerns such as security, synchronization, logging, etc. This increases the readability, understandability, maintainability, and security of software systems. Furthermore, AOP allows automatic injection of the crosscutting concerns into the application code using a weaving mechanism. This thesis comes to provide theoretical study of using AOP for security hardening of applications. The main contributions of this thesis are the following. We propose a comparative study of AOP approaches from a security perspective. We establish a security appropriateness analysis of AspectJ and we propose new security constructs for this language. Since aspects in AspectJ are weaved (combined) with the Java Virtual Machine Language (JVML) application code, we develop a formal semantics for the JVML. We propose also a semantics for AspectJ that formalizes the advice weaving. We develop a new AOP calculus, lambda_SAOP, based on lambda calculus extended with security pointcuts. Finally, we implement three new constructs in AspectJ, namely getLocal, setLocal , and dflow, for local variable accesses and data flow analysis. In conclusion, this thesis demonstrates the relevance, importance, and appropriateness of using the AOP programming paradigm in hardening the security of applications.