I am currently pursuing a PhD in Computer Science at CU Boulder advised by Gowtham Kaki as part of the Programming Languages and Verification (CUPLV) lab. I am particularly interested in making it easier for developers to securely build products and protocols. I do this through using formal methods to prove that protocols actually provide the guarantees they aim for, or to fix protocols if they fall short. I am also interested in developing static analysis tools that alert developers to issues in their code before it’s released.
In my previous roles I’ve worked as a developer, administrator, architect, researcher, and user. From this experience I strongly believe that using program analysis tools, formal methods, and programming languages and frameworks with safeguards built in are the best way to ensure that we reach a future where users can trust products to protect their information and systems. My goal is to work towards this future through making these tools more accessible and accurate.
In my spare time I help run the CU Cybersecurity Club.
This is a personal project to build out an abstract interpreter written for and in Rust. I wanted to both get some experience working with Rust’s Mid-level Intermediate Representation as well as writing a library for abstract interpretation from scratch. Abstract interpretation is a method to perform sound over-approximate static analysis of a program. My implementation currently supports the interval and boolean abstract domains.
This project aims to allow protocol designers and developers to easily check if their protocol guarantees indistinguishability. In particular, it helps them check if the probability of generating any particular message trace (including both client and server messages) is equivalent under the assumption that a specified set of inputs are public knowledge. This property is also referred to as herd privacy in the context of Distributed Identity. This framework is useful for both toy protocols, such as showing that one-time pad encryption does not guarantee indistinguishability if keys are reused, and for production-grade protocols, such as showing that TLS ECH with some modifications guarantees indistinguishability. This project is meant to make it easier to prove specifications similar to those I used for my TLS ECH project. I am using F* and the Z3 SMT solver for this project.
The neural networks in use today are known to be vulnerable to adversarial attacks. In the case of networks used for computer vision, just slightly altering the pixels of the image can cause a neural network to observe a dramatically different object, even if the image looks exactly the same to a human. ERAN is a tool that can be used to evaluate how robust neural networks are to these small perturbations. For this class project, my partner and I created a sound relaxation for the Exponential Linear Unit (ELU) activation function in the DeepPoly domain, one of the abstract domains ERAN uses for its analysis. Our extension enables ERAN to verify the robustness of neural networks that use the common ELU activation functions. To the best of our knowledge, our extended version of ERAN is the first such framework to allow for verification of networks that use ELU functions.
Transport Layer Security (TLS) is a protocol that protects network traffic from observation and tampering. It is best known for its use in HTTPS, which stands for HTTP over TLS. Unfortunately, TLS, and by extension HTTPS, leaks information about what server a user is connecting to during its initial handshake. This information could be used by nation states to censor internet traffic or by an ISP to track a user’s browsing behavior for advertising purposes. TLS ECH is a proposed extension that aims to hide which server a user is connecting to from observers.
For this project I developed a formal specification of the TLS ECH specification. In the process, I discovered a known bug with the latest version of the specification: that server messages must be padded to a common length for the anonymity set. In this absence of this fix, it is trivially easy to distinguish which server a user is connecting to. I then adapted my specification to prove that my proposed fix allows TLS ECH to provide its primary security goal: that connection establishment to different backend servers in the same anonymity set is indistinguishable to an outside observer. The specification and verification proofs are done in F*.
Distributed systems are notoriously difficult to design correctly. Zookeeper is an important coordination service for several distributed systems used in industry including Spark and Hadoop. For a class, I created a formal specification of the Zookeper atomic broadcast protocol (Zab). I then validated the protocol using bounded model-checking. The specification was written using TLA+ and PlusCal.
When I was working as a consultant at Teradata, I frequently had to connect to Hadoop clusters through a secured proxy. Several Hadoop-related services have helpful dashboards complete with links to data throughout the cluster. This was a pain to work with when connecting through the secured proxies since the links would fail to resolve. I created this simple chrome extension to allow me to make a list of hosts that my browser would automatically redirect (to forwarded ports I’d opened using the proxy). It made using the Hadoops dashboards for these clusters much easier.
This project was an interdisciplinary senior design project involving two other computer engineering students and three mechanical engineering students. We were working on developing hardware and software that would allow an unmanned octocopter to take and analyze multi-spectral images of vineyards to detect plant stress. My part of the project focused on writing software to navigate around the vineyard, visually locate a docking station, and land the octocopter on the docking station. Our team received the best-in-session award, the highest award given for senior design projects.