Active Projects

Our group is currently interested in programming language design, program analysis, and software verification problems associated with two programming models:

Policy-agnostic programming for security and privacy

As software that handles sensitive information becomes increasingly complex, there is growing programmer burden in managing policy spaghetti, functionality intertwined with policy. To address the issue of programmer burden, we propose a new programming model that factors out the specification of security and privacy concerns from the rest of the program and enforces the properties by construction. We have designed a language semantics for policy-agnostic programming with informaton flow policies and developed dynamic and static enforcement techniques. We are currently interested in (1) extending the approach for statistical privacy, (2) techniques for enforcing policy-agnostic programming through sound program repair for both strongly statically typed and dynamically typed languages, and (3) techniques for retrofitting legacy code with the policy-agnostic model, for purposes of fixing bugs and interacting with new policies and code.

AutoType  

A technique for automatically inferring high-level information flow predicates from potentially buggy code, based on refinement type inference. This is related to the Lifty and Jifty projects.

 

Binah  

A web framework that uses liquid types, decidable refinement types, for enforcing expressive properties across application code and database queries. We are working on both enforcing Binah code for information flow security properties and rewriting Binah application code and database queries to enforce these policies. Binah is based on the Lifty language and implemented using Haskell and Liquid Haskell on top of the Yesod web framework.

With Ranjit Jhala (UCSD), Nadia Polikarpova (UCSD), and Niki Vazou (UMD).

[wiki]

Jacqueline  

A approach for precise, dynamic enforcement of high-level information flow security policies across the application and database. Supports policy-agnostic programming by using the Jeeves runtime. Implemented in Python on top of the Django web framework.

With Thomas H. Austin (San Jose State), Armando Solar-Lezama (MIT), Cormac Flanagan (UCSC), and Stephen Chong (Harvard).

[paper] [code]

Jagger  

Applying policy-agnostic programming to asynchronous dependency injection. We are taking the Jeeves semantics and mapping them onto Dagger, Google's open source static dependency injection framework. We are interested in the practical issues involved with getting the policy-agnostic semantics to work in production settings.

 

Jifty  

A solution for using refinement types to verify high-level information flow policies in JavaScript code. The eventual goal is to support policy-agnostic programming in JavaScript through mostly static program repair. We are implementing Jifty on top of the Flow type checker.

With Avik Chaudhuri (Facebook) and Panagiotis Vekris (Facebook).

 

Jeeves  

A dynamic semantics that supports the automatic enforcement of high-level predicates for information flow security through simulating simultaneous multiple executions. Policies may depend on state and the sensitive values they protect. Implemented as an embedded domain-specific language in Python.

With Kuat Yessenov (formerly MIT), Armando Solar-Lezama (MIT), Thomas H. Austin (San Jose State), and Cormac Flanagan (UCSC).

[project page] [code]

Jostle  

A framework that supports privacy-agnostic programming by exposing fine-grained algorithmic choice and dynamically analyzing privacy and accuracy tradeoffs.

With Matt Fredrikson (CMU).

 

Lifty  

A strongly statically typed language that supports the specification of high-level, state-dependent information flow security predicates using liquid types, decidable refinement types. Lifty statically supports Jeeves's policy-agnostic programming semantics through type-based program repair. Implemented using Liquid Haskell.

With Nadia Polikarpova (UCSD), Shachar Itzhaky (Technion), and Armando Solar-Lezama (MIT).

[draft] [code]

Rule-based modeling for intracellular signalling

Traditionally, researchers model intracellular signalling using systems of ordinary differential equations (ODEs), but there are two problems with ODE models. First, a precise model requires a different ODE for each interaction between agents, causing ODE models to scale poorly with respect to number of agent types. Second, ODE models have little structure that we can exploit for scale-mitigating analyses. As an alternative, rule-based languages allow the representation of models as programs describing rewrites over graphs, where nodes correspond to proteins and edges describe protein complexes. Not only are these programs more concise than the corresponding ODE systems, but their structure also supports various analyses that are otherwise not possible. Our current work focuses on analyzing causal relationships between rules, and combining causal information with language design and model-checking techniques to create biologically relevant model analyses.

Counterfactual Analysis for KaFlow  

Dynamic causal analysis for Kappa programs to general causal stories, with the goal of producing summaries that are 1) minimal, 2) unique, and 3) faithful to biological intuitions.

With Jerome Feret (ENS), Jean Krivine (CNRS), and Walter Fontana (Harvard Medical School).

[code][slides]

KaFlow  

Dynamic causal analysis for Kappa programs to general causal stories, with the goal of producing summaries that are 1) minimal, 2) unique, and 3) faithful to biological intuitions.

With Jerome Feret (ENS), Jean Krivine (CNRS), and Walter Fontana (Harvard Medical School).

[code]

TQL  

A language for querying patterns in simulation trajectories for Kappa.

[code][documentation]

KaStat  

Statistical testing for Kappa to estimate the probability the probability of two rules holding a given type of influence relationship. Also calculates the frequencies of causal stories contributing to a given relationship.

With Jean Krivine (CNRS).

 

Syndra  

An inference engine for navigating knowledge representations about rule-based biological models, based on first-order logic. Detects redundancies and inconsistencies.

With Walter Fontana (Harvard Medical School).

[code][slides]