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

Security Analysis for 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.

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.

System Assurance vis Real-World Semantics

One of my research directions focuses on the dependability of systems, by investigating a very general and comprehensive approach for enforcing safety and security constraints in computer systems like CPSs. It focuses on specifying and analyzing constraints that derive from the physical world through enriched specifications and enhanced error-checking techniques. Systems like CPSs interact with the real world in order to sense and affect it. They should obey rules inherited from the real world, e.g., laws of physics. To enforce these constraints, I develop rich semantic types and type systems to analyze the consistency of software logic with the real-world entities with which the logic interacts.