Kinetic: Verifiable Dynamic Network Control
http://www.cs.princeton.edu/~mshahbaz/papers/nsdi15-kinetic.pdf http://resonance.noise.gatech.edu/
ranging from unexpected failures to shifting traffic patterns to planned maintenance, operators typically rely on a combination of manual intervention and ad hoc scripts. … realistic Kinetic programs scale well with the number of policies and the size of the network.
[20, 27, 3, 22]
require compelx instrumentation and “wrappers” that dynamically change low-level network configuration. recent survey … 89% of respondents said that they could not be certain that the changes they made to network configuration would not introduce new bugs.
3.3 Composing independent policies
represent the overall network state as a product automaton that can be decomposed in terms of simpler tasks, where each task has simpler (and smaller) FSMs.
4 Language and abstractions
Kinetic extends Pyretic DSL with a subclass of Dynamic-FSMPolicy —
which takes two arguments: an LPEC projection map (L) and an FSM
description (M).
Each LPEC has an FSM, which has a set of states, where each state has a Pyretic policy; and a set of transitions between those states, where transitions occur in response to events … When events arrive, the respective LPEC FSMs may transition between states, ultimately inducing the Pyretic runtime to recompile the policy and push updated rules to the switches.
