My main research focus is in operating systems and security
with a concentration in how virtualization can help enable
novel security properties.
I am also interested in cryptography and implementing new
cryptographic tools in a practical setting.
See a full listing of my
Anon-Pass provide practical anonymity for users of
subscription services. It allows users to authenticate to
a service anonymously (i.e., prove the to service s/he
should be allowed access) without linking the current
access with any prior login. But at the same time, it
guarantees that if a user tries to log in more than once
at the same time, the service will be able to detect the
double use of a single credential.
InkTag is a virtualization-based architecture that gives
strong safety guarantees to high-assurance processes even
in the presence of a malicious operating system. We
introduce paraverification, a technique that simplifies
the InkTag hypervisor by forcing the untrusted operating
system to participate in its own verification.
Modern systems keep long memories and an adversary who
gains access to a Linux system can recover the contents of
applications' windows, audio buffers, and data remaining
in device drivers — long after the applications have
terminated. Lacuna is a system that allows users to run
programs in "private sessions." After the session is
over, all memories of its execution are erased.