Skip to main content
Article
Faceted Execution of Policy-Agnostic Programs, Extended Version
UCSC-SOE-12-18 (2012)
  • Thomas H. Austin, University of California, Santa Cruz
  • Jean Yang, Massachusetts Institute of Technology
  • Cormac Flanagan, University of California, Santa Cruz
  • Armando Solar-Lezama, Massachusetts Institute of Technology
Abstract
It is important for applications to protect sensitive data. Even for simple confidentiality and integrity policies, it is often difficult for programmers to reason about how the policies should interact and how to enforce policies across the program. A promising approach is policy-agnostic programming, a model that allows the programmer to implement policies separately from core functionality. Yang et al. describe Jeeves, a programming language that supports information flow policies describing how to reveal sensitive values in different output channels. Jeeves uses symbolic evaluation and constraint-solving to produce outputs adhering to the policies. This strategy provides strong confidentiality guarantees but limits expressiveness and implementation feasibility. We describe a new language Jeeves* that provides the same guarantees while exploiting the structure of sensitive values to yield greater expressiveness and to facilitate reasoning about runtime behavior. We present a semantics based on Austin et al.'s faceted execution describing a model for propagating multiple views of sensitive values through a program. We provide a proof of termination-insensitive non-interference and describe how the semantics facilitate reasoning about program behavior.
Keywords
  • Faceted,
  • Policy-Agnostic programs,
  • Symbolic evaluation,
  • computer science
Disciplines
Publication Date
October 11, 2012
Publisher Statement
SJSU users: use the following link to login and access the article via SJSU databases
Citation Information
Thomas H. Austin, Jean Yang, Cormac Flanagan and Armando Solar-Lezama. "Faceted Execution of Policy-Agnostic Programs, Extended Version" UCSC-SOE-12-18 (2012)
Available at: http://works.bepress.com/thomas_austin/15/