Help Privacy Policy Disclaimer
  Advanced SearchBrowse





Towards Runtime Verification of Programmable Switches


Feldmann,  Anja       
Internet Architecture, MPI for Informatics, Max Planck Society;

External Resource
No external resources are shared
Fulltext (restricted access)
There are currently no full texts shared for your IP range.
Fulltext (public)

(Preprint), 2MB

Supplementary Material (public)
There is no public supplementary material available

Shukla, A., Hudemann, K., Vági, Z., Hügerich, L., Smaragdakis, G., Schmid, S., et al. (2020). Towards Runtime Verification of Programmable Switches. Retrieved from http://arxiv.org/abs/2004.10887.

Cite as: https://hdl.handle.net/21.11116/0000-0007-0AAD-C
Is it possible to patch software bugs in P4 programs without human
involvement? We show that this is partially possible in many cases due to
advances in software testing and the structure of P4 programs. Our insight is
that runtime verification can detect bugs, even those that are not detected at
compile-time, with machine learning-guided fuzzing. This enables a more
automated and real-time localization of bugs in P4 programs using software
testing techniques like Tarantula. Once the bug in a P4 program is localized,
the faulty code can be patched due to the programmable nature of P4. In
addition, platform-dependent bugs can be detected. From P4_14 to P4_16 (latest
version), our observation is that as the programmable blocks increase, the
patchability of P4 programs increases accordingly. To this end, we design,
develop, and evaluate P6 that (a) detects, (b) localizes, and (c) patches bugs
in P4 programs with minimal human interaction. P6 tests P4 switch
non-intrusively, i.e., requires no modification to the P4 program for detecting
and localizing bugs. We used a P6 prototype to detect and patch seven existing
bugs in eight publicly available P4 application programs deployed on two
different switch platforms: behavioral model (bmv2) and Tofino. Our evaluation
shows that P6 significantly outperforms bug detection baselines while
generating fewer packets and patches bugs in P4 programs such as switch.p4
without triggering any regressions.