Research Directions

Quick Note: This page presents a short summary of my recent research directions. At the end of each section, I list some of the projects that I am currently working on, or potential projects I am going to explore. Happy to chat more if you are perspective students who are interested in working on these projects.

Overview

The primary goal of my research is to advance the state of the art of formal methods for correctness and security of computer systems, especially cyber-physical systems (CPSs), and to develop tools and techniques to help construct systems that are correct and secure. Many computer systems are safety and security critical. Systematic, correct, and secure system design and implementation are urgently needed, and I believe that rigorous formal methods are essential for substantial improvements. They enable reasoning from logical or mathematical specifications of the behaviors of computer systems and offer rigorous proofs that all system behaviors meet some desirable properties. Formal methods are crucial for security goals, because they can show that no attack (with assumptions) will cause a system to misbehave. My research approach is to investigate sound, powerful, and pragmatic formal reasoning techniques for safety and security properties, and develop efficient enforcement mechanisms of these properties in constructing practical systems

Quantitative Safety and Security Analysis of Cyber-Physical Systems

A major piece of my research is to develop fundamental concepts and methodologies for secure design and implementation of Cyber-Physical Systems (CPSs). CPSs, which interact continuously with the physical world, raise significant challenges for formal methods. Security and privacy models for CPSs have to be aware of the interaction between software systems and physical dynamics; enforcement of security properties requires us to go significantly beyond the state-of-the-art in the CPSs area. I introduce frameworks for modeling and analyzing attacks on CPSs. The frameworks often introduce a threat model of attacks, formalization of security properties, and techniques developed for reasoning with the security properties.

Specifying quantitative safety and tolerance

Real CPS rarely satisfy a binary notion of safety; they operate with margins, tolerate bounded sensor error, and degrade gracefully under attack. I develop formal notions that make these quantitative aspects precise — quantitative safety, robustness under attack, and attack tolerance over time.

  • HSCC’23 — sensor-attack robustness
  • CSF’25 — timed quantitative safety and tolerance
  • NFM’26 — tolerance contracts for sensors

Verifying quantitative properties relationally

The technical core of my work is relational verification: establishing a quantitative property of one system by relating its behavior to another (a reference, a nominal model, or an uncompromised version of itself). This includes forall-exists relational reasoning, simulation-distance techniques, and proof systems for CPS models expressed in differential dynamic logic.

  • CSF’21 — boolean robustness under sensor attacks
  • NAHS’25 — measuring robustness under sensor attacks
  • NFM’25 — relational reasoning for dynamical logics
  • CSF’25 — a proof calculus for forall-exists timed properties

Verified artifacts

I mechanize key results in the Lean 4 proof assistant, so that the formal guarantees are machine-checked rather than argued on paper. These artifacts include a from-scratch formalization of the underlying dynamical logic, the quantitative-safety and simulation-distance results, and a mechanized audit of a relational proof calculus.

Language-based Approaches for Application Security

Another piece of my research uses abstractions from programming languages to specify and enforce security properties, such as secure information flow, in software systems. The correctness and security of applications often rely on correctly enforcing appropriate restrictions on sensitive information. The main challenge is finding the right abstractions to enable formal methods for security, in particular, abstractions to present to the programmers, e.g., useful sets of formally defined, composable, verifiable, and high performance security primitives.

  • S&P’21 — Dynamic IFC for Java-like languages