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.

This project was a project I was working on with my first advisor at CU Boulder to detect web skimmers in the wild. Web skimmers are pieces of code on websites that look for sensitive user-information, such as credit card numbers, and send that information back to criminals. Web skimmers can be found on trustworthy websites, if the websites have flaws criminals can exploit, in addition to on phishing pages. Sophisticated malware is known to obfuscate its behavior or act benign if it believes it’s being observed. Any code that executes in a webpage is easy to detect, but code that executes in a browser is protected from direct observation by malware. For this reason, we put additional forensics capabilities into the Chromium browser so we could observe malicious code without being noticed. In particular, we adapted an exesting Chromium-based forensics engine (JSGraph) to capture the API calls that could be used to both explicitly and implicitly exfiltrate data. Our adaptations hook directly into the Blink rendering engine to record DOM manipulations and interactions with V8 including both javascript and webassembly code. We also investigated the use of taint tracking to identify when user input was being sent to an attacker.

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.