A compositional framework for access control policies enforcement

Despite considerable number of work on authorization models, enforcing multiple policies is still a challenge in order to achieve the level of security required in many real-world systems. Moreover current approaches address security settings independently, and their incorporation into systems development lifecycle is not well understood. This paper presents a formal model for the specification of access control policies. The approach can handle the enforcement of multiple policies through policies composition. Temporal dependencies among authorizations can be formulated. Interval Temporal Logic (ITL) is our underlying formal framework and policies are modeled as safety properties expressing how authorizations are granted over time. The approach is compositional, and can be used to specify other system’s properties such as functional and temporal requirements. The use of a common formalism eases the integration of security requirements into system requirements so that they can be reasoned about uniformly throughout the development lifecycle. Furthermore specification of policies are executable in Tempura, a simulation tool for ITL.