A framework of composable security features: Preserving separation of security concerns from models to code

Modeling of security and access control policies, along with their implementation in code, must be an integral part of the software development process, to ensure that the proper level of security in an application is attained. This dissertation proposes a framework for secure software design and coding. The base of the proposed approach is a set of security features, which are design components that realize specific security capabilities. Designers can select the features they require and compose them to yield a custom access control policy. To visualize security information, the framework provides a set of security diagrams, which are extensions to UML that depict security as a separate concern. The security design is transitioned into enforcement code that preserves separation of concerns. An essential property of the code is security assurance, to insure that the application code behaves consistently with the security policy. To provide security assurance, this dissertation formalizes the application behavior using labeled transition systems and structural operational semantics [82]. Simulation relations [64] are used to demonstrate the correctness of the secure code with respect to the design.