Skip to main content
USENIX
  • Conferences
  • Students
Sign in
  • Home
  • Attend
    • Registration Information
    • Registration Discounts
    • Students and Grants
    • Venue, Hotel, and Travel
    • Oakland Dining Guide
  • Activities
    • Birds-of-a-Feather Sessions
    • Poster Session
  • Program
    • At a Glance
    • Technical Sessions
  • Participate
    • Call for Papers
    • Call for Posters
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Past Symposia
    • Questions?
    • Help Promote!
  • Home
  • Attend
    • Registration Information
    • Registration Discounts
    • Students and Grants
    • Venue, Hotel, and Travel
    • Oakland Dining Guide
  • Activities
  • Program
    • At a Glance
    • Technical Sessions
  • Participate
    • Call for Papers
    • Call for Posters
    • Instructions for Participants
  • Sponsorship
  • About
    • Symposium Organizers
    • Past Symposia
    • Questions?
    • Help Promote!

sponsors

Gold Sponsor
Silver Sponsor
Silver Sponsor
Silver Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
Bronze Sponsor
General Sponsor
General Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Media Sponsor
Industry Partner

help promote

NSDI '15 button

Get more
Help Promote graphics!

connect with us


  •  Twitter
  •  Facebook
  •  LinkedIn
  •  Google+
  •  YouTube

twitter

Tweets by @usenix

usenix conference policies

  • Event Code of Conduct
  • Conference Network Policy
  • Statement on Environmental Responsibility Policy

You are here

Home » Checking Beliefs in Dynamic Networks
Tweet

connect with us

https://twitter.com/usenix
https://www.facebook.com/usenixassociation
https://plus.google.com/108588319090208187909/posts
http://www.linkedin.com/groups/USENIX-Association-49559/about
http://www.youtube.com/user/USENIXAssociation

Checking Beliefs in Dynamic Networks

Authors: 

Nuno P. Lopes, Nikolaj Bjørner, and Patrice Godefroid, Microsoft Research; Karthick Jayaraman, Microsoft Azure; George Varghese, Microsoft Research

Abstract: 

Network Verification is a form of model checking in which a model of the network is checked for properties stated using a specification language. Existing network verification tools lack a general specification language and hardcode the network model. Hence they cannot, for example, model policies at a high level of abstraction. Neither can they model dynamic networks; even a simple packet format change requires changes to internals. Standard verification tools (e.g., model checkers) have expressive specification and modeling languages but do not scale to large header spaces. We introduce Network Optimized Datalog (NoD) as a tool for network verification in which both the specification language and modeling languages are Datalog. NoD can also scale to large to large header spaces because of a new filter-project operator and a symbolic header representation.

As a consequence, NoD allows checking for beliefs about network reachability policies in dynamic networks. A belief is a high-level invariant (e.g., “Internal controllers cannot be accessed from the Internet”) that a network operator thinks is true. Beliefs may not hold, but checking them can uncover bugs or policy exceptions with little manual effort. Refuted beliefs can be used as a basis for revised beliefs. Further, in real networks, machines are added and links fail; on a longer term, packet formats and even forwarding behaviors can change, enabled by OpenFlow and P4. NoD allows the analyst to model such dynamic networks by adding new Datalog rules.

For a large Singapore data center with 820K rules, NoD checks if any guest VM can access any controller (the equivalent of 5K specific reachability invariants) in 12 minutes. NoD checks for loops in an experimental SWAN backbone network with new headers in a fraction of a second. NoD generalizes a specialized system, SecGuru, we currently use in production to catch hundreds of configuration bugs a year. NoD has been released as part of the publicly available Z3 SMT solver.

Nuno P. Lopes, Microsoft Research

Nikolaj Bjørner, Microsoft Research

Patrice Godefroid, Microsoft Research

Karthick Jayaraman, Microsoft Azure

George Varghese, Microsoft Research

Open Access Media

USENIX is committed to Open Access to the research presented at our events. Papers and proceedings are freely available to everyone once the event begins. Any video, audio, and/or slides that are posted after the event are also free and open to everyone. Support USENIX and our commitment to Open Access.

BibTeX
@inproceedings {189018,
author = {Nuno P. Lopes and Nikolaj Bj{\o}rner and Patrice Godefroid and Karthick Jayaraman and George Varghese},
title = {Checking Beliefs in Dynamic Networks},
booktitle = {12th USENIX Symposium on Networked Systems Design and Implementation (NSDI 15)},
year = {2015},
isbn = {978-1-931971-218},
address = {Oakland, CA},
pages = {499--512},
url = {https://www.usenix.org/conference/nsdi15/technical-sessions/presentation/lopes},
publisher = {USENIX Association},
month = may,
}
Download
Lopes PDF
View the slides

Presentation Video 

Presentation Audio

MP3 Download

Download Audio

  • Log in or    Register to post comments

Gold Sponsors

Silver Sponsors

Bronze Sponsors

General Sponsors

Media Sponsors & Industry Partners

© USENIX

  • Privacy Policy
  • Contact Us