Runtime Verification for Programmable Switches
Apoorv Shukla, Kevin Nico Hudemann, Zsolt Vági, Lily Hügerich, Georgios Smaragdakis, Artur Hecker, Stefan Schmid, Anja Feldmann · IEEE/ACM Transactions on Networking · 2023
We introduce a runtime verification framework for programmable switches that complements static analysis. To evaluate our approach, we design and developP6, a runtime verification system that automatically detects, localizes, and patches software bugs in P4 programs. Bugs are reported via a violation of pre-specified expected behavior that is captured byP6.P6is based on machine learning-guided fuzzing that tests P4 switch non-intrusively, i.e., without modifying the P4 program for detecting runtime bugs. This enables an automated and real-time localization and patching of bugs. We used aP6prototype to detect and patch existing bugs in various publicly available P4 application programs deployed on two different switch platforms, namely, behavioral model (bmv2) and Tofino. Our evaluation shows thatP6significantly outperforms bug detection baselines while generating fewer packets and patches bugs in large P4 programs, e.g.,switch.p4without triggering any regressions.