Flexible Information-Flow Control

Due to the pervasiveness of untrusted code handling sensitive
information, information leaks in programs pose a high risk of unwanted
data disclosure. While information-flow control techniques provide
strong guarantees, they are not widely used in practice. Conversely more
light-weight techniques such as taint tracking lack formal guarantees
and analysis.

To address this, we investigate more permissive techniques with weaker
guarantees: Taint tracking is widely used, but hard to capture formally.
We present a formal security definition of the security property it
enforces and explore a new enforcement method based on the faceted
values technique. Additionally, we establish a connection between the
security notions of opacity and noninterference. To make fully-fledged
information-flow control easier to use, we present an approach to
secure database-backed applications using homogeneous meta-programming
to secure applications combining server-side code, client-side code, and
database interactions.