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.
