About This Item

Ask the MINDS@UW Librarian

Verifying Information Flow Control Over Unbounded Processes

Show full item record

File(s):

Author(s)
Haris, William; Kidd, Nicholas; Chaki, Sagar; Jha, Somesh; Reps, Thomas
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Date
Mar 15, 2012
Abstract
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. 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.
Permanent link
http://digital.library.wisc.edu/1793/60674 
Export
Export to RefWorks 
‚Äč

Part of

Show full item record

Search and browse




About MINDS@UW

Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.