DIFC Programs by Automatic Instrumentation

Decentralized information flow control (DIFC) operating systems provide applications with mechanisms for enforcing information-flow policies for their data. However, significant obstacles keep such operating systems from achieving widespread adoption. One key obstacle is that DIFC operating systems provide only low-level mechanisms for allowing application programmers to enforce their desired policies. It can be difficult for the programmer to ensure that their use of these mechanisms enforces their high-level policies, while at the same time not breaking the underlying functionality of the application. These are issues both for programmers who would develop new applications for a DIFC operating system and for programmers who would port existing applications to a DIFC operating system.

Our work significantly eases this task. We present an automatic technique that takes as input a program with no DIFC code, and two policies: one that specifies prohibited information flows and one that specifies flows that must be allowed. Our technique then produces a new version of the input program that satisfies the two policies. To evaluate our technique, we created an automatic tool, called SWIM (for Secure What I Mean), that implements the technique, and applied it to a set of real-world programs and policies. The results of our evaluation demonstrate that the technique is both sufficiently expressive to generate code for real-world policies, and that it can generate such code efficiently. It thus represents a significant contribution towards developing systems with strong end-to-end information-flow guarantees.

Download this report (PDF)

Return to tech report index