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 reasoningNetKAT 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?
ConcurrencyNetworks 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.
Verification via model learningWe 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?