cv

Senior Software Engineer

Google Cloud

I lead the trust and transparency project for Google-vendored binaries in customer virtual machines. This includes a new code signing pipeline, standards body participation, and software supply chain integrity innovations.

• Transparency

Software Engineer

LogicBlox, Inc.

I wrote database query compilers and evaluators that improved common workloads by 1000x.

Software Engineering Intern

BMT SMS, Inc.

Wrote device drivers for statistics gathering and a standalone statistics visualization tool. Created an application for driving a 1 DoF robot with wave data to test monitoring equipment.

Software Engineering Intern

Microsoft Corp

Microsoft Office Sharepoint Server team. Wrote powershell apps and web modals for portal administration.

RATS working group member

Internet Engineering Task Force (IETF)

I contribute to the design and wording of the CoRIM and CMW formats as well and guideline documentation.

• Logical interpretation of profiles
• Issuance operational guidelines

PhD

Northeastern University

Programming Languages

B.S.

University of Texas at Austin

B.S., Pure Mathematics

B.S.

University of Texas at Austin

Computer Science

Pushdown flow analysis with abstract garbage collection

Journal of Functional Programming

In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection push the boundaries of what we can learn about programs statically. This work illuminates and poses solutions to theoretical and practical challenges that stand in the way of combining the power of these techniques. Pushdown flow analysis grants unbounded yet computable polyvariance to the analysis of return-flow in higher-order programs. Abstract garbage collection grants unbounded polyvariance to abstract addresses which become unreachable between invocations of the abstract contexts in which they were created. Pushdown analysis solves the problem of precisely analyzing recursion in higher-order languages; abstract garbage collection is essential in solving the “stickiness” problem. Alone, our benchmarks demonstrate that each method can reduce analysis times and boost precision by orders of magnitude.

Abstracting Abstract Control

DLS

The strength of a dynamic language is also its weakness: run-time flexibility comes at the cost of compile-time predictability. Many of the hallmarks of dynamic languages such as closures, continuations, various forms of reflection, and a lack of static types make many programmers rejoice, while compiler writers, tool developers, and verification engineers lament. The dynamism of these features simply confounds statically reasoning about programs that use them. Consequently, static analyses for dynamic languages are few, far between, and seldom sound.

Optimizing Abstract Abstract Machines

ICFP

This article contributes a step-by-step process for going from a naive analyzer derived under the abstracting abstract machine approach to an efficient program analyzer. The end result of the process is a two to three order-of-magnitude improvement over the systematically derived analyzer, making it competitive with hand-optimized implementations that compute fundamentally less precise results.

gce-tcb-verifier

Code-signing and verification tool for virtual firmware

• Confidential Computing

go-sev-guest

AMD SEV-SNP attestation report collection and verification.

• Confidential Computing