Foundations of dynamic access control

Abstract

New commercial operating systems e.g., Windows 7 and 8, and research operating systems such as Asbestos and Flume, include labels for integrity/confidentiality protection. Unlike the strict Bell-LaPadula mandatory access controls, these labels are allowed to change in controlled ways by users and applications. The implications of these dynamic changes need to be examined carefully, and existing formalisms cannot express or help us understand their impact on access control safety. We present a logic-programming framework to specify, analyze and automatically verify such dynamic access control models. We study the problem of reachability (equivalently safety) in these models and show that they are undecidable in the general case. We also identify an expressive fragment of this formalism that has a sound and complete decision procedure. We build a theory (and tools) for reasoning about information-flow in the general context, and show its application on real-world use-cases.We are able to highlight several important vulnerabilities in these models, as well as suggest design changes that can be provably validated. © Springer-Verlag 2012.