Before lecture, read the paper assigned below, and submit two items
to the submission website
- Submit your own question about the paper (e.g., what you find most
confusing about the paper or the paper's general context/problem), before
lecture (i.e., 1pm). You cannot use the question below. To the extent
possible, during lecture we will try to answer questions submitted
- Submit your answer for the question below, before the beginning of the lecture.
Also keep in mind that you will need to write a
paper summary for your choice of papers
throughout the semester.
Read the paper
Machine-Verified Network Controllers
by Guha et al.
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?