A Language for Automatically Enforcing Privacy Policies

Abstract

It is becoming increasingly important for applications to protect sensitive data. Unfortunately, policies for confidentiality and integrity are difficult to manage because their global nature requires coordinated reasoning and enforcement. To mitigate this, we propose policy-agnostic programming, a model in which the programmer implements core functionality separately from privacy policies and relies on the runtime to automatically enforce the policies. We describe the Jeeves programming language, which allows programmers to define high- and low-confidentiality components of sensitive values along with declarative, context-dependent policies for the disclosure of these components. These sensitive values can be used interchangeably with other program values; the Jeeves runtime is responsible for producing the appropriate results of computations.

We have defined the semantics of Jeeves and proven a non-interference guarantee. We have implemented Jeeves as an embedded domain-specific language in Scala, using the Z3 SMT solver as a model finder. We have used this to implement a conference management system that interacts with a Scalatra frontend and a MySQL backend. In this talk I describe the Jeeves programming language, our experience using Jeeves, and our recent work in extending Jeeves to support integrity policies.

Bio: Jean Yang is a Ph.D. student at MIT working with Armando Solar- Lezama. She graduated from Harvard University in 2008 in Computer Science. She received the Best Paper Award at PLDI in 2010 for her paper "Safe to the Last Instruction: Automated Verification of a Type- Safe Operation System" with Chris Hawblitzel of Microsoft Research. She is a recipient of the NSF Graduate Research Fellowship and of the Facebook Fellowship