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

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