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的关键技术洞察。