Kinetic: Event-Based SDN Control (text)

by Sasha Shkrebets — last modified Mar 20, 2023 08:08 AM

In this lecture, we'll talk about Kinetic, which provides new capabilities for SDN control.

Welcome back.

In this lecture, we'll talk about Kinetic, which provides new capabilities for

SDN control.

Such as the ability to implement a dynamic network

control program that handles arbitrary network events,

such as intrusions, shifts in traffic load, and so forth.

Kinetic also allows an operator to verify that a program is correct

in the sense that it will react properly when particular network events occur.

There are all kinds of different network events, such as traffic load shifts,

security incidents.

Things that relate to users, such as authentication, data usage,

as well as things that relate to the data plan, such as topology changes and

switch and link failures.

For different kinds of events, network operators may react in different ways.

For example, if a host is infected, operators might decide to react in

different ways depending on who or what the event pertains to.

For example, an operator might decide to only block that infected host or

to block all communications in the network.

The operator might also decide to direct communication for that host some

internal garden wall post, which is something you'll do in the assignment.

Main insight in Kinetic is network events and dynamic reactions to them should be

programmatically encoded in the network control program by operators, rather than

requiring network corporators to react manually when these types of event occur.

A Dynamic Network Control Program is a software program that

embeds event-reaction relationships in the control program itself, so

that when network events occur, the software program can update policies.

Which in turn,

affect the flow table entries that are installed in switches in the data plane.

Kinetic tackles some important questions.

So how to invent event reaction logic software and how to verify

the control program will make the appropriate changes when an event occurs.

Kinetic is a domain specific language and a control program.

It helps network operators create SDN control programs that embed custom

event-reaction relationships.

Kinetic also automatically verifies if the program that an operator writes is correct

and says if it conforms to temporal constraints that the operator specifies.

We'll look at some of those later in this lecture.

Kinetic's approach is to provide a domain specific language that's constrained,

but structured enough to make it possible for

network operators to express these configurations.

An operator expresses how network behavior should change in

terms of finance state machine.

This makes it possible for a network operator to verify programs' correctness

with a model checker like NuSMV,

which is well suited to checking programs that are expressed in this fashion.

Kinetic's domain specific language borrows some extractions from Pyretic.

Such as encoding forwarding behavior in a policy variable.

But it provides new constructs and functions that'll allow an operator to

express these policies in ways that respond to changing conditions.

So, as network events arrive, the controller

can determine which policy variable is running at any particular time.

And thus, how switches should forward traffic.

Here's a simple example that we'll explore in some more detail.

A particular event might be an intrusion detection system.

It raises an infected event.

State, in this case,

is the policy variable's value, which is to either allow or block the packet.

When an event occurs, changing the infected state to true.

The policy variable changes from allowing the traffic from that host to blocking it.

Kinetic instantiates FSM instances per flow.

This makes it possible to represent state in a way that's linear

in a number of hosts, rather than geometric.

To decompose network policy in this way

we use Pyretic's parallel composition operator.

An important abstraction in Kinetic is the LPEC, or

the located packet equivalence class.

In the IDS example, a flow is defined by a source IP address or the host.

Other policies might require more flexibility

such as the ability to group packets by location.

Here's an example of how an operator can define an LPEC in Kinetic.

To do so, the operator simply defines the LPEC function to return a match.

Based on any combination on flow spaced headers.

Kinetic also performs automated verifications of

correctness of a program that an operator writes.

The programmer can specify various temporal properties, and

the controller verifies both current and

future forwarding behavior, based on these network events.

Furthermore, verification is automated.

Kinetic's constrained but

structured language allows the controller to automatically parse and

translate the program into a program that can be verified by a model checker.

Furthermore, its verification is run before the program is actually deployed.

When an operator runs a Kinetic program, that program is translated

into a finite state machine model that can be directly tested against

user specified temporal properties in a model checker called NuSMV.

That model checker then returns either true,

indicating that those temporal properties have been satisfied, or

false with a counter example of how those properties have been violated.

Examples of temporal properties, include things like,

if a host is infected, drop all packets from that host.

This constraint is expressed in a logic called computation tree logic, or

CTL as you can see here.

Another temporal property that an operator may wish to verify

is if a host is authenticated by either the web authentication portal or

802.1X and is not infected, packets should never be dropped.

Here's an example of how that's expressed in CTL.

To write a kinetic program,

an operator defines a Pyretic dynamic policy that has a special structure.

There are four steps in writing such a program.

The first is to define the LPEC function.

In this case we've defined that packets with the same source IP will have the same

state in the finance state machine that we defined.

We then defined the transition functions for the finance state machine.

In this case we have an infected function which simply

returns the infected variables and value.

And a policy function, which changes the value of the Kinetic

policy that is run, depending on the value of infected.

In this case, if the infected variable is true,

the Kinetic program changes its policy to drop.

We then define the finance state machine using these two functions.

And finally we set up mechanisms for listening to these events.

In the main function we simply instantiate this dynamic policy.

And once we've instantiated that policy, we can ask various questions about it.

Using CTL, and ask the NuSMV model checker to verify that

the policy conforms to these constraint.

Finally, we can sequentially compose the policy that we've defined

with the default flooding policy.

Let's take a look at Kinetic in action.

We'll first start a default topology in Mininet.

Note that before the controller starts it runs the new SNV model checker

to verify that the policy that we've written

matches the temporal constraints that we've defined.

You can see by default that h1 can ping h2, but

if I send an event to the controller indicating that each one is infected.

Suddenly, we see that each one can no longer send traffic.

If at a later point the host is no longer infected, an event indicating

that the infected state is false, could be sent to the controller.

At which point,

h1's ability to send traffic to the rest of the network resumes.

Kinetic has been deployed on campus networks,

as part of a functional access control system,

as well as in home networks to implement a usage-based access control system.

In summary, Kinetic is a domain specific language and

control platform that encodes event-reaction logic.

We perform the user study that shows that it's much easier to express dynamics in

the network, and it also helps to reduce the number of lines of code

to express these types of event base control programs.

It scales well to large networks and many events.

And its verification process can effectively reduce bugs

in the programs that operators write that require reactions

to these types of network events.