Colloquium “Verification of Network Security Properties with NetKAT”
Invitation to a colloquium organized by the Department of Computer Science and research training group „Cybercrime and Forensic Computing“:
Tuesday, 13 July 2021, 18:15 CEST
online via Zoom: https://fau.zoom.us/j/93355339391
Lecturer:
Prof. Dr. Dexter Kozen, Cornell University, Ithaca, NY, USA
Title:
Verification of Network Security Properties with NetKAT
Abstract:
Networks have received widespread attention in recent years as a target for domain-specific language design. The recent emergence of software-defined networking (SDN) has led to the appearance of a number of programming languages that seek to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network.
NetKAT is a recently developed programming/specification language and logic designed for reasoning about packet-switching networks. NetKAT provides general-purpose programming constructs along with special purpose networking primitives for specifying routing behavior and encoding network topologies. In this talk I will introduce the NetKAT language and show how it can be used to specify and automatically verify network security properties such as access control, non-interference, waypointing, loop freedom, and other correctness properties, along with a verified compiler for translating NetKAT programs to hardware instructions for SDN switches.
Short Bio:
Dexter Kozen is a professor in Computer Science at Cornell University. He received his undergraduate degree from Dartmouth College in 1974 and his PhD from Cornell in 1977 and has been a member of the Cornell faculty since 1985. His research interests are in the design and analysis of algorithms, computational complexity theory, and logics and semantics of programming languages. He is the author of approximately 250 research articles and four books.
Dexter lives in Ithaca with his wife Frances, Managing Director of the Cornell Institute for Fiber and Fashion Innovation in the College of Human Ecology at Cornell. They have three sons. For leisure activities, Dexter enjoys music of all types, but especially modern rock. He also enjoys sports, especially rugby, ice hockey, and skiing.