Stella Lau
MIT
stellal@csail.mit.edu
Bio
Stella Lau is a Ph.D. candidate in the Programming Languages and Verification Group at MIT CSAIL where she is advised by Adam Chlipala. Her research integrates programming languages, formal methods, computer security, and computer architecture. Her thesis work focuses on ruling out bugs at the hardware-software interface by applying formal methods to hardware designs to provably achieve security properties such as isolation and confidentiality. Previously, Stella received her B.A. and M.Eng from the University of Cambridge, where she worked with Peter Sewell, Timothy Griffin, and Marcelo Fiore. She has interned at Google, Jane Street, Facebook, and Microsoft Research.
Areas of Research
- Programming Languages
Verifying secure hardware support for confidentiality and integrity
We often want to run security-critical code on the same machine as untrusted code without leaking secrets. We can decompose this problem into two parts: i) attackers should neither be able to obtain secrets from nor interfere with security-critical code due to being physically colocated on the same machine and ii) security-critical code should not itself leak secrets when executing independently on its own machine. Traditionally, programmers rely on architectural process isolation provided by primitives such as virtual memory and context switching to achieve i) and constant-time programming techniques to achieve ii). However, the isolation and constant-time guarantees that can be enforced with commodity hardware are too weak: microarchitectural timing side channels are exploited to extract secrets from both colocated processes and code traditionally deemed constant-time. Despite years of mitigations, new attack vectors continue to be discovered. My research aims to eliminate leakages at the hardware-software boundary by applying formal methods to provably achieve security properties such as isolation, integrity, and confidentiality. For i), we developed a specification and verification methodology for strong timing isolation to rule out, with machine-checked proof, interference across hardware security domains. We verified that a multicore, pipelined RISC-V processor securely implements strong timing isolation. Ongoing work involves connecting the isolation guarantee with hardware-software contract guarantees about cryptographic, constant-time programs to address ii) and obtain end-to-end confidentiality and integrity guarantees spanning the hardware-software stack.