Abstract Interpretation of Stateful Networks

TitleAbstract Interpretation of Stateful Networks
Publication TypeConference Paper
Year of Publication2018
AuthorsAlpernas, K., Manevich R., Panda A., Sagiv M., Shenker S. J., Shoham S., & Velner Y.
Published inProceedings of SAS 2018
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.

Acknowledgment

We thank our anonymous shepherd, and anonymous referees for insightful comments which improved this paper. We thank LogicBlox for providing us with an academic license for their software, and Todd J. Green and Martin Bravenboer for providing technical support and helping with optimization. This publication is part of projects that have received funding from the European Research Council (ERC) under the European Union’s Seventh Framework Program (FP7/2007–2013)/ERC grant agreement no. [321174-VSSC], and Horizon 2020 research and innovation programme (grant agreement No. [759102-SVIS]). The research was supported in part by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, and the Pazy Foundation. This material is based upon work supported by the United States-Israel Binational Science Foundation (BSF) grants No. 2016260 and 2012259. This research was also supported in part by NSF grants 1704941 and 1420064, and funding provided by Intel Corporation.

URLhttps://link.springer.com/chapter/10.1007/978-3-319-99725-4_8
ICSI Research Group

Networking and Security