Protecting Information under Dynamic Policies: Specification, Conditions and Enforcement

Sammanfattning: Information-flow control enforces security policies on the information handled by computer applications. These policies often contain dynamic aspects, specifying how the confidentiality and integrity of information changes over time. This thesis focuses on the enforcement of such dynamic policies. The contributions are divided into three parts. Firstly, we need a means to specify our dynamic concerns in a manner that can be understood by a computer. The thesis builds on the Paralocks language as a suitable specification mechanism for such dynamic policies. Secondly, having specified a dynamic policy we require an understanding of what it means for a program to comply with that policy. The thesis identifies and addresses several of the challenges that the dynamic nature of policies introduces. Finally, given a policy specification and a definition of policy compliance, we explore how we can mechanically verify this compliance on programs. The thesis discusses two approaches: one static, using a type system, and one dynamic, using a run-time monitor.