Reasoning about Software Defined Networks 2013
Thursday 16:00-18:00 TBD
Instructor: Shmuel (Mooly) Sagiv
Advisor: Michael Schapira
Software-defined networking (SDN) is an approach to computer networking which evolved from work done at UC Berkeley and Stanford University around 2005.
SDN allows network administrators to manage network services through abstraction of lower level functionality.
This is done by decoupling the system that makes decisions about where traffic is sent (the control plane) from the underlying systems that forwards traffic to the selected destination (the data plane).
SDNs shift some of the complexity of developing network protocols from hardware to software.
The main idea is that the hardware (switch) implement simple forwarding rules to either drop packets, forward to another switch, or forward to the controller.
The controller is a general program implemented in software which reacts to messages from the switches by changing the forwarding rules.
SDNs achieve scalability by installing enough rules to prevent frequent needs to forward packets to the controller.
This seminar aims to study programming methodologies and tools which ease the task of creating correct and efficient controller code.
This includes compilation techniques, testing and verifying SDN.
The seminar does not assume prior knowledge in SDNs, testing, or verification.
The attendees are advised to learn about SDNs using the following references:
There will be an overview lecture on SDN by Michael Shapira October 24th.
List of Potential Papers
Interesting Links to explore
- October 17, Short Meeting due to DISC 2013 Conference in Jerusalem
- October 24, Michael Shapira: Introduction to Software Defined Networks
- October 31, Mooly Sagiv: Reasoning about SDN
- November 7, Mooly Sagiv: Productivity Tools for Software Defined Networks
- November 14, Hila Peleg: Languages for Software Defined Networks
- November 21, Eldad Rubinstein:Maple: Simplifying SDN Programming Using Algorithmic Policies
- November 28, Ofri Ziv: VeriFlow: Verifying Network-Wide Invariants in Real Time
- December 5, Guest Lecture: Professor Orna Grumberg, Technion: Using model checking to find security vulnerabilities
- December 12, Guest Lecture: Yotam Harchol Hebrew University: SDN Controller Building and Programming
- December 19, Eviatar Khen: Header Space Analysis: Static Checking For Networks
- December 26, Ronen Jacobi: Toward Synthesis of Network Updates
- January 2, Itzik Malkiel: Practical Experience in Designing an OpenFlow Controller
- January 9, Shay Gozansky: Automatic Test Packet Generation
- January 16, Ori Gerstel: "SDN in Service Provider core networks"
List of Papers
All the articles can be located in the internet using a search engine. Please use most updated version. Please also download and play with any other available material.
Please do not use author's slides.
High Level Network Objectives
Consistency Issues in SDNs
- Mark Reitblatt, Nate Foster, Jennifer Rexford, Cole Schlesinger, and David Walker. Abstractions for Network Update.
- Christopher Monsanto, Joshua Reich, Nate Foster, Jennifer Rexford, and David Walker. Composing Software Defined Networks.
- Laurent Vanbever, Joshua Reich, Theophilus Benson, Nate Foster, and Jennifer Rexford. HotSwap: Correct and Efficient Controller Upgrades for Software-Defined Networks.
- Mark Reitblatt, Marco Canini, Arjun Guha, and Nate Foster. FatTire: Declarative Fault Tolerance for Software-Defined Network.
- Andrew Noyes, Todd War, Pavol Cerny', and Nate Foster. Toward Synthesis of Network Updates.
- Naga Praveen Katta, Jennifer Rexford, and David Walker, Incremental consistent updates.
- Brandon Heller, Colin Scott, Nick McKeown, and Scott Shenker:
Leveraging SDN Layering to Systematically Troubleshoot Networks.
- Nate Foster, Arjun Guha, Mark Reitblatt, Alec Story, Michael J. Freedman, Naga Praveen Katta, Christopher Monsanto, Joshua Reich, Jennifer Rexford, Cole Schlesinger,
David Walker, and Rob Harrison:
Languages for software-defined networks.
- Arjun Guha, Mark Reitblatt, and Nate Foster. Machine-Verified Network Controllers.
Andreas Voellmy, Junchang Wang, Richard Yang, Bryan Ford, Paul Hudak
Maple: Simplifying SDN Programming Using Algorithmic Policies.
- Nanxi Kang, Zhenming Liu, Jennifer Rexford, and David Walker:
Optimizing the “One Big Switch” Abstraction
in Software-Defined Networks
- Andreas Voellmy, Junchang Wang, Y. Richard Yang, Bryan Ford, Paul Hudak: Maple: simplifying SDN programming using algorithmic policies. SIGCOMM 2013: 87-98
- David Erickson: The Beacon OpenFlow Controller
- Tim Nelson, Arjun Guha, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi:
A Balance of Power: Expressive, Analyzable Controller Programming
- Andrew D. Ferguson, Arjun Guha, Chen Liang, Rodrigo Fonseca, Shriram Krishnamurthi:
An API for Application Control of SDNs
- NetKAT: Semantic Foundations for Networks accepted to POPL '14
Testing and Model Checking
- Marco Canini, Daniele Venzano, Peter Pere, Dejan Kostic, and Jennifer Rexford:
A NICE Way to Test OpenFlow Applications
Maciej Kuzniar, Peter Peresini, Marco Canini, Daniele Venzano, Dejan Kostic:
A SOFT Way for OpenFlow Switch Interoperability Testing
- Divjyot Sethi, Srinivas Narayana, Sharad Malik:
Abstractions for Model Checking SDN Controllers, FMCAD 2013
Colin Scott, Andreas Wundsam, Sam Whitlock, Andrew Or, Eugene Huang, Kyriakos Zarifis, Scott Shenker:
How Did We Get Into This Mess?
Isolating Fault-Inducing Inputs to SDN Control Software
- Peyman Kazemian, Stanford University; George Varghese, Nick McKeown:
Header Space Analysis: Static Checking for Networks.
- Ahmed Khurshid, Xuan Zou, Wenxuan Zhou, Matthew Caesar, and P. Brighten Godfrey: VeriFlow: Verifying Network-Wide Invariants in Real Time
- H. Zeng, P. Kazemian, G. Varghese, N. McKeown:
Automatic Test Packet Generation
- Real Time Network Policy Checking using Header Space Analysis”,
P. Kazemian, M. Chang, H. Zeng, G. Varghese, N. McKeown, S. Whyte
Kyriakos Zarifis, and
Leveraging SDN Layering to Systematically Troubleshoot
- Haohui Mai Ahmed Khurshid Rachit Agarwal
Matthew Caesar P. Brighten Godfrey Samuel T. King:
Debugging the Data Plane with Anteater
- A Practical Experience in Designing an OpenFlow Controller
- Stefan Schmid and Jukka SuomelaExploiting: Locality in Distributed SDN Control
For further information Email:firstname.lastname@example.org