The **P**rogramming **LA**nguages, **I**nformation security and **D**ata privacy (PLAID)
research lab at UVM.

##### Faculty #####

[Chris Skalka](http://www.cs.uvm.edu/~ceskalka/)  
[David Darais](http://david.darais.com)  
[Joe Near](http://www.uvm.edu/~jnear/)  

##### PhD Students #####

Chike Abuah  
John Ring  
Krystal Maughan  
Ryan Estes  

##### MS Students #####

Duncan Enzmann  
Kristin Mills  
Sam Clark  

##### BS Students #####

Alex Silence  
Jacob Wunder  
Phillip Nguyen  

##### Courses #####

Compilers  
Computer Networks  
Computer Security Foundations  
Data Privacy  
Programming Languages  
Software Verification  
Type Theory  

-------------------------------------------------

#### Recent Papers by UVM PLAID ####

- **A Language for Probabilistically Oblivious Computation.**  
  David Darais, Ian Sweet, Chang Liu, Michael Hicks.  
  *Principles of Programming Languages (POPL). ACM, 2020.*  

- **Proof Carrying Network Code.**  
  Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle
  Diller, Steffan Smolka, Nate Foster.  
  *Computer and Communications Security (CCS). ACM, 2019.*

- **Duet: An Expressive Higher-order Language and Linear Type System for
  Statically Enforcing Differential Privacy.**  
  Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu,
  Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song.  
  *Object-oriented Programming, Systems, Languages, and Applications (OOPSLA). ACM, 2019.*  
  ***«ACM SIGPLAN Distinguished Paper Award»***

- **Data Capsule: A New Paradigm for Automatic Compliance of Data Privacy
  Regulations.**  
  Lun Wang, Joseph P. Near, Neel Somani, Peng Gao, Andrew Low, David Dao, and
  Dawn Song.  
  *Workshop on Polystore Systems (POLY). Spriner, 2019.*

- **Towards Practical Differentially Private Convex Optimization.**  
  Roger Iyengar, Joseph P. Near, Dawn Song, Om Thakkar, Abhradeep Thakurta, Lun
  Wang.  
  *IEEE Security and Privacy (IEEE S&P). IEEE, 2019.*

- **Constructive Galois Connections.**  
  David Darais, David Van Horn.  
  *Journal of Functional Programming (JFP). Cambridge University Press, 2019.*

- **Tracking the Provenance of Access Control Decisions.**  
  Frank Capobianco, Christian Skalka, and Trent Jaeger.  
  *Workshop on Theory and Practice of Provenance (TaPP). USENIX Association, 2017.*

- **On Risk in Access Control Enforcement.**  
  Giuseppe Petracca, Frank Capobianco, Christian Skalka, and Trent Jaeger.  
  *Symposium on Access Control Models and Technologies (SACMAT). ACM, 2017.*

- **Life on the Edge: Unraveling Policies into Configurations.**  
  Shrutarshi Basu, Nate Foster, Hossein Hojjat, Paparao Palacharla, Christian
  Skalka, and Xi Wang.  
  *Architectures for Networking and Communications Systems (ANCS). ACM, 2017.*

-  **In-Depth Enforcement of Dynamic Integrity Taint Analysis.**  
  Sepehr Amir-Mohammadian and Christian Skalka.  
  *Workshop on Programming Languages and Security (PLAS). ACM, 2016.*

-------------------------------------------------

#### Industry Partnerships ####

###### *AI in the OODA Loop* ######

The OODA loop is a decision making process that is commonly used in Security
Operations Centers (SOCs), among other contexts. The goal of this project is to
investigate AI support for this process in cloud SOCs, to improve recall,
precision, and efficiency in identifying legitimate security threats. This
project is an industry collaboration with Threat Stack Inc., and is supported
by the Threat Stack Fellowship.

*UVM PIs: Chris Skalka, Joe Near. Funded by the UVM Threat Stack Fellowship.*

#### Funded Projects ####

###### *Verified Analyzers for Critical Software* ######

The reliability of a complete software system hinges on the reliability of each
tool used to construct it. Among these tools are program analyzers, as used
both internally by compilers for program optimization, and externally by
developers to eliminate software defects. In this project we investigate both
formal verification and automated synthesis of program analyzers using
interactive proof assistants. We first embed a new correctness framework in a
proof assistant, then we exploit calculational properties of the framework to
enable synthesis, and finally we apply the approach to applications in software
security. Our results will both accelerate existing approaches for designing
high assurance analyzers, as well as enable developers without expertise in
formal verification to prototype them. 

*UVM PIs: David Darais. Funded by NSF award CCF-1901278.*

###### *Languages for Secure Multiparty Computation* ######

Secure computation tools can enable new paradigms, such as publicly auditing
that queries for the PII of US citizens are in compliance with a court order
while hiding the queries made, or outsourcing network-threat analysis while
keeping details of the network secret. However, use of secure computation tools
is limited: (1) it takes too long; (2) one solution may not meet new
application needs; (3) it requires domain experts to design, prove secure, and
implement a solution; and (4) it is difficult to convey the security guarantees
to non-experts. We will close this gap by building a system, called PANTHEON,
that transforms the description of a computation involving sensitive data into
a cryptographically secure, “end-to-end” solution that satisfies specified
security goals. PANTHEON will greatly expand the number of programmers capable
of developing secure-computation protocols, and the number of users who will
benefit from their deployment.

*UVM PIs: David Darais. Funded by IARPA (HECTOR).*

###### *Languages for Differential Privacy* ######

Differential privacy is a promising framework for analyzing data while
providing formal privacy guarantees. Today, implementing
differentially private algorithms is an error-prone process: incorrect
algorithms don't crash; instead, they appear to function correctly,
but don't actually protect privacy. In this project, we invent new
programming languages capable of automatically verifying that an
algorithm satisfies differential privacy, enabling non-experts to
quickly develop correct differentially private algorithms.

*UVM PIs: Joe Near. Funded by DARPA (Brandeis).*

###### *Proof Carrying Network Code (PCNC)* ######

The goal of this collaborative project is to support formally well-defined
security guarantees in software defined networks (SDNs) involving multiple
security domains (federations).

*UVM PIs: Chris Skalka. Funded by NSF SaTC award CNS-1718083.*

###### *STRATA* ######

An integrative approach to defense in depth. This multi-institutional research
project seeks to combine authorization, isolation, information flow, and
auditing in a uniform framework. At UVM we are focused on mathematically
well-founded approaches to auditing. 

*UVM PIs: Chris Skalka. Funded by NSF SaTC award CNS-1408801.*