Foundations of access control for secure storage

Over the years, formal techniques have played a significant role in the study of secure communication. Unfortunately, secure storage has received far less attention. In particular, the uses and consequences of dynamic access control for security in file systems, operating systems, and other distributed systems are seldom well-understood. In this dissertation, we develop and apply formal techniques to understand the foundations of access control for security in such systems. Our case studies include the security designs of some state-of-the-art storage systems and operating systems. Our techniques are derived from ideas in programming languages and logic.