Research
Research Vision. PAWSSEC (Provable Assurance for Whole-System Security) is a long-term research vision for achieving end-to-end, machine-checked security guarantees across the computing stack, from programming languages and compilers to systems and hardware.
My research lies at the intersection of programming languages, formal verification, compiler technology, and systems security. I develop mathematical foundations and practical tools for building software whose correctness and security properties can be established rigorously and preserved across different layers of the software stack. My work spans language design, verified compilation, systems software, and emerging applications of formal methods to AI systems.
Programming Languages
Programming languages provide the foundation for building reliable and secure software. My research develops verification-friendly programming languages, formal semantics, and type systems that make correctness and security properties explicit and amenable to machine-checked verification.
Representative Projects
- BeePL. A verification-friendly language and verified compilation framework for Linux eBPF.Publications:PriSC 2025,arXiv
- Jasmin. A verification-oriented programming language for high-performance cryptographic software. My research extends its formal foundations through structured leakage models, fine-grained constant-time policies, and verified compilation that preserves security guarantees.
- λir. A language with intensional receive.Publications:Master's thesis
Verified Compilation and Toolchains
Modern software relies on complex compilation toolchains where correctness and security guarantees established at the source level can be compromised by compiler transformations or supporting infrastructure. My research develops verified compilation techniques and formally verified toolchains that preserve these guarantees throughout the software build process, from compilation to linking, loading, and code generation.
Representative Projects
- BeePL.A verification-friendly language for Linux eBPF with a formally verified compilation path through CompCert.Ongoing work
- Structured Leakage.A formal framework for describing program leakage in a structured way and relating leakage across source and target languages. It provides the semantic foundation for reasoning about cryptographic constant-time security and its preservation through compilation.Publications:CCS 2021
- Fine-Grained Constant-Time Security.Extending structured leakage with fine-grained leakage models that account for cache-line observations and variable-time instructions. The work provides source-level verification and a formally verified compilation infrastructure that preserves constant-time security for the selected leakage model.Publications:CCS 2022
- Verified Linking and Loading.Developing machine-checked linkers and loaders that preserve the semantics and security properties established during compilation, extending formal assurance from compiled components to executable programs.Ongoing work
Formal Methods for AI Systems
Large language models and autonomous agents introduce new challenges for correctness, security, and reliability. I am exploring how ideas from programming languages, compiler technology, and formal verification can provide principled foundations for AI systems through structured prompt representations, policy enforcement, and verification techniques for agentic workflows.
Representative Projects
- Verified Prompt Compilation.Compiler-inspired frameworks for systematically improving the correctness, safety, and reliability of natural language prompts through formal intermediate representations and verified transformations.Ongoing work
- AgentFlow.A formal authorization framework for AI agents based on information flow, security labels, and path-sensitive policies, enabling formal reasoning about secure agent interactions and policy enforcement.Ongoing work