Concurrency Networks, and Coinduction

Large computer networks typically require detailed configuration, applied at each node individually. This makes it hard to ensure that the total configuration of network nodes amounts to the intended behaviour of the network as a whole. To remedy this, one can separate the configuration of the network from the hardware implementing it. This technique, called Software Defined Networking (SDN) entails that network policy is decided centrally, after which relevant parts of a configuration implementing this policy are distributed among network devices.

As an added benefit of centralising network policy, it becomes possible to treat this policy as a single object, and reason about or even verify its properties. As an example, NetKAT [Anderson et al., 2014] is a framework which allows the user to specify global network policy in a domain-specific language. These expressions can be compiled [Smolka et al., 2015] to OpenFlow instructions and can run on actual hardware. Moreover, NetKAT allows the user to reason about the policy they wrote using straightforward algebraic laws, which accurately (i.e., soundly and completely) describe its semantics; as a matter of fact, this process can be automated [Foster et al., 2015] quite efficiently using coinductive techniques.

One feature missing from NetKAT is the ability to express concurrency, for instance when processing a packet using multiple tables simultaneously, or perhaps even multiple devices, such as a firewall and an intrusion detection system. The CoNeCo project is aimed at adding this functionality to NetKAT. More precisely, we aim to extend the mathematical foundation of NetKAT known as Kleene algebra with primitives for reasoning about concurrency. The plan is to then build on this foundation to find a concurrent version of NetKAT, which enjoys the same benefits as NetKAT proper, including completeness of the algebraic theory, the possibility of running on network hardware and an efficient decision procedure.