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 it is 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 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 with a small discussion on open problems in this framework and future work. This talk summarizes our work from FMSE 2006, CCS 2008, PLAS 2009 (best paper), and SACMAT 2011, as well as ongoing work.
Prasad Naldurg has been a researcher in the Security and Privacy Focus Area at Microsoft Research India since 2005. He received his Ph.D. in Computer Science from the University of Illinois at Urbana-Champaign in 2004. His research interests include formal methods and verification for security, programming languages and tools, privacy, and applied cryptography.