Proposal of an Automatic Verification Method for Network Configuration Model by Static Analysis

TL;DR

This work addresses validating network designs before deployment by automatically verifying a UML-based Network Configuration Model with static analysis to detect policy violations and reveal the specific configuration values responsible. It introduces a three-tier verification framework—single-node, multi-node, and protocol-dependent checks—along with a design-information output transformation that renders the model’s state in device-like CLI reports. In a case study on Shinshu University’s large campus network, the method detected policy violations with approximately 88% initial accuracy and, after refinements, achieved full detection and root-cause identification; it also produced design outputs equivalent to real device status aside from startup-order effects. The approach improves design validation by enabling early, explainable feedback and facilitating designer review, with potential extension to other vendors and dynamic verification synergy.

Abstract

In the network design phase, designers typically assess the validity of the network configuration on paper. However, the interactions between devices based on network protocols can be complex, making this assessment challenging. Meanwhile, testing with actual devices incurs significant costs and effort for procurement and preparation. Traditional methods, however, have limitations in identifying configuration values that cause policy violations and verifying syntactically incomplete device configuration files. In this paper, we propose a method to automatically verify the consistency of a model representing the network configuration (Network Configuration Model) by static analysis. The proposed method performs verification based on the network configuration model to detect policy violations and points out configuration values that cause these violations. Additionally, to facilitate the designers' review of each network device's configuration, the model is converted into a format that mimics the output of actual devices, which designers are likely familiar with. As a case study, we applied the proposed method to the network configuration of Shinshu University, a large-scale campus network, by intentionally introducing configuration errors and applying the method. We further evaluated whether it could output device states equivalent to those of actual devices.

Figures (5)

• Figure 1: Network configuration metamodel
• Figure 2: Network configuration model
• Figure 3: Overview of the proposed method
• Figure 4: Network used for evaluation
• Figure 5: Network configuration model for input (top in Fig.4)