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 by J. Pavlich-Mariscal et al (2007) 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, 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.