Runtime Verification for Programmable Switches

Journal Article (2023)
Author(s)

Apoorv Shukla (Huawei Technologies Deutschland GmbH)

Kevin Hudemann (SAP AG)

Zsolt Vagi (Swisscom AG)

Lily Hügerich (Technical University of Berlin)

Georgios Smaragdakis (TU Delft - Cyber Security)

Artur Hecker (Huawei Technologies Deutschland GmbH)

Stefan Schmid (Technical University of Berlin)

Anja Feldmann (Max Planck Institut für Informatik)

Research Group
Cyber Security
Copyright
© 2023 Apoorv Shukla, Kevin Hudemann, Zsolt Vagi, Lily Hugerich, G. Smaragdakis, Artur Hecker, Stefan Schmid, Anja Feldmann
DOI related publication
https://doi.org/10.1109/TNET.2023.3234931
More Info
expand_more
Publication Year
2023
Language
English
Copyright
© 2023 Apoorv Shukla, Kevin Hudemann, Zsolt Vagi, Lily Hugerich, G. Smaragdakis, Artur Hecker, Stefan Schmid, Anja Feldmann
Research Group
Cyber Security
Issue number
4
Volume number
31
Pages (from-to)
1822-1837
Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Abstract

We introduce a runtime verification framework for programmable switches that complements static analysis. To evaluate our approach, we design and develop P6, 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 by P6. P6 is 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 a P6 prototype 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 that P6 significantly outperforms bug detection baselines while generating fewer packets and patches bugs in large P4 programs, e.g., switch.p4 without triggering any regressions.

Files

Runtime_Verification_for_Progr... (pdf)
(pdf | 3.03 Mb)
- Embargo expired in 11-09-2023
License info not available