Distributed Information Flow Control (DIFC) systems enable programmers to express desired information-flow policies, and enforce the policies via a reference monitor that restricts interactions between system objects, such as processes and files. Current research on DIFC systems focuses on the reference-monitor implementation, and assumes that the application correctly enforces the desired information-flow policy. The focus of this paper is a semi-automatic technique to verify that the application does indeed enforce the (high-level) policy. We perform a source-to-source transformation on an input C program, and then ask if the transformed program satisfies an LTL formula expressing the desired policy. The transformation soundly abstracts programs with a potentially unbounded number of processes and communication channels. We implemented our approach and evaluated it on a set of real-world programs.

(Click here to access the paper: PDF.)