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
Volume32
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

Other

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

Fingerprint

Computer programming languages

Keywords

  • Middleboxes
  • Mutable dataplane
  • Network verification

ASJC Scopus subject areas

  • Software

Cite this

Panda, A., Argyraki, K., Sagiv, M., Schapira, M., & Shenker, S. (2015). New directions for network verification. In T. Ball, R. Bodik, B. S. Lerner, G. Morrisett, & S. Krishnamurthi (Eds.), 1st Summit on Advances in Programming Languages, SNAPL 2015 (Vol. 32, pp. 209-220). Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. https://doi.org/10.4230/LIPIcs.SNAPL.2015.209

New directions for network verification. / Panda, Aurojit; Argyraki, Katerina; Sagiv, Mooly; Schapira, Michael; Shenker, Scott.

1st Summit on Advances in Programming Languages, SNAPL 2015. ed. / Thomas Ball; Rastislav Bodik; Benjamin S. Lerner; Greg Morrisett; Shriram Krishnamurthi. Vol. 32 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. p. 209-220.

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

Panda, A, Argyraki, K, Sagiv, M, Schapira, M & Shenker, S 2015, New directions for network verification. in T Ball, R Bodik, BS Lerner, G Morrisett & S Krishnamurthi (eds), 1st Summit on Advances in Programming Languages, SNAPL 2015. vol. 32, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, pp. 209-220, 1st Summit on Advances in Programming Languages, SNAPL 2015, Asilomar, United States, 5/3/15. https://doi.org/10.4230/LIPIcs.SNAPL.2015.209
Panda A, Argyraki K, Sagiv M, Schapira M, Shenker S. New directions for network verification. In Ball T, Bodik R, Lerner BS, Morrisett G, Krishnamurthi S, editors, 1st Summit on Advances in Programming Languages, SNAPL 2015. Vol. 32. Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing. 2015. p. 209-220 https://doi.org/10.4230/LIPIcs.SNAPL.2015.209
Panda, Aurojit ; Argyraki, Katerina ; Sagiv, Mooly ; Schapira, Michael ; Shenker, Scott. / New directions for network verification. 1st Summit on Advances in Programming Languages, SNAPL 2015. editor / Thomas Ball ; Rastislav Bodik ; Benjamin S. Lerner ; Greg Morrisett ; Shriram Krishnamurthi. Vol. 32 Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing, 2015. pp. 209-220
@inproceedings{8880d0ba6529421e90038f23988a39cd,
title = "New directions for network verification",
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.",
keywords = "Middleboxes, Mutable dataplane, Network verification",
author = "Aurojit Panda and Katerina Argyraki and Mooly Sagiv and Michael Schapira and Scott Shenker",
year = "2015",
month = "5",
day = "1",
doi = "10.4230/LIPIcs.SNAPL.2015.209",
language = "English (US)",
volume = "32",
pages = "209--220",
editor = "Thomas Ball and Rastislav Bodik and Lerner, {Benjamin S.} and Greg Morrisett and Shriram Krishnamurthi",
booktitle = "1st Summit on Advances in Programming Languages, SNAPL 2015",
publisher = "Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing",

}

TY - GEN

T1 - New directions for network verification

AU - Panda, Aurojit

AU - Argyraki, Katerina

AU - Sagiv, Mooly

AU - Schapira, Michael

AU - Shenker, Scott

PY - 2015/5/1

Y1 - 2015/5/1

N2 - 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.

AB - 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.

KW - Middleboxes

KW - Mutable dataplane

KW - Network verification

UR - http://www.scopus.com/inward/record.url?scp=84959046039&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84959046039&partnerID=8YFLogxK

U2 - 10.4230/LIPIcs.SNAPL.2015.209

DO - 10.4230/LIPIcs.SNAPL.2015.209

M3 - Conference contribution

VL - 32

SP - 209

EP - 220

BT - 1st Summit on Advances in Programming Languages, SNAPL 2015

A2 - Ball, Thomas

A2 - Bodik, Rastislav

A2 - Lerner, Benjamin S.

A2 - Morrisett, Greg

A2 - Krishnamurthi, Shriram

PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing

ER -