Research

Active Research Directions

Our group is currently investigating how the following two programming models can change the way people think about their respective domains, and facilitate the creation of programs and analyses that were previously difficult or impossible.

• Policy-agnostic programming for security and privacy. As an alternative to approaches for detecting information leaks, my collaborators and I 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. In our work on Jeeves we 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 and (2) techniques for retrofitting legacy code with the policy-agnostic model, for purposes of fixing bugs and interacting with new policies and code.
• Rule-based programming for biological modeling. 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.

Publications

Enforcing Information Flow Policies with Targeted Program Synthesis, Nadia Polikarpova, Jean Yang, Shachar Itzhaky, Travis Hance, and Armando Solar-Lezama. In submission. [Paper: arXiv]	Draft
A Trace Query Language for Rule-based Models, Jonathan Laurent, Hector F. Medina-Abarca, Pierre Boutillier, Jean Yang, and Walter Fontana. CMSB 2018. [Paper: pdf]	CMSB 2018
Counterfactual Resimulation for Causal Analysis of Rule-Based Models, Jonathan Laurent, Jean Yang, and Walter Fontana. IJCAI 2018. [Paper: pdf]	IJCAI 2018
A tool for automated inference in rule-based biological models, Chelsea Voss, Jean Yang, and Walter Fontana. Static Analysis in Systems Biology Workshop 2017. [Slides: pdf]	SASB 2017
Precise, Dynamic Information Flow for Database-Backed Applications, Jean Yang, Travis Hance, Thomas H. Austin, Armando Solar-Lezama, Cormac Flanagan, and Stephen Chong. Programming Language Design and Implementation 2016. [Paper: pdf | Slides: pptx pdf | Talk: YouTube | BibTex]	PLDI 2016
Preventing Information Leaks with Policy-Agnostic Programming, Jean Yang. PhD thesis. [pdf]	PhD thesis
Secure Distributed Programming with Value-Dependent Types, Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang. Journal of Functional Programming 23(4), July 2013. [BibTex]	JFP 2013
Faceted Execution of Policy-Agnostic Programs, Thomas H. Austin, Jean Yang, Cormac Flanagan, and Armando Solar-Lezama. Workshop on Programming Languages and Analysis for Security 2013. [Paper: pdf | BibTex]	PLAS 2013
A Language for Automatically Enforcing Privacy Policies, Jean Yang, Kuat Yessenov, and Armando Solar-Lezama. Principles of Programming Languages 2012. [Paper: pdf | Slides: pptx pdf | Talk: mp4 stream | BibTex]	POPL 2012
Secure Distributed Programming with Value-Dependent Types, Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bharagavan, and Jean Yang. International Conference on Functional Programming 2011. [Paper: pdf | BibTeX]	ICFP 2011
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Jean Yang and Chris Hawblitzel. CACM Research Highlight. Communications of the ACM, September 2010. [Full text: html pdf | Technical Perspective: html pdf | [BibTeX]	CACM 2010
Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System, Jean Yang and Chris Hawblitzel. Programming Language Design and Implementation 2010. Best Paper Award. [Paper: pdf | Slides: pptx pdf | related video | BibTeX]	PLDI 2010

Workshop Talks

Causal analysis of rule-based models through counterfactual reasoning, Jonathan Laurent, Jean Yang, and Walter Fontana. Static Analysis in Systems Biology Workshop 2016 (presentation only). [Slides: pdf]

Software Patents

Stephen C. Heise, Jean Yang, Dwayne Reeves, and Yiding Jia. Privacy verification tool. US20140282837 A1, filed March 15, 2013. [BibTeX]

Chris Hawblitzel and Jean Yang. Automated verification of a type-safe operating system. US8341602 B2, filed February 27, 2010 and issued December 25, 2012. [BibTeX]