A framework of composable access control definition, enforcement and assurance

This paper proposes an approach for secure software design and coding; and, it provides a formal underpinning for security assurance, i.e., a proof that the generated code correctly realizes security specifications. The base of the proposed approach is a set of security features [17] that separate security concerns from the main design. To create specific access control models, designers can select the features they require, compose them, and represent them through security diagrams [17], i.e., extensions to UML to represent security concerns. These security specifications are then transitioned into aspect-oriented enforcement code. To provide security assurance, this paper formalizes the application behavior using labeled transition systems and structural operational semantics; and it uses simulation relations to demonstrate the correctness of the secure code.