Speaker: Prasad Naldurg (Microsoft Research, India)

Title: Foundations of Dynamic Access Control

Abstract: In this talk, I will describe our work on understanding the foundations of dynamic access control. In contrast to traditional operating systems, new commercial operating systems e.g., Windows 7, and research operating systems such as Asbestos and Flume, include labels for integrity 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 a reasonably expressive fragment of this formalism that has a sound and complete decision procedure. We build a theory (and tool) based on bounded model-checking 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. I will conclude a small discussion on open problems in this framework and future work. This talk summarizes some of our work from FMSE 2006, CCS 2008, PLAS 2009 (best paper) and SACMAT 2011.