Welcome back. In this lecture, we will continue our discussion of verification. And in particular, we will talk about control plane verification using a controller called Kinetic. Changes to the network configuration are common. Based on some studies that we've done in the past, we've found that a network might experience anywhere from 1,000 to 18,000 network configuration changes in a single month. Now some of these changes can be automated with scripts and other network management systems, but there's still no way to reason concretely about these changes. In particular, an operator has very little assurance that a particular configuration change would ultimately result incorrect behavior. Network operators need domain specific support for expressing the dynamics of the control program so that they can have better assurance that the network will behave as they intend it to behave when a particular event, such as an intrusion, an authentication event or traffic shift occurs. Kinetic enables verifiable, event based network control. Network policies are represented as finite state machines, where each finite state machine maps to a pyretic policy. One of the nice properties of finite state machines is that they're verifiable. In particular, finite state machines are amendable to verification techniques including model checking as we'll see later in this lesson. Pyretic enables Sequential Composition of finite state machines which makes it easier for a network operator to express policies. It also allows the expression of policies with finite state machines to scale, which makes it more tractable not only to express policies, but also to verify them. Here's a high level diagram showing the kinetic system architecture. Kinetic is based on the Pyretic runtime. On top of Pyretic, Kinetic adds event drivers that handle certain types of external events. These external events can really be any type of external event that you could encode with a JSON message. A JSON event handler enables kinetic to handle a broad range of events. These events might include anything from traffic shifts to intrusions, to authentication events, to host arrival and departures, to even timing events. A kinetic program includes a composition of finite state machines, mechanisms to hook up these events to a program and something that's called an LPEC, or located packets equivalence class, projection map. It figures out how to map flows to individual finite state machines. Using a kinetic library, a programmer can then express which parts of float space mapped to each finite state machine, or program, and how these finite state machines relate to one another. This particular expression also turns out to be amenable to verification. The Kinetic Language Architecture is an extension to Pyretic. We add a special dynamic policy class called an FSM policy. That FSM definition in turn includes variable definitions. Those variable definitions each have a type, an initial value, and an associated transition functions, or transitions where transition refers to a function that is called when the transition occurs. Here's an example of a simple kinetic policy that takes input from an intrusion detection system. It simply indicates whether a host is infected or not. There are two types of transitions in kinetics, an exogenous transition, that's triggered by an external event which might be a JSON message from an intrusion detection system. And an androgynous transition, it's triggered by a change in an internal variable. Here in our FSM definition, we define an internal variable called infected. That internal variable is a bullion that has an initial value of false. A transition on that variable simply results in an update to the value of the internal variable for infected. So a transition simply updates the value of infected to true or false, depending on the message that his passed as an external event. We also define a second variable called policy which determines the Pyretic policy that will be applied in any state. This particular policy variable can take two possible values, drop or identity. Note that those are simple Pyretic policies or we can actually refer to more complex Pyretic policies. The initial value for this variable is identity and the transition function is the policy function that we've defined above. This particular transition function, hence, the current value of the internal variable for infected. If that infected variable is true, the transition function sets the current policy to be dropped. Otherwise, the default policy is identity. We can see in the finite state machine, that an exogenous event causes the transition of the infected variable between false and true and the transition of that internal variable in turn, causes the endogenous transition of the policy variable. Let's take a closer look at the LPEC, or the located packet equivalence class. The LPEC defines the granularity on which this finite state machine is defined. In particular, it defines the granularity on which we want policies to transition. In the case of an intrusion detection system, we might want policies to transition on a host-level granularity. So we define the LPEC according to the source IP address as in line 18 and step 3 here. An advantage to kinetic is that the policies that we've defined can easily translate to the language of a model checker called NuSMV. The model checker allows us to check properties that are specified in a language called CTL or computation tree logic. Here are some example assertions that we have expressed in CTL. For example, we can say that if in an infection event arrives, the system should eventually drop the packet. The modifier A, suggests that this policy always holds and the modifier G indicates that this policy, for any execution path. Likewise, we can say that if an infection is cleared, the controller should transition to the identity policy. We can also test other properties. For example, we can say that from any state, it's always possible to return to the identity policy. And for all paths, a policy should allow a packet until an infection occurs. One of the powerful aspects with CTL is that properties can be checked before the program ever executes. In our experience thus far with kinetic, many programmers find errors in their finite state machine logic and their policies before they even run the program. Kinetic actually executes the new SMV model checker on the programs that you define as you start the controller. So, it's very easy to determine whether the control program has errors, before your control program even runs. Let's have a quick look at Kinetic in action. First we'll have a quick look at the source code and the steps that you must take to write a kinetic program. The first step is to define an LPEC function. In this case, we've defined packets with the same source IP to have a same state or to be part of the same LPEC. We then define our transition function as we've discussed. Next, we define the FSM description. And finally, we set up policy and events screens. Once we have defined our dynamic policy in this fashion, we can instantiate it. And because this is an FSM policy, we can call a function that converts the FSM definition for this policy into a string that can be passed directly to the new SMV model check. Once we have instantiated our model checker, we can then specify CTL assertions that we can check using the new SMV model checker. Once we've added those specifications, we can then directly invoke verification from our pyretic program. Finally, we can invoke the pyretic program as usual. Let's take a quick look at the kinetic IDS in action. First, we start the kinetic IDS. You can see that in addition to starting up the controller as usual, the controller also model-checks the policies that we've specified. We now start a simple 3-node, single-switched topology that connects to this control. By default, each one can ping H2. If we use the JSON message sender, to send an infected event to our controller, we can see that the controller no longer permits the host to communicate to one another because the LPEC associated with H1 has transitioned to the state, where infected is true. We can use the JSON sender to reset the value of infected to false, which will in turn cause the endogenous transition of the policy variable, that once again allows traffic to flow between the two hosts. In summary, event-based control is a common idiom. Operators need ways to efficiently express dynamic properties of network control as well as easy ways to verify them. While other approaches make it possible to verify data-plane state, we also need ways to verify dynamic properties of network control. Kinetic provides a way of verifying dynamic network control. Policies are expressed as finite state machines that map very naturally to model checkers such as new SMV. In the case of kinetic, the policies that you write automatically translate to syntax that can be checked with the new SMV model checker. Once kinetic policies are translated to new SMV, a huge array of properties can be checked using the CTL language.
