The central objective of this project is to develop new abstractions for programming of networks, with modular constructs. We will provide rigorous semantic probabilistic foundations, enabling quantitative reasoning, and semantic foundations for concurrency. This will serve as a solid platform for program analysis tools where compositional reasoning about complex interactions will be a reality. These are the main strands of the project:

Probabilistic reasoning

NetKAT is a domain-specific language that can be used to compositionally specify and verify deterministic policies of Software Defined Networks (SDNs). We will work on developing a conservative probabilistic extension of the language – ProbNetKAT. This will enable programming and verification of probabilistic features in SDN, such as: We will use the foundational insights gained in devising the semantics of ProbNetKAT to develop a scalable tool for verifying probabilistic network programs.

Concurrency

Networks are inherently concurrent systems, for instance when processing a packet using multiple tables simultaneously, or perhaps even multiple devices, such as a firewall and an intrusion detection system. We will extend NetKAT with constructs to express and verify concurrency in packet processing. We will need to: We will base our explorations on Concurrent Kleene Algebra (CKA), extending results on soundness and completeness, as well as algorithms for (bi)simulation.

Verification via model learning

We will explore formally verifying code compiled from a high-level language into low-level code running on a network. We will explore recent results on categorical automata learning and use NetKAT to learn models of basic networking behaviour, such as packet forwarding and filtering. The challenge will be on finding bugs and their source: The obstacle in this application will be engineering the interface between the information needed for the learning process and what is available from the network program, hardware, or compiler.