Neves, M., Huffaker, B., Levchenko, K., & Barcellos, M. (2021). Dynamic property enforcement in programmable data planes. IEEE/ACM Transactions on Networking. https://doi.org/10.1109/TNET.2021.3068339
Abstract
Network programmers can currently deploy an arbitrary set of protocols in forwarding devices through data plane programming languages such as P4. However, as any other type of software, P4 programs are subject to bugs and misconfigurations. Network verification tools have been proposed as a means of ensuring that the network behaves as expected, but these tools frequently face severe scalability issues. In this paper, we argue for a novel approach to this problem. Rather than statically inspecting a network configuration looking for bugs, we propose to enforce networking properties at runtime. To this end, we developed P4box, a system for deploying runtime monitors in programmable data planes. P4box allows programmers to easily express a broad range of properties (both program-specific and network-wide). Moreover, we provide an automated framework based on assertions and symbolic execution for ensuring monitor correctness. Our experiments on a SmartNIC show that P4box monitors represent a small overhead to network devices in terms of latency, throughput and power consumption.
Rights
This is an author’s accepted version of a paper published in the IEEE/ACM Transactions on Networking. © 2021 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE.
