2010—2016 PhD Computer Science, Harvard University, 3.91

• Advisor: Stephen Chong
• Thesis: Software Contracts for Security

2008—2009 MSc Computer Science, University of Texas at Dallas, 3.96

• Graduate Information Assurance Program Certificate

2019—present Galois, Principal Scientist

Synthesizing Evidence of Emergent Computation (DARPA AIMEE)

• Applying program synthesis techniques to identify and mitigate exploitable vulnerabilities in system designs.

Computers and Humans Exploring Software Security (DARPA CHESS)

• Developing automated reasoning tools to decrease the time and expertise required to find and fix security vulnerabilities in large software projects.

Understanding and Programming Weird Machines (DARPA CFAR)

• Developed formal approach to characterizing emergent computational power arising from mismatches between high-level programs and their implementations.
• Developed prototype tools for embedding security monitors into programs via "weird machines."

2017—2018 Galois, Research Engineer

DARPA Cyber Fault-tolerant Attack Recovery (CFAR)

• Developed tooling to support the creation and debugging of diversified program variants using a diversifying compiler.
• Designed and implemented software diversification techniques for heap-allocated memory.

DHS Information Marketplace for Policy and Analysis of Cyber-risk & Trust (IMPACT)

• Implemented remote attestation TLS integration for Intel SGX-based secure data analysis platform.

2016—2017 Harvard University, Research Fellow with Stephen Chong

• Awarded Harvard Physical Sciences Accelerator funding to commercialize my research on Shill, a secure shell scripting language.

2010—2016 Harvard University, Research Assistant with Stephen Chong

Language-based authority control

• Designed a novel software contract framework for enforcing a wide range of access control mechanisms.

Integrating programming Language and operating system information security mechanisms

• Developed a secure shell scripting language that combines capability-based security, software contracts, and operating system mandatory access controls to provide strong, composable security guarantees for scripts and legacy programs.
• Investigated techniques for applying software contracts and information-flow types to increase the security of programs relying on capability-based security.

Accrue: providing language-based security guarantees proportional to programmer effort

• Designed a type system and enforcement mechanism that applied termination analysis to assure progress-sensitive information-security guarantees.
• Designed a type system and static program analysis to ensure the correctness of cryptographically enforced information erasure policies.
• Implemented an inter-procedural information-flow analysis for LLVM bitcode.

CHILI: enabling the execution of code of unknown origin while eliminating classes of security attacks

• Developed information flow and numerical abstract analysis frameworks for Java programs.
• Designed a sound technique for improving the efficiency of hybrid information-flow monitors using static analysis.

Summer 2012 SRI International Computer Science Laboratory, Research Intern with Ashish Gehani and Natarajan Shankar

• Developed a declarative specification language for collecting and integrating streaming provenance data.
• Developed prototype for system-wide tool for removing unnecessary functionality from binaries and system libraries.

2009—2010 Defense Information Systems Agency, Computer Scientist

• Performed project management and software architecture tasks for DoD-wide endpoint security program.
• Participated in DoD and NIST security architecture and standards working groups.

Summer 2006 IBM, Co-op Professional Programmer

• Developed test bed for high availability software, decreasing time required for regression testing from one week to one day.

2005—2007 University of Texas at Dallas, Mentor

• One-on-one mentoring with 2-3 computer science students per week.