Dexter Kozen presents the newest research on NetKat
On March 13th Guest Professor at DIKU Dexter Kozen visiting from Cornell University held a lecture on the newest breakthroughs in the development of NetKat, a high-level language for programming networks. Here you can watch a video of the whole lecture.
Dexter Kozen is visiting DIKU for a period of half a year to perform research within the logic of programming languages and collaborate with Professor Fritz Henglein.
At a recent DIKU Talk Dexter held a lecture on NetKat.
See the presentation here
Pictures from the lecture
Læs abstract fra talken
NetKat: A Formal System for the Verification of Network
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.