Paper Info
Title
Faceted execution of policy-agnostic programs
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 extend Jeeves with faceted values, which exploit the structure of sensitive values to yield both greater expressiveness and to facilitate reasoning about runtime behavior. We present a faceted semantics for Jeeves and describe a model for propagating multiple views of sensitive information through a program. We provide a proof of termination-insensitive non-interference and describe how the semantics facilitate reasoning about program behavior.
Year
DOI
Venue
2013
10.1145/2465106.2465121
PLAS
Keywords
Field
DocType
faceted semantics,faceted execution,faceted value,limits expressiveness,sensitive data,information flow policy,program behavior,greater expressiveness,sensitive information,sensitive value,policy-agnostic programming,privacy,security
Information flow (information theory),Programmer,Programming language,Confidentiality,Program behavior,Computer science,Communication channel,Exploit,Information sensitivity,Semantics
Conference
Citations 
PageRank 
References 
9
0.46
43
Authors
4
Name
Order
Citations
PageRank
Thomas H. Austin130715.96
Jean Yang21077.90
Cormac Flanagan32990181.36
Armando Solar-Lezama479159.48