Abstract
Software Defined Networking (SDN) has become a new paradigm in computer networking, introducing a decoupled architecture that separates the network into the data plane and the control plane. The control plane acts as the centralized brain, managing configuration updates and network management
tasks, while the data plane handles traffic based on the configurations provided by the control plane.
Given its asynchronous distributed nature, SDN can experience data races due to message passing between the control and data planes. This paper presents Tracer, a tool designed to automatically detect and explain the occurrence of data races in DyNetKAT SDN models. DyNetKAT is a formal framework for modeling and analyzing SDN behaviors, with robust operational semantics and a complete axiomatization implemented in Maude. Built on NetKAT, a language leveraging Kleene
Algebra with Tests to express data plane forwarding behavior, DyNetKAT extends these capabilities by adding primitives for communication between the control and data planes. Tracer exploits the DyNetKAT axiomatization and enables race detection in SDNs based on Lamport vector clocks. Tracer is a publicly available tool.
tasks, while the data plane handles traffic based on the configurations provided by the control plane.
Given its asynchronous distributed nature, SDN can experience data races due to message passing between the control and data planes. This paper presents Tracer, a tool designed to automatically detect and explain the occurrence of data races in DyNetKAT SDN models. DyNetKAT is a formal framework for modeling and analyzing SDN behaviors, with robust operational semantics and a complete axiomatization implemented in Maude. Built on NetKAT, a language leveraging Kleene
Algebra with Tests to express data plane forwarding behavior, DyNetKAT extends these capabilities by adding primitives for communication between the control and data planes. Tracer exploits the DyNetKAT axiomatization and enables race detection in SDNs based on Lamport vector clocks. Tracer is a publicly available tool.
| Original language | English |
|---|---|
| Publication status | Accepted/In press - 16 Sept 2024 |
| Event | 26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2024 - Universitatea de Vest, Timișoara, Romania Duration: 16 Sept 2024 → 19 Sept 2024 Conference number: 26 https://synasc.ro/2024/ |
Conference
| Conference | 26th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2024 |
|---|---|
| Abbreviated title | SYNASC 2024 |
| Country/Territory | Romania |
| City | Timișoara |
| Period | 16/09/24 → 19/09/24 |
| Internet address |