Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.
Submit two items to the submission website (see link in the navigation bar at the top of the page):
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?
Questions or comments regarding 6.826? Contact us on Piazza or send e-mail to the 6.826 staff at 6826-staff@lists.csail.mit.edu.