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.


  • Prerequisites
  • Requirements
  • Schedule
  • List of Potential Papers
  • Interesting Links to explore 
  • Prerequisites


    Seminar Requirements


    1. October 17, Short Meeting due to DISC 2013 Conference in Jerusalem
    2. October 24, Michael Shapira: Introduction to Software Defined Networks
    3. October 31, Mooly Sagiv: Reasoning about SDN
    4. November 7, Mooly Sagiv: Productivity Tools for Software Defined Networks
    5. November 14, Hila Peleg: Languages for Software Defined Networks
    6. November 21, Eldad Rubinstein:Maple: Simplifying SDN Programming Using Algorithmic Policies
    7. November 28, Ofri Ziv: VeriFlow: Verifying Network-Wide Invariants in Real Time
    8. December 5, Guest Lecture: Professor Orna Grumberg, Technion: Using model checking to find security vulnerabilities
    9. December 12, Guest Lecture: Yotam Harchol Hebrew University: SDN Controller Building and Programming
    10. December 19, Eviatar Khen: Header Space Analysis: Static Checking For Networks
    11. December 26, Ronen Jacobi: Toward Synthesis of Network Updates
    12. January 2, Itzik Malkiel: Practical Experience in Designing an OpenFlow Controller
    13. January 9, Shay Gozansky: Automatic Test Packet Generation
    14. 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

    Language Abstractions

    Testing and Model Checking


    Interesting Links

    For further information