Show simple item record

dc.contributor.authorHarris, Williamen_US
dc.contributor.authorKidd, Nicholasen_US
dc.contributor.authorChaki, Sagaren_US
dc.contributor.authorJha, Someshen_US
dc.contributor.authorReps, Thomasen_US
dc.description.abstractDecentralized 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. Current research on DIFC systems focuses on the reference monitor implementation, and assumes 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.en_US
dc.publisherUniversity of Wisconsin-Madison Department of Computer Sciencesen_US
dc.titleVerifying Information Flow Control Over Unbounded Processesen_US
dc.typeTechnical Reporten_US

Files in this item


This item appears in the following Collection(s)

  • CS Technical Reports
    Technical Reports Archive for the Department of Computer Sciences at the University of Wisconsin-Madison

Show simple item record