Lecture preparation

Assignment

Why are we reading this paper?

• Networks can have a concise specification amenable to formal verification
• SDN-based networks have significant complexity below the network specification

What to learn from this paper?

• Modeling the system using a language-based approach, as opposed to a state-machine view
• How an SDN-based network operates

Answer this question

Suppose you are building a network using NetCore, with several servers dedicated to monitoring traffic (in the same sense as the paper's example of logging HTTP traffic). Different traffic (e.g., based on destination address or destination port) gets logged to different servers. How would you formally prove that, on the real network as implemented by OpenFlow switches, all traffic is getting logged to some server? What theorem statements would you need to state in Coq, and what parts of NetCore's formal framework would help you in your proof?