Research

Developed a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security; presented SCHERI, a new processor design within this framework; and formally proved that SCHERI provides end-to-end secure speculation guarantees under the constant-time policy.

Presented a transformation framework that rewrites cryptographic assembly programs to separate secret and public stack data, facilitating secure speculation using hardware taint tracking.

Presented a software-hardware co-design mitigation that strengthens ASLR against microarchitectural side-channel attacks.

Presented a novel BTB replacement policy that achieves near-ideal frontend processor performance for data center applications.

Characterized widely-used data center applications (e.g. MySQL, MongoDB, FFmpeg, Nginx) and predicted how these applications might evolve in the future to enable suitable hardware development early on.