My group works on programming-language-based approaches to improve the security and safety of large scale system software. More specifically, we build formally verified operating system kernels and hypervisors as well as novel secure enclaves with trusted (or certified) execution environments. We also work on making enclaves more scalable, efficient, and composable.

Before applying for this opportunity you need to submit your online profile. Click the button below to continue.