I lead the Davis Automated Reasoning Group (DARG), a team of researchers developing tools and techniques for ensuring correctness of software. The use of software is prevalent in our daily lives, and is increasingly used in safety and security-critical systems. Software systems come in a variety of shapes and sizes, from firmware for IoT devices consisting of thousands of lines of code to operating systems consisting of millions of lines of code to deep neural networks with billions of parameters. Each such system has different performance, security, safety, and functional requirements. Our research develops theoretical formalisms as well as practical tools to tackle these challenges, with the goal of developing foundational research and transitioning it to industry to have real-world impact.

A short description of some of our research can be found below; more details can be found in the publications. Our software tools are available on GitHub. I discussed some of our projects as well as my research philosophy in Episode 7 of the Build Better Systems Podcast; interview was in Aug. 2020.

Analysis and Repair of Deep Neural Networks

Deep neural networks (DNNs) have become the state-of-the-art in a variety of applications including image recognition and natural language processing. Moreover, they are increasingly used in safety and security-critical applications such as autonomous vehicles. This project aims to improve our understanding of DNNs by developing techniques to analyze, verify, and repair them.

Related publications: PLDI 2021 TACAS 2021 SAS 2020 SRDM 2019 NeurIPS 2019

Related presentations:

Efficient Abstract Interpretation

Abstract interpretation is a general framework for expressing static program analyses. This project aims to improve the time and memory performance of abstract interpretation, specifically the fixpoint computation central to all abstract interpreters. Our research is used in two open-source abstract interpreters: NASA IKOS and Facebook SPARTA.

Related publications: SAS 2020 POPL 2020

Related presentations:

Neuro-Symbolic Program Analysis

Neuro-symbolic program analysis augments static program analysis with machine learning to find bugs in large systems software, such as the Linux kernel.

Related publications: OOPSLA Onward! 2020 FSE 2019 FSE 2018 ICSE 2018

Verified Measured Boot

Security attacks during boot are arguably the most difficult to defend against. Consequently, many systems deploy a secure boot protocol known as measured boot. Measured boot ensures that every layer of firmware/software is measured before booting, and that the measurements are reliably recorded for future verification.

Researchers have recently proposed a new architecture known as Device Identifier Composition Engine (DICE) for measured boot. Unfortunately, manual security analysis of a DICE implementation is challenging. DICE introduces complex cryptographic primitives such as key generation, key derivation, X.509 CSR and certificate generation in multiple layers of the firmware stack. This project aims to formally specify security properties for DICE and develop a fully verified DICE implementation satisfying these properties.

Related publications: USENIX Security 2021

Related presentations: DICE*: A Formally Verified Implementation of DICE Measured Boot at USENIX Security 2021.

Related software: DICE*