Master’s Thesis Defense: Mark Nelson, 11/27, ASECO Lab

Friday, October 27th at 1:00pm in POST 311 (ASECO Lab).

Analysis of Secure Boot, OpenFlow and Intel SGX Protocols using Actor Network Theory
Mark Nelson

Why do we still publish insecure protocols and defective software? We’ve been at this for nearly 50 years and we continue to create systems that are inherently insecure. To motivate formal methods, this thesis will develop a historical perspective of the science of safety and apply the lessons learned to high-technology. Then, it will extend a modeling technique uniquely suited for studying complex systems, using set theory as a formal method to examine security claims. We have adopted the name Actor Networks for the organization, usage and methodology of this method. Finally, we will use this methodology to model three complex protocols: Secure boot, OpenFlow and Intel SGX.

Thesis Committee:
Peter-Michael Seidel, Chair
Dusko Pavlovic
Yingfei Dong