Submit

Login Login

Register Register

Home / Journals / CMC / Online First / doi:10.32604/cmc.2026.075747
Journal Menu
Special Issues
Table of Content

All issues

Online First

2026

2025

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

Open Access

ARTICLE

NetVerifier: Scalable Verification for Programmable Networks

Ying Yao1, Le Tian1,2,3, Yuxiang Hu1,2,3,*, Pengshuai Cui1,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: email

Computers, Materials & Continua https://doi.org/10.32604/cmc.2026.075747

Received 07 November 2025; Accepted 15 January 2026; Published online 06 February 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

Programmable network; network verification; symbolic execution; scalability

  • 32

    View

  • 7

    Download

  • 1

    Like

Related articles
Copyright© 2026 Tech Science Press
© 1997-2026 TSP (Henderson, USA) unless otherwise stated

Share Link