[LINK] The Jeeves Programming Language

[stephen at melbpc.org.au]

Jeeves Programming Language 

 <http://www.newscientist.com> 25th January 2012 by Jacob Aron 



Researchers at the Massachusetts Institute of Technology have come up 
with a new programming language, called Jeeves, that automatically 
enforces privacy policies.

Programmers have to explicitly ensure data flowing through their software 
obeys necessary privacy policies, but it is easy to slip up and let 
information leak out. 

Jeeves solves that by substituting the value of variables within the 
software depending on who the user is. 

For example, say Alice posts a message but doesn't want anyone but 
herself to see who wrote it. The programmer can use the variable "author" 
without worrying what the user sees - when the software runs, Jeeves 
ensures Alice will see her own name, but everyone else logging in will 
see "Anonymous".

Jean Yang, who helped develop Jeeves, says the new language lets a 
programmer delegate privacy responsibilities and concentrate on the 
actual function of their code, much like a party host might entrust their 
butler with ensuring the needs of each guest are met so they can spend 
more time socialising ..

Jeeves Website:  <https://sites.google.com/site/jeevesprogramming/home>

It is becoming increasingly important for applications to not leak 
sensitive data. 

With current techniques, the programmer bears the burden of ensuring that 
the application's behavior adheres to policies about information flow. 
Unfortunately, privacy policies are difficult to manage because their 
global nature requires coordinated reasoning and enforcement.

To address this problem, we describe a programming model that makes the 
system responsible for ensuring adherence to privacy policies. 

The programming model has two components: core programs describing 
functionality independent of privacy concerns and declarative, 
decentralized policies controlling how sensitive values are disclosed 
depending on the context. The system is responsible for automatically 
ensuring outputs are consistent with the policies.

We have implemented this programming model in a new functional constraint 
language named Jeeves. 

In Jeeves, sensitive values are introduced as symbolic variables and 
policies correspond to constraints that are resolved at output channels. 
We have implemented Jeeves as an embedded domain-specific language in 
Scala using an SMT solver as a model finder.

Jeeves Programming Language

We present the Jeeves language, which allows the programmer provide 
privacy policies separately from the core program.  The programmer can 
introduce sensitive values into a core program written independently of 
policies, provide decentralized and declarative policies, and rely on the 
runtime system to automatically enforce the policies in the context of 
each output channel.

Implementation

We have implemented Jeeves as an embedded domain-specific language in 
Scala.  Our implementation supports symbolic evaluation of expressions 
containing sensitive values, stores a constraint environment to propagate 
policies, and uses the Z3 SMT solver to determine outputs consistent with 
policies.  Jeeves supports equality constraints on immutable integers, 
booleans, and objects.

The code is on Google code here: http://code.google.com/p/scalasmt/

We have a platform ScalaSMT for general-purpose constraint-based 
programming in Scala (browse here) ..

http://code.google.com/p/scalasmt/source/browse/#hg%2Fsrc%2Fmain%2Fscala

. and a more specialized Jeeves library on top of that (browse here) ..

<http://code.google.com/p/scalasmt/source/browse/#hg%2Fsrc%2Fmain%2Fscala%
2Fjeeves>
--

Cheers,
Stephen