Abstract Interpretation of Stateful Networks

Kalev Alpernas, Roman Manevich, Aurojit Panda, Mooly Sagiv, Scott Shenker, Sharon Shoham, Yaron Velner

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

Abstract

Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

Original languageEnglish (US)
Title of host publicationStatic Analysis - 25th International Symposium, SAS 2018, Proceedings
EditorsAndreas Podelski
PublisherSpringer-Verlag
Pages86-106
Number of pages21
ISBN (Print)9783319997247
DOIs
StatePublished - Jan 1 2018
Event25th International Static Analysis Symposium, SAS 2018 - Freiburg, Germany
Duration: Aug 29 2018Aug 31 2018

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume11002 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other25th International Static Analysis Symposium, SAS 2018
CountryGermany
CityFreiburg
Period8/29/188/31/18

Fingerprint

Abstract Interpretation
Scalability
Vertex of a graph
Isolation
Polynomials
Acoustic waves
Hardware
State Space
Safety
Entire
Query
Verify
Robustness
Processing
Polynomial

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Alpernas, K., Manevich, R., Panda, A., Sagiv, M., Shenker, S., Shoham, S., & Velner, Y. (2018). Abstract Interpretation of Stateful Networks. In A. Podelski (Ed.), Static Analysis - 25th International Symposium, SAS 2018, Proceedings (pp. 86-106). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11002 LNCS). Springer-Verlag. https://doi.org/10.1007/978-3-319-99725-4_8

Abstract Interpretation of Stateful Networks. / Alpernas, Kalev; Manevich, Roman; Panda, Aurojit; Sagiv, Mooly; Shenker, Scott; Shoham, Sharon; Velner, Yaron.

Static Analysis - 25th International Symposium, SAS 2018, Proceedings. ed. / Andreas Podelski. Springer-Verlag, 2018. p. 86-106 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11002 LNCS).

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

Alpernas, K, Manevich, R, Panda, A, Sagiv, M, Shenker, S, Shoham, S & Velner, Y 2018, Abstract Interpretation of Stateful Networks. in A Podelski (ed.), Static Analysis - 25th International Symposium, SAS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11002 LNCS, Springer-Verlag, pp. 86-106, 25th International Static Analysis Symposium, SAS 2018, Freiburg, Germany, 8/29/18. https://doi.org/10.1007/978-3-319-99725-4_8
Alpernas K, Manevich R, Panda A, Sagiv M, Shenker S, Shoham S et al. Abstract Interpretation of Stateful Networks. In Podelski A, editor, Static Analysis - 25th International Symposium, SAS 2018, Proceedings. Springer-Verlag. 2018. p. 86-106. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-319-99725-4_8
Alpernas, Kalev ; Manevich, Roman ; Panda, Aurojit ; Sagiv, Mooly ; Shenker, Scott ; Shoham, Sharon ; Velner, Yaron. / Abstract Interpretation of Stateful Networks. Static Analysis - 25th International Symposium, SAS 2018, Proceedings. editor / Andreas Podelski. Springer-Verlag, 2018. pp. 86-106 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{6407b31b9ebe4847af11cd5f900af8be,
title = "Abstract Interpretation of Stateful Networks",
abstract = "Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.",
author = "Kalev Alpernas and Roman Manevich and Aurojit Panda and Mooly Sagiv and Scott Shenker and Sharon Shoham and Yaron Velner",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-319-99725-4_8",
language = "English (US)",
isbn = "9783319997247",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer-Verlag",
pages = "86--106",
editor = "Andreas Podelski",
booktitle = "Static Analysis - 25th International Symposium, SAS 2018, Proceedings",

}

TY - GEN

T1 - Abstract Interpretation of Stateful Networks

AU - Alpernas, Kalev

AU - Manevich, Roman

AU - Panda, Aurojit

AU - Sagiv, Mooly

AU - Shenker, Scott

AU - Shoham, Sharon

AU - Velner, Yaron

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

AB - Modern networks achieve robustness and scalability by maintaining states on their nodes. These nodes are referred to as middleboxes and are essential for network functionality. However, the presence of middleboxes drastically complicates the task of network verification. Previous work showed that the problem is undecidable in general and EXPSPACE-complete when abstracting away the order of packet arrival. We describe a new algorithm for conservatively checking isolation properties of stateful networks. The asymptotic complexity of the algorithm is polynomial in the size of the network, albeit being exponential in the maximal number of queries of the local state that a middlebox can do, which is often small. Our algorithm is sound, i.e., it can never miss a violation of safety but may fail to verify some properties. The algorithm performs on-the fly abstract interpretation by (1) abstracting away the order of packet processing and the number of times each packet arrives, (2) abstracting away correlations between states of different middleboxes and channel contents, and (3) representing middlebox states by their effect on each packet separately, rather than taking into account the entire state space. We show that the abstractions do not lose precision when middleboxes may reset in any state. This is encouraging since many real middleboxes reset, e.g., after some session timeout is reached or due to hardware failure.

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

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

U2 - 10.1007/978-3-319-99725-4_8

DO - 10.1007/978-3-319-99725-4_8

M3 - Conference contribution

SN - 9783319997247

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 86

EP - 106

BT - Static Analysis - 25th International Symposium, SAS 2018, Proceedings

A2 - Podelski, Andreas

PB - Springer-Verlag

ER -