This talk is for general CS audience.

Paul Van Oorschot
Professor of Computer Science
Carleton University (Canada)

Host: Professor N. Asokan
Time: 14:15 (coffee at 14:00)
Venue: T3, CS building

Improving real-world systems security: is formal verification of software the answer?

Abstract:

Formal verification of software has enjoyed major successes recently, including as applied to the seL4 separation kernel and highly-visible work on TLS 1.3 (transport layer security, as used, e.g., by HTTPS in web browsers). More broadly, formal methods have been heavily promoted by some, including within major governments, as the way to make cybersecurity research “more scientific”.  We consider some simple questions related to formal verification. Do proofs about software properties translate into real-world security guarantees, or add value to practical systems? Do the models they are based on map to empirical environments? If one or more proof assumptions don’t hold in practice, what residual value remains? What side effects does formal verification impose on real systems; has cost-benefit analysis been considered? We aim to stimulate thought on how to bring formal methods into closer alignment with improving practical systems security.

Bio:

Paul Van Oorschot is a Professor of Computer Science at Carleton University in Ottawa, where he has been Canada Research Chair since 2002, following 14-years in industry at Bell-Northern Research and related companies. He is an ACM Fellow and a Fellow of the Royal Society of Canada. He was Program Chair of USENIX Security 2008 and NDSS 2001-2002, and co-author of the Handbook of Applied Cryptography (1996). He has served on the editorial boards of IEEE TDSC, IEEE TIFS, and ACM TISSEC.  His research interests include authentication and identity management, computer security, Internet security, security and usability, software security, and applied cryptography.