Verifying Isolation Properties in the Presence of Middleboxes

TL;DR

This paper presents a scalable model checking approach to verify isolation properties in networks with middleboxes like caches and firewalls, overcoming previous limitations in handling large, complex networks.

Contribution

It introduces a novel method leveraging SMT solvers to verify invariants in large networks with dynamic datapath elements, significantly improving scalability.

Findings

Can verify invariants in networks with 30,000 middleboxes within minutes

Outperforms traditional model checking in handling large, complex networks

Enables practical verification of network isolation properties with middleboxes

Abstract

Great progress has been made recently in verifying the correctness of router forwarding tables. However, these approaches do not work for networks containing middleboxes such as caches and firewalls whose forwarding behavior depends on previously observed traffic. We explore how to verify isolation properties in networks that include such "dynamic datapath" elements using model checking. Our work leverages recent advances in SMT solvers, and the main challenge lies in scaling the approach to handle large and complicated networks. While the straightforward application of model checking to this problem can only handle very small networks (if at all), our approach can verify simple realistic invariants on networks containing 30,000 middleboxes in a few minutes.