Data plane verification (DPV) analyzes routing tables and detects routing abnormalities and policy violations during network operation and planning. Thus, it has become an important tool to harden the networking infrastructure and the computing systems building on top. Substantial advancements have been made in the last decade and state-of-the-art DPV systems can achieve sub-us verification for an update of a single forwarding rule. In this paper, we introduce fast inverse model transformation (FIMT), the first theoretical framework to systematically model and analyze centralized DPV systems. FIMT reveals the algebraic structure in the model update process, a key step in fast DPV systems. Thus, it can systematically analyze the correctness of several DPV systems, using algebraic properties. The theory also guides the design and implementation of NeoFlash, a refactored version of Flash with new optimization techniques. Evaluations show that NeoFlash outperforms existing state-of-the-art centralized DPV systems in various datasets and reveal insights to key techniques towards fast DPV.

翻译：数据平面验证（DPV）通过分析路由表，在网络运行与规划过程中检测路由异常及策略违规。因此，它已成为强化网络基础设施及其上层计算系统的重要工具。过去十年间，该领域取得了显著进展，最先进的DPV系统可在亚微秒级别内完成单条转发规则更新的验证。本文提出快速逆模型变换（FIMT）——首个系统建模与分析集中式DPV系统的理论框架。FIMT揭示了模型更新过程中的代数结构（这是高速DPV系统的关键步骤），从而能够利用代数性质系统性地分析多个DPV系统的正确性。该理论还指导了NeoFlash（基于Flash重构并采用新优化技术的版本）的设计与实现。评估表明，NeoFlash在多种数据集上均优于现有最先进的集中式DPV系统，并揭示了实现高速DPV的关键技术洞见。