Kinetic:
Verifiable Dynamic Control

Expressing dynamic network policies in a concise and intuitive way, with verifiability!

View on Github » (branch 'kinetic')

What is 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.

Kinetic is build on top of Pyretic, an SDN programming language embedded in Python. It is a member of the Frenetic family of SDN languages.

Kinetic: Control-plane Verification


Highlights

  • Using Finite State Machines

    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.


  • Composing Network Policies

    Using Pyretic's composition operators, it is possible to compose multiple finite state machine (FSM)-based network policies together.


  • Verifying The Control Logic of Network Policies

    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.

  • View example »


    Pre-installed VM

    Most recommended way to get hands-on with Kinetic is through our pre-built VirtualBox VMs. Click below to download our VMs.

    32-bit VM (coming soon) » 64-bit VM »

    Tutorial and Documentation

    For more documentation and tutorial on how to build and run Kinetic programs, click below:

    Kinetic Tutorial »

    Contact

    Project Lead: Hyojoon Kim [Webpage]
    Email: joonk AT gatech DOT edu

    View more contributors »