Verifying Information Flow Control Over Unbounded Processes
William R. Harris, Nicholas A. Kidd, Sagar Chaki, Somesh Jha, and Thomas Reps
Decentralized Information Flow Control (DIFC) systems enable
programmers to express a desired DIFC policy, and to have the policy
enforced via a reference monitor that restricts interactions between
system objects, such as processes and files. Past research on DIFC
systems focused on the reference-monitor implementation, and assumed
that the desired DIFC policy is correctly specified. The focus of
this paper is an automatic technique to verify that an application,
plus its calls to DIFC primitives, does indeed correctly implement a
desired policy. We present an abstraction that allows a model
checker to reason soundly about DIFC programs that manipulate
potentially unbounded sets of processes, principals, and
communication channels. We implemented our approach and evaluated
it on a set of real-world programs.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)