NetChecker: enabling real-time and error-locatable runtime verification for programmable networks - Ying Yao; Le Tian; Yuxiang Hu (Journal of King Saud University: Computer and Information Sciences)
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.