Expressing dynamic network policies in a concise and intuitive way, with verifiability!
View on Github » (branch 'kinetic')
Kinetic is a domain specific language (DSL) and an SDN network control system that allows operators to express dynamic network policies in a concise, intuitive way. Using Kinetic, programmers can implement a network-wide control program that can dynamically change network behavior based on various types of network events.
In Kinetic, you use a finite state machine (FSM) abstraction to express network policies that change network behavior (e.g., forwarding) based on arbitrary network events (e.g., intrusion). FSMs (1) intuitively and concisely capture control dynamics in response to network events; and (2) their structure makes them amenable to verification.
Using Pyretic's composition operators, it is possible to compose multiple finite state machine (FSM)-based network policies together.
Kinetic supports verification of network policies using the NuSMV symbolic model checker. Kinetic automatically generates a NuSMV input from the program written by the programmer/operator, and verifies logic statements written in CTL (Computation Tree Logic).
Kinetic helps operators verify control logic. This capability helps operators both reason about future data-plane states that a control program could install and troubleshoot incorrect behavior when it does arise.
Most recommended way to get hands-on with Kinetic is through our pre-built VirtualBox VMs. Click below to download our VMs. (Username/password in VM: mininet/mininet)
For more documentation and tutorial on how to build and run Kinetic programs, click below: