NetKat: A Formal System for the Verification of Networks
COPLAS/DIKU Talk by Dexter Kozen, Cornell University
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.