Packet flow analysis in IP networks via abstract interpretation

TL;DR

This paper introduces an abstract interpretation-based static analysis method for IP networks, enabling flexible and formal verification of packet flows and high-level policy inference beyond previous approaches.

Contribution

It formalizes a new abstract interpretation approach for network analysis, providing correctness guarantees and addressing complex, multi-router policy inference problems.

Findings

Demonstrates the flexibility of the approach for various network analysis tasks

Provides formal correctness guarantees for the analysis method

Successfully applies the method to infer high-level network policies

Abstract

Static analysis (aka offline analysis) of a model of an IP network is useful for understanding, debugging, and verifying packet flow properties of the network. There have been static analysis approaches proposed in the literature for networks based on model checking as well as graph reachability. Abstract interpretation is a method that has typically been applied to static analysis of programs. We propose a new, abstract-interpretation based approach for analysis of networks. We formalize our approach, mention its correctness guarantee, and demonstrate its flexibility in addressing multiple network-analysis problems that have been previously solved via tailor-made approaches. Finally, we investigate an application of our analysis to a novel problem -- inferring a high-level policy for the network -- which has been addressed in the past only in the restricted single-router setting.