Formal Methods for System Security

Formal methods provide a rigorous, mathematically grounded analysis of a system. Used as part of a security analysis, formal methods can provide verification that a system meets its security requirements. In this course students will learn about and gain experience using a variety of techniques, including symbolic execution, model checking, and proofs of equivalence and refinement. Students will develop an understanding of different specification logics and what can and cannot be expressed in each. Topics include assertion-based verification, simulation relations, linear temporal logic, information flow analysis, and hyperproperties.