<p>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.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

NetChecker: enabling real-time and error-locatable runtime verification for programmable networks

  • Ying Yao,
  • Le Tian,
  • Yuxiang Hu

摘要

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.