Open Access

ARTICLE

NetVerifier: Scalable Verification for Programmable Networks

Ying Yao¹, Le Tian^1,2,3, Yuxiang Hu^1,2,3,*, Pengshuai Cui^1,2,3

1 Information Engineering University, Zhengzhou, China
2 National Key Laboratory of Advanced Communication Networks, Zhengzhou, China
3 Key Laboratory of Cyberspace Security, Ministry of Education, Zhengzhou, China

* Corresponding Author: Yuxiang Hu. Email:

Computers, Materials & Continua 2026, 87(2), 77 https://doi.org/10.32604/cmc.2026.075747

Received 07 November 2025; Accepted 15 January 2026; Issue published 12 March 2026

Abstract

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.

---

Keywords

---