Abstract Interpretation of Stateful Networks

TL;DR

This paper introduces a polynomial-time, sound algorithm for verifying isolation properties in stateful networks with middleboxes, using abstract interpretation techniques that simplify state analysis while ensuring safety violations are not missed.

Contribution

The paper presents a novel, efficient algorithm for conservative verification of stateful networks, handling complex middlebox behaviors with abstraction techniques that preserve soundness.

Findings

Algorithm is polynomial in network size but exponential in local query complexity.

It is sound and guarantees no missed safety violations.

Abstractions remain precise even when middleboxes reset.

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.