[an error occurred while processing this directive] [an error occurred while processing this directive] [an error occurred while processing this directive] [an error occurred while processing this directive] PhD Candidate [an error occurred while processing this directive] Stanford University [an error occurred while processing this directive] [an error occurred while processing this directive] [an error occurred while processing this directive] [an error occurred while processing this directive]

Operating Systems and Networking

Programming Systems

Security

[an error occurred while processing this directive] [an error occurred while processing this directive] I'm interested in systems security because small mistakes in the software we use every day can have devastating consequences, from the monetary---hackers used a Firefox browser zero-day to compromise Coinbase employees' machines---to the humanitarian---hackers attacked visitors to ``websites that focus on content related to the Uighur community'' using multiple Safari zero-days. Fortunately, tools like language design and verification can help developers write more correct software, but there are practical barriers to adopting these tools: many of them at least require re-writing code, and at worst require serious verification expertise. Re-creating verified versions of existing software, like the twenty-one-million line Firefox browser, is impractical---and the systems we rely on most reflect the efforts of many hundreds of people over decades and millions of lines of code. My research addresses this practical gap by re-imagining strong formal tools so that they're effective on huge existing systems. For example, one of my research projects, Sys, is the first system to scale symbolic execution to web browsers, through a new combination of symbolic execution and static analysis. Another, VeRA, applies automated verification to the Firefox just-in-time compiler (JIT), as the first verification DSL to handle the details of a real-world range analysis. Neither VeRA nor Sys require developers to re-write the browser.

VeRA automatically verifies routines written in a subset of standard C++, Sys is a lightweight bug finder, and both tools have uncovered serious browser security vulnerabilities. [an error occurred while processing this directive] I'm a PhD student at Stanford University advised by Dawson Engler (and working with Deian Stefan at UCSD). I'm interested in using techniques from programming languages to make systems more secure. [an error occurred while processing this directive] Personal home page [an error occurred while processing this directive] [an error occurred while processing this directive]