Perhaps lulled into a sense of complacency because of the Internet’s best-effort delivery model, which makes no explicit promises about network behavior, networking has long relied on ad hoc configuration and a “we’ll fix it when it breaks” operational attitude. However, as networking matures as a field, and institutions increasingly rely on networks to provide isolation and other behavioral guarantees, there is growing interest in developing rigorous verification tools that can ensure the correctness of network configurations. The theme of this project is developing techniques for verifying that the network satisfies certain correctness properties. For example, we are interested in showing isolation between packets sent between two end-hosts. This is the most straightforward network invariant: can two hosts exchange packets? In most cases we want to ensure that two hosts can exchange packets, but there are scenarios where isolation is crucial and here we want to ensure that the hosts cannot exchange packets. A variation of the above invariant, where there is an asymmetry in that, for example, we might want to allow host a to initiate contact with host b, but not allow host b to initiate contact with host a. But once contact is properly initiated, we want two-way reachability.
This project is led by Arjoit Panda under the supervision of Scott Shenker. 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.