Towards automatic exploitation of programmable networks
Mihai-Valentin Dumitru, Dragoș Dumitrescu, Costin Raiciu · 2024
P4 verification works have found numerous bugs in programs of various sizes. While existing tools are efficient in finding bugs such as invalid header accesses, little effort has been put in understanding the potential impact of these bugs against the network. In this paper, we investigate whether these bugs can expose security vulnerabilities similar to those studied extensively for commodity CPUs. This work presents the design and implementation of HackP4 – a tool which makes use of static and dynamic analysis techniques to assess security properties of P4 dataplanes. HackP4 discovers vulnerabilities in P4 programs and automatically generates security exploits if they exist; otherwise, it provides guarantees of their absence. We present the results of running HackP4 against several P4 programs and show the kind of vulnerabilities it is able to capture. Finally, we discuss best practices for mitigating bugs and minimizing the impact of vulnerabilities.