Research › Language-Based Security

Language-Based Security and Verification

Programming languages are a powerful place to enforce security. We design type systems and static analyses that guarantee information-flow security, correct authorization, and secure multiparty computation at the level of source code, and we use SMT solvers and proof assistants to make those guarantees mechanical. Past work includes proof-carrying network code for software-defined networks and defense-in-depth for retrofitted software.

Faculty

Christian Skalka Director

Professor and Chair, Department of Computer Science

Joseph Near

Associate Professor, Department of Computer Science

Selected publications

arXiv 2026

Qoreo: Choreographic Programming for Quantum Distributed Systems

Jennifer Paykin, Steven Baldasty, Joseph Near, Christian Skalka

arXiv (preprint)
PLDI 2025

Efficient, Portable, Census-Polymorphic Choreographic Programming

Mako Bates, Shun Kashiwa, Syed Jafri, Gan Shen, Lindsey Kuper, Joseph Near

ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
ESOP 2025

SMT-Boosted Security Types for Low-Level MPC

Christian Skalka, Joseph Near

European Symposium on Programming (ESOP), pp. 258–285
PPDP 2024

Language-Based Security for Low-Level MPC

Christian Skalka, Joseph Near

International Symposium on Principles and Practice of Declarative Programming (PPDP)
TOPLAS 2023

Contextual Linear Types for Differential Privacy

M. Toro, David Darais, Chike Abuah, Joseph Near, D. Arquez, F. Olmedo, É. Tanter

ACM Transactions on Programming Languages and Systems (TOPLAS)
OOPSLA 2022

Solo: A Lightweight Static Analysis for Differential Privacy

Chike Abuah, David Darais, Joseph Near

ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)
CCS 2021

Zero Knowledge Static Program Analysis

Z. Fang, David Darais, Joseph Near, Y. Zhang

ACM Conference on Computer and Communications Security (CCS)
CSF 2020

Types and Abstract Interpretation for Authorization Hook Advice

Christian Skalka, David Darais, Trent Jaeger, Frank Capobianco

IEEE Computer Security Foundations Symposium (CSF)
OOPSLA 2019

Duet: An Expressive Higher-order Language and Linear Type System for Statically Enforcing Differential Privacy

Joseph Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, Dawn Song

ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA)

🏅 ACM SIGPLAN Distinguished Paper Award
CCS 2019

Proof Carrying Network Code

Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffen Smolka, Nate Foster

ACM Conference on Computer and Communications Security (CCS)

All publications in this area →

Related courses

Course	Description	Instructor
CS 3990 / CS 5990 Special Topics in Security and Privacy Language-Based Security	Rotating special-topics courses drawn from current research, such as Computer Security Foundations (language-based security, information flow, authorization logics) and Software Verification (proof assistants and certified software). Prerequisites: Varies	—

All security and privacy courses →

Funded projects

DARPA

TOPSPIN: Tools for Proving Security and Performance of Instances of Weird Networks

Provably Weird Network Deployment and Detection (PWND2) · 2025–2027 · UVM PIs: Christian Skalka, Joseph Near
DARPA

SALSA: Securing Antiquated Languages via Program Synthesis and Human Assistance

Small Business Innovation Research (SBIR) · 2022–2026 · UVM PI: Joseph Near
NSF

A New Approach to Federated Network Security (Proof Carrying Network Code)

SaTC: CORE: Small: Collaborative · CNS-1718083 · 2017–2022 · $212,872 · UVM PI: Christian Skalka · Collaborative with Cornell and RIT.
NSF

Retrofitting Software for Defense-in-Depth (STRATA)

TWC: Medium: Collaborative · CNS-1408801 · 2014–2019 · $299,243 · UVM PI: Christian Skalka

Work with us

Interested in language-based security? See how to join the Center as an MS, PhD, or undergraduate researcher.