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:

• Is a network resilient up to k-link failure?
• Can we quantify the degree of resilience versus the increase in latency?

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:

• devise syntax and semantics to extend NetKAT proper, and
• show that we can still express useful properties such as reachability and waypointing.

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:

• Is the compiler introducing the bug? Is the semantics unsound?
• Is the hardware faulty? Is the bug introduced due to concurrent behaviour?

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.