Bridging the Gap Between People and Policies in Security and Privacy
Technical Report Identifier: EECS-2006-191
December 21, 2006
Abstract: The most powerful of security and privacy mechanisms may be rendered ineffective if people cannot use them. A common usability problem is that it is hard to specify the policies that the mechanisms enforce. Indeed, the more powerful the mechanism, the larger and more complex its policy can be; this makes it difficult not only to write a policy down, but also to make sure that an existing policy is a secure one.
In this dissertation, we make progress in addressing both these problems: translating people's high-level intentions into low-level policies and verifying that low-level policies meet high-level goals. To this end, we explore two application domains and their corresponding user bases.
For system administrators, we define a useful secure information-flow property, which we term CW-Lite. It says that untrusted processes should not be able to send unfiltered inputs to trusted processes. This is a basic security concern which can lead to system compromise, but it is unverified on most systems today because there is no effective, easy way to do the verification. A big advantage of our approach is that system administrators can perform a completely automated verification of CW-Lite using our tools, making it easier to integrate into a system.