Applications of Automata and Concurrency Theory in Networks (Invited Paper)

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 seeking to provide high-level abstractions to simplify the task of specifying the packet-processing behavior of a network.

Previous work by Anderson et al. [Anderson et al.,POPL'14,2014] introduced NetKAT, a language and logic for specifying and verifying the packet-processing behavior of 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 a PSPACE 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 [Kozen,ACM Trans. Program. Lang. Syst.,1997]. Several practical applications of NetKAT have been developed, including algorithms for testing reachability and non-interference and a syntactic correctness proof for a compiler that translates programs to hardware instructions for SDN switches.

In a follow-up paper [Foster et al.,POPL'15,2015], the coalgebraic theory of NetKAT was developed and a bisimulation-based algorithm for deciding equivalence was devised. The new algorithm was shown to be significantly more efficient than the previous naive algorithm [Anderson et al.,POPL'14,2014], which was PSPACE in the best case and the worst case, as it was based on the determinization of a nondeterministic algorithm. Along with the coalgebraic model of NetKAT, the authors presented a specialized version of the Brzozowski derivative in both semantic and syntactic forms. They also also proved a version of Kleene's theorem for NetKAT that shows that the coalgebraic model is equivalent to the standard packet-processing and language models introduced previously [Anderson et al.,POPL'14,2014]. They demonstrated the real-world applicability of the tool by using it to decide common network verification questions such as all-pairs connectivity, loop-freedom, and translation validation - all pressing questions in modern networks.

This talk will survey applications of automata theory, concurrency theory and coalgebra to problems in networking. We will suggest directions for exploring the bridge between the two communities and ways to deliver new synergies. On the one hand, this will lead to new insights and techniques that will enable the development of rigorous semantic foundations for networks. On the other hand, the idysiocransies of networks will provide new challenges for the automata and concurrency community.