Run-time Performance Monitoring, Verification, and Healing of End-to-End SDN Services

Softwarization enables tremendous flexibility for networks as the use of software-defined networking (SDN) and programmable data planes (e.g. P4) together support dynamic reconfiguration of networks in real-time, in response to network conditions and new service requests. However, as the topologies and characteristics of the dynamically reconfigured networks are not known in advance, it is imperative to ensure that end-to-end network services continue to satisfy their associated service-level agreements (SLAs), including those with performance requirements, despite unanticipated network conditions and failures. It is infeasible to guarantee prior to network deployment that a potentially unknown set of dynamic network configurations satisfies desired performance-based SLAs. Run-time verification based on formal assertions -- in combination with programmable data plane monitoring capabilities such as P4-INT -- can provide a basis for detecting potential performance-based SLA violations of SDN networks, together with identifying and executing appropriate network mitigations that leverage network programmability. In this paper, we propose a textit{verification transverse} based on formal specifications, that spans desired performance SLAs across the distributed SDN control and programmable data planes, and can coordinate with both planes to execute dynamic reconfigurations that mitigate the detected issues. We demonstrate a proof-of-concept implementation based on an adaptation of the Aerial run-time verification tool, together with P4-INT, on a network running a distributed set of ONOS open-source controllers together with a data plane consisting of P4 software switches.