Veranstalter: SFB MAKI
Referent: Nate Foster, Cornell University, USA
Formal specification and verification of computer networks has become a reality in recent years, with the rise of software-defined networking (SDN) and domain-specific languages and tools. But despite many notable advances, current systems have a key limitation: they model networks as deterministic packet-processing functions.
This works well in simple settings where the network implements point-to- point forwarding and the properties of interest only concern the paths used to carry traffic, but it does not give a satisfactory account of more complicated phenomena such as fault-tolerance, congestion, and utilization.
There is a fundamental mismatch between the realities of modern networks and the capabilities of existing tools—e.g., equal-cost multi-path routing (ECMP) and fast-failover schemes are widely deployed, but current tools cannot handle properties that are quantitative or probabilistic in nature.
This talk will present a new language for network programming based on a probabilistic semantics. I will show how to extend the NetKAT language with new primitives for expressing probabilistic behaviors, and enrich the semantics from one based on deterministic functions to one based on measurable functions on sets of packet histories.
I will discuss a number of properties of the semantics including suitable notions of continuity and approximation as well as a decision procedure. I will also describe an implementation and present case studies showing how the language can be used to model a diverse collection of scenarios drawn from real-world networks.
Probabilistic NetKAT is joint work with colleagues from Cornell, UPenn, and UCL.
Nate Foster is an Associate Professor of Computer Science at Cornell University and a Principal Research Engineer at Barefoot Networks. He also serves as Steering Committee Chair for the P4 Language Consortium. The goal of his research is to develop languages and tools that make it easy for programmers to build secure and reliable systems. He is the recipient of an NSF CAREER award, a Sloan Research fellowship, and several best paper and teaching prizes. He enjoys spending free time with his family and his bikes.