New directions for network verification

Aurojit Panda, Katerina Argyraki, Mooly Sagiv, Michael Schapira, Scott Shenker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Network verification has recently gained popularity in the programming languages and verification community. Much of the recent work in this area has focused on verifying the behavior of simple networks, whose actions are dictated by static, immutable rules configured ahead of time. However, in reality, modern networks contain a variety of middleboxes, whose behavior is affected both by their configuration and by mutable state updated in response to packets received by them. In this position paper we critically review recent progress on network verification, propose some next steps towards a more complete form of network verification, dispel some myths about networks, provide a more formal description of our approach, and end with a discussion of the formal questions posed to this community by the network verification agenda.

Original languageEnglish (US)
Title of host publication1st Summit on Advances in Programming Languages, SNAPL 2015
EditorsThomas Ball, Rastislav Bodik, Benjamin S. Lerner, Greg Morrisett, Shriram Krishnamurthi
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Pages209-220
Number of pages12
ISBN (Electronic)9783939897804
DOIs
StatePublished - May 1 2015
Event1st Summit on Advances in Programming Languages, SNAPL 2015 - Asilomar, United States
Duration: May 3 2015May 6 2015

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume32
ISSN (Print)1868-8969

Other

Other1st Summit on Advances in Programming Languages, SNAPL 2015
CountryUnited States
CityAsilomar
Period5/3/155/6/15

Keywords

  • Middleboxes
  • Mutable dataplane
  • Network verification

ASJC Scopus subject areas

  • Software

Fingerprint Dive into the research topics of 'New directions for network verification'. Together they form a unique fingerprint.

Cite this