NetKAT: A Formal System for the Verification of Networks

Cray Distinguished Speaker Series
October 17, 2016 - 11:15am to 12:15pm
Cornell University
Keller 3-180
Gopalan Nadathur

ABSTRACT: Networks have received widespread attention in recent years as a target for domain-specific language design. The emergence of software-defined networking (SDN) as a popular paradigm for network programming has led to the appearance of a number of SDN programming languages that seek to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network. Recent work by Anderson et al. (POPL 14) and Foster et al. (POPL 15) introduced NetKAT, a language and logic for reasoning about packet-switching networks. NetKAT provides general-purpose programming constructs such as parallel and sequential composition, conditional tests, and iteration, as well as special purpose primitives for querying and modifying packet headers and encoding network topologies.

In contrast to competing approaches, NetKAT has a formal mathematical semantics and an equational deductive system that is sound and complete over that semantics, as well as an efficient decision procedure. It is based on Kleene algebra with tests (KAT), an algebraic system for propositional program verification that has been extensively studied for nearly two decades. Several practical applications of NetKAT have been developed, including algorithms for testing reachability and non-interference and a correctness proof for a compiler that translates programs to hardware instructions for SDN switches. In this talk I will present a survey of this recent work.

BIO: Dexter Kozen is the Joseph Newton Pew, Jr. Professor in Engineering at Cornell University. He received his undergraduate degree from Dartmouth College in mathematics in 1974 and his PhD from Cornell in computer science in 1977. After working as a member of the research staff at the IBM Thomas J. Watson Research Center for several years, he returned to Ithaca to join the Cornell faculty in computer science in 1985. He is a former Guggenheim fellow and a fellow of the Association of Computing Machinery, the American Association for the Advancement of Science, and the European Association of Theoretical Computer Science. He is a recipient of the John G. Kemeny Prize in Computing, an IBM Outstanding Innovation Award, the 2016 EATCS Award, and the 2016 IEEE Computer Society McDowell Award. Kozen's research interests span a variety of topics on the boundary of computer science and mathematics: design and analysis of algorithms, computational complexity theory, complexity of decision problems in logic and algebra, and logics and semantics of programming languages. He is the author of over 150 research articles and four books.