Specifying and Verifying Dynamic Information Flow Properties

David Sands
Chalmers University of Technology, Sweden

Security is rarely a static notion. What is considered to be
confidential or untrusted data varies over time according to
changing events and states. The static verification of secure
information flow has been a popular theme in recent programming
language research, but information flow policies considered are
based on multilevel security which presents a static view of
security levels. In this talk we provide a road map of the main
directions of current research, and introduce a simple mechanism
called flow locks for specifying dynamic information flow policies,
and a type-and-effect system for statically verifying flow lock
policies. We show that this simple mechanism can represent a
number of recently proposed information flow paradigms for
declassification.

Describing joint work with Niklas Broberg