NetChecker: enabling real-time and error-locatable runtime verification for programmable networks
Abstract Runtime errors may occur in programmable networks due to incorrect table hits, erroneous rule matches, and mistakes in the P4 pipeline, which cannot be debugged and repaired before program deployment. In this paper, we present the design and implementation of NetChecker, a real-time and err...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Springer
2025-06-01
|
| Series: | Journal of King Saud University: Computer and Information Sciences |
| Subjects: | |
| Online Access: | https://doi.org/10.1007/s44443-025-00083-6 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1849331613313269760 |
|---|---|
| author | Ying Yao Le Tian Yuxiang Hu |
| author_facet | Ying Yao Le Tian Yuxiang Hu |
| author_sort | Ying Yao |
| collection | DOAJ |
| description | Abstract Runtime errors may occur in programmable networks due to incorrect table hits, erroneous rule matches, and mistakes in the P4 pipeline, which cannot be debugged and repaired before program deployment. In this paper, we present the design and implementation of NetChecker, a real-time and error-locatable runtime verification system for programmable networks. NetChecker enables the developer to freely express their verification and error localization requirements for any data plane programs using a high-level specification language named Language Aided Verification (LAV), referred to as the LAV program. Furthermore, NetChecker employs a set of translators to convert the aforementioned LAV program into a snippet of the target data plane program, enabling concurrent verification and error localization with the target data plane program execution. Experimental results in diverse network scenarios and open-source programs demonstrate that NetChecker is capable of detecting potential errors in real time and locating them without introducing significant overhead in programmable networks. |
| format | Article |
| id | doaj-art-be3d6b4f135840daa6f7033fa7766b21 |
| institution | Kabale University |
| issn | 1319-1578 2213-1248 |
| language | English |
| publishDate | 2025-06-01 |
| publisher | Springer |
| record_format | Article |
| series | Journal of King Saud University: Computer and Information Sciences |
| spelling | doaj-art-be3d6b4f135840daa6f7033fa7766b212025-08-20T03:46:28ZengSpringerJournal of King Saud University: Computer and Information Sciences1319-15782213-12482025-06-0137411710.1007/s44443-025-00083-6NetChecker: enabling real-time and error-locatable runtime verification for programmable networksYing Yao0Le Tian1Yuxiang Hu2Information Engineering UniversityInformation Engineering UniversityInformation Engineering UniversityAbstract Runtime errors may occur in programmable networks due to incorrect table hits, erroneous rule matches, and mistakes in the P4 pipeline, which cannot be debugged and repaired before program deployment. In this paper, we present the design and implementation of NetChecker, a real-time and error-locatable runtime verification system for programmable networks. NetChecker enables the developer to freely express their verification and error localization requirements for any data plane programs using a high-level specification language named Language Aided Verification (LAV), referred to as the LAV program. Furthermore, NetChecker employs a set of translators to convert the aforementioned LAV program into a snippet of the target data plane program, enabling concurrent verification and error localization with the target data plane program execution. Experimental results in diverse network scenarios and open-source programs demonstrate that NetChecker is capable of detecting potential errors in real time and locating them without introducing significant overhead in programmable networks.https://doi.org/10.1007/s44443-025-00083-6Programmable networkRuntime verificationError detectionError localization |
| spellingShingle | Ying Yao Le Tian Yuxiang Hu NetChecker: enabling real-time and error-locatable runtime verification for programmable networks Journal of King Saud University: Computer and Information Sciences Programmable network Runtime verification Error detection Error localization |
| title | NetChecker: enabling real-time and error-locatable runtime verification for programmable networks |
| title_full | NetChecker: enabling real-time and error-locatable runtime verification for programmable networks |
| title_fullStr | NetChecker: enabling real-time and error-locatable runtime verification for programmable networks |
| title_full_unstemmed | NetChecker: enabling real-time and error-locatable runtime verification for programmable networks |
| title_short | NetChecker: enabling real-time and error-locatable runtime verification for programmable networks |
| title_sort | netchecker enabling real time and error locatable runtime verification for programmable networks |
| topic | Programmable network Runtime verification Error detection Error localization |
| url | https://doi.org/10.1007/s44443-025-00083-6 |
| work_keys_str_mv | AT yingyao netcheckerenablingrealtimeanderrorlocatableruntimeverificationforprogrammablenetworks AT letian netcheckerenablingrealtimeanderrorlocatableruntimeverificationforprogrammablenetworks AT yuxianghu netcheckerenablingrealtimeanderrorlocatableruntimeverificationforprogrammablenetworks |