NetVerifier: Scalable Verification for Programmable Networks

In the process of programmable networks simplifying network management and increasing network flexibility through custom packet behavior, security incidents caused by human logic errors are seriously threatening their safe operation, robust verification methods are required to ensure their correctness. As one of the formal methods, symbolic execution offers a viable approach for verifying programmable networks by systematically exploring all possible paths within a program. However, its application in this field encounters scalability issues due to path explosion and complex constraint-solving. Therefore, in this paper, we propose NetVerifier, a scalable verification system for programmable networks. To mitigate the path explosion issue, we develop multiple pruning strategies that strategically eliminate irrelevant execution paths while preserving verification integrity by precisely identifying the execution paths related to the verification purpose. To address the complex constraint-solving problem, we introduce an execution results reuse solution to avoid redundant computation of the same constraints. To apply these solutions intelligently, a matching algorithm is implemented to automatically select appropriate solutions based on the characteristics of the verification requirement. Moreover, Language Aided Verification (LAV), an assertion language, is designed to express verification intentions in a concise form. Experimental results on diverse open-source programs of varying scales demonstrate NetVerifier’s improvement in scalability and effectiveness in identifying potential network errors. In the best scenario, compared with ASSERT-P4, NetVerifier reduced the execution path, verification time, and memory occupation of the verification process by 99.92%, 94.76%, and 65.19%, respectively.