Gossip In NetKAT

In this talk we will combine the study of NetKAT with the study of dynamic gossip. The talk is largely based on my master thesis, but as I am currently working on this will also contain some work in progress and loose ends. NetKAT is a sound and complete network programming language based on Kleene algebra with tests, originally used to describe packets traveling through networks. It has a coalgebraic decision procedure deciding NetKAT equivalences. Dynamic gossip is a field in which it is studied how information spreads through a gossip graph, where the links in the gossip graph are changeable (dynamic). So far no sound and complete logic is available that describes dynamic gossip in a satisfactory way. In my thesis I explored the application of NetKAT to dynamic gossip. We will see that a change of perspective on NetKAT in which we keep track of the state of the switches in a network allows us to use NetKAT to model the Learn New Secrets Protocol, which is one of many gossip protocols. The addition to NetKAT to keep track of the state of switches is formalised and shown to remain sound and complete with respect to the packet-processing model. We will see how to formalise various notions from dynamic gossip in NetKAT, strengthening the claim that NetKAT can be used to model gossip. We will end the talk looking at the current state of affairs: can NetKAT be used to tell us anything new about dynamic gossip, could we give alternative proofs for known results of gossip and can we achieve some benchmark results using our own implementation in Haskell combined with the existing NetKAT implementation in OCaml.

hosted by