A Two-Fold Traffic Flow Model for Network Security Management

Introducing formal methods in the automatic resolution of network security management problems can guarantee solution correctness, so also boosting human confidence in using automatic techniques. A necessary step to achieve this feature is the definition of formal network models, representing network topology, traffic flows, etc. Each state-of-the-art formal network modeling approach has been proposed and validated only for a specific management problem (e.g., verification of configurations or refinement of policies into configurations). This paper analyzes a possible combination of the most promising state-of-the-art modeling approaches into a unified formal model that can be used by existing automatic resolution algorithms to solve both the verification and the refinement problems, without the need of major changes. The model is flexible enough to allow different aggregation levels of traffic into flows. The paper analyzes two opposite flow aggregation strategies, named Atomic Flows and Maximal Flows, and compares their performance when applied to the two identified security problems.