It is increasingly important for applications to protect the privacy and security of data. Unfortunately, it is often non-trivial for programmers to enforce privacy policies. We have developed Jeeves to make it easier for programmers to enforce information flow policies: policies that describe who can see what information flows through a program. Jeeves allows the programmer to write policy-agnostic programs, separately implementing policies on sensitive values from other functionality.
To implement programs adhering to information flow policies in state-of-the art systems, programmers must write checks and filters across the program. Jeeves is the first language that aims to factor these checks and filters out of the program, allowing the programmer to write them once alongside the program. While there exist approaches for checking that programs do not leak information, they do not automatically manage these policy checks. To use an analogy to memory management, the other approaches do something like what valgrind does for finding memory leaks, while Jeeves is the equivalent of a memory-managed language, but for information flow policies.
Just like Wooster's clever valet Jeeves in Wodehouse's stories, the Jeeves runtime does the hard work, automatically enforcing the policies to show the appropriate output to each viewer.
Realizations of Policy-Agnostic Programming
In the last years, the work on policy-agnostic programming has spread beyond the Jeeves language. We have been working on the following policy-agnostic languages and frameworks:
- Jeeves, a language with dynamic support for policy-agnostic programs. Implemented as an embedded domain-specific language in Python--a Python library that uses overloading and dynamic source-rewriting to achieve the desired semantics.
- Jacqueline, a web framework that supports policy-agnostic programming for SQL database-backed application. Implemented on top of the Django Python web framework, using the Jeeves library.
- Lifty, a language and compiler that supports static type-driven repair for policy-agnostic programming. Implemented using Liquid Haskell, an extension of Haskell that supports decidably checked refinement types.
- Binah, a web framework that supports static type-driven repair across application code and database queries in a web framework. Programmers specify each policy once, and the framework is responsible for inserting check. The farmework can also infer policies from checks in the code. Implemented on top of the Yesod Haskell web framework, using Liquid Haskell.