Kinetic: verifiable dynamic network control

TLDR

Network conditions are dynamic, yet operators still rely on manual intervention and ad hoc scripts to update configurations, highlighting a need for tools that express data‑plane behavior in response to events. We present Kinetic, a domain‑specific language and network control system that lets operators control networks dynamically in a concise, intuitive way. Kinetic automatically verifies the correctness of control programs against user‑specified temporal properties. A user study with several hundred operators shows Kinetic is intuitive and usable, and performance evaluation demonstrates that realistic programs scale with policy count and network size.

Abstract

Network conditions are dynamic; unfortunately, current approaches to configuring networks. Network operators need tools to express how a network's data-plane behavior should respond to a wide range of events and changing conditions, ranging from unexpected failures to shifting traffic patterns to planned maintenance. Yet, to update the network configuration today, operators typically rely on a combination of manual intervention and ad hoc scripts. In this paper, we present Kinetic, a domain specific language and network control system that enables operators to control their networks dynamically in a concise, intuitive way. Kinetic also automatically verifies the correctness of these control programs with respect to user-specified temporal properties. Our user study of Kinetic with several hundred network operators demonstrates that Kinetic is intuitive and usable, and our performance evaluation shows that realistic Kinetic programs scale well with the number of policies and the size of the network.