ABSTRACT
Virtualization is a key foundation for the cloud computing infrastructure we use every day. Cloud computing providers rely on commodity hypervisors to host and protect user applications and data in virtual machines, but their growing complexity poses a security risk as large codebases contain many vulnerabilities. Formal verification is increasingly being used to try to address this problem to prove the correctness of software, but this has been intractable in practice for commodity hypervisors due to their size and complexity. I will describe some recent work to address this challenge and some new techniques that make it possible for the first time to verify the security of the widely-used Linux KVM hypervisor.

BIO

Jason Nieh is a Professor of Computer Science and Co-Director of the Software Systems Laboratory at Columbia University. He has served as a consultant to both government and industry, including as the technical advisor to nine States on the Microsoft Antitrust Settlement, and as an expert witness before the US International Trade Commission. He was previously Chief Scientist of Cellrox and Desktone, acquired by VMware. Nieh has made research contributions across a broad range of areas, including operating systems, virtualization, computer architecture, thin-client computing, cloud computing, mobile computing, multimedia, web technologies, and performance evaluation. Technologies he developed are now widely used in major operating system platforms, including Android and Linux, and are built into ARM processors, billions of which ship each year.

Nieh is a Fellow of the ACM and IEEE. Honors for his research work include the Sigma Xi Young Investigator Award, awarded once every two years in the physical sciences and engineering, a National Science Foundation CAREER Award, a Department of Energy Early Career Award, five IBM Faculty Awards and two IBM Shared University Research Awards, six Google Research Awards, and various best paper awards, including those from MobiCom, SIGCSE, SIGMETRICS, and SOSP.

A dedicated teacher, he received the Distinguished Faculty Teaching Award for his innovations in teaching operating systems and for introducing virtualization as a pedagogical tool, which has become common practice at universities around the world.

Nieh earned his B.S. from MIT and his M.S. and Ph.D. from Stanford University, all in Electrical Engineering. He is married to Belinda Nieh and they have four children, Joanna, Caleb, Emma, and Zachary. They live in New York City.