Fast Inverse Model Transformation: Algebraic Framework for Fast Data Plane Verification

作     者：Chen, Shenshen Luo, Jian Guo, Dong Gao, Kai Yang, Yang Richard 

作者机构：Tongji University School of Computer Science and Technology Shanghai201804 China Sichuan University Chengdu School of Cyber Science and Engineering Sichuan610065 China Yale University Department of Computer Science New HavenCT06511 United States Fudan University School of Computer Science Shanghai200433 China 

出 版 物：《IEEE Transactions on Dependable and Secure Computing》 (IEEE Trans. Dependable Secure Comput.)

年 卷 期：2025年

核心收录：

学科分类：0808[工学-电气工程] 08[工学] 0701[理学-数学] 

主　　题：Algebra 

摘      要：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-µs 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 and optimization techniques, using algebraic properties. The theory also guides the design and implementation of Uimt, a generic DPV framework with provable optimization techniques. Using Uimt, we create two variants of existing DPV systems, NeoFlash and NeoDeltaNet. 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. © 2004-2012 IEEE All rights reserved.