UC Santa Cruz

This thesis aims to make progress on the problem of using dynamic information flow control for computer security at the application level, specifically using Faceted Values. This technique involves augmenting program data values so that each one is a pair of two primitive values:

one high-security version that is visible only to high-security observers, and one low-security version that is visible to everyone else. These augmented values are called faceted values, and the various versions are called facets. This technique allows very precise tracking of information flow through a program, allowing programmers to increase confidence in the security of their systems.

This thesis helps to increase the maturity of research on the ``Faceted Values'' technique, bringing it in line with research on the prior techniques ``No Sensitive Upgrades'' and ``Secure Multi Execution.'' Specifically, we have formalized a new semantics (called Multef) and proved that it satisfies a strong (``termination sensitive'') security property, we have implemented the technique as a Haskell library (called FIO) using two monads, and we have tested it in a prototype social network application (called FacetBook).