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
AN - SCOPUS:84959046039
T3 - Leibniz International Proceedings in Informatics, LIPIcs
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
T2 - 1st Summit on Advances in Programming Languages, SNAPL 2015
Y2 - 3 May 2015 through 6 May 2015
ER -