Portless NetKAT

[poddarh]

Portless NetKAT

Portless NetKAT is a modified version of the NetKAT language for defining policies without ports. The language, takes the regular NetKAT and replaces the Switch and Port header with Location and From headers. Here, both Location and From can take values that either represent a host or a switch.

Simple example policy

Topology:

[h1]----1[s1]2---2[s2]1----[h2]

Portful Policy:

if sw = 1 then
       if pt = 1 then pt := 2
  else if pt = 2 then pt := 1
  else drop
else if sw = 2 then
       if pt = 1 then pt := 2
  else if pt = 2 then pt := 1
  else drop
else drop

Equivalent Portless Policy:

if loc = "s1" then
       if from = "h1" then loc := "s2"
  else if from = "s2" then loc := "h1"
  else drop
if loc = "s2" then
       if from = "h2" then loc := "s1"
  else if from = "s1" then loc := "h2"
  else drop
else drop

Compilation

As the tables that are finally generated need to talk about ports, the Frenetic.Netkat.Portless_Compiler provides a compile function with the following signature:

• val compile: portless_policy -> topo -> portful_policy

where,

• portless_policy = Frenetic.Netkat.Syntax.policy
• topo = Frenetic.Network.Net.Topology.t (not to be confused with Frenetic.Net.Topology.t)
• portful_policy = Frenetic.Netkat.Syntax.policy

The topology can be parsed from dot or gml files using the module Frenetic.Network.Net.Parse NOTE: The labels for devices are used as the switch and host names.

---

The Frenetic.Topology.Mininet Module

This module defnes the type topo_name as follows:

type topo_name =
  | Tree of int * int
  | Linear of int
  | Single of int
  | Minimal

It also defines the function topo_from_name as follows:

val topo_from_name: topo_name -> Frenetic.Network.Net.Topology.t

This function takes in a topo_name and returns the topology representing that name. The generated topology is equivalent to the one that is generated by mininet:

$ mn --topo=<topo_name> --mac

---

Start Controller Command

The frenetic portless-controller command starts a simple controller that installs the local portless policy to the switches on the netowrk. It has the following flags:

• [--policy-file file] containing NetKAT policy to apply to the network. Defaults to policy.kat.
• [--topology-file file] containing .dot topology of network. Defaults to topology.kat.
• [--topology-name name] The name of the topology. Same as mn --topo value. Overrides the --topology-file value if provided.
• [--openflow-port int] Port to listen on for OpenFlow switches. Defaults to 6633.

Sample Policies for Fully Connected Networks

$ sudo mn --controller=remote --topo=<topo-name> --mac --arp
$ frenetic portless-controller --topology-name <topo-name> --pol <pol-file>

topo-name = minimal

Portless Policy:

if from = "h1" then loc := "h2"
               else loc := "h1"

topo-name = single,4

Portless Policy:

     if ethDst = 00:00:00:00:00:01 then loc := "h1"
else if ethDst = 00:00:00:00:00:02 then loc := "h2"
else if ethDst = 00:00:00:00:00:03 then loc := "h3"
else if ethDst = 00:00:00:00:00:04 then loc := "h4"
else drop

topo-name = linear,3

Portless Policy:

if ethDst = 00:00:00:00:00:01 then
         if loc = "s1" then loc := "h1"
    else if loc = "s2" then loc := "s1"
    else if loc = "s3" then loc := "s2"
    else drop
else if ethDst = 00:00:00:00:00:02 then
         if loc = "s2" then loc := "h2"
    else if loc = "s1" then loc := "s2"
    else if loc = "s3" then loc := "s2"
    else drop
else if ethDst = 00:00:00:00:00:03 then
         if loc = "s3" then loc := "h3"
    else if loc = "s2" then loc := "s3"
    else if loc = "s1" then loc := "s2"
    else drop
else drop

topo-name = tree,2,2

Portless Policy:

if loc = "s1" then
         if from = "s2" then loc := "s3"
    else if from = "s3" then loc := "s2"
    else drop
else if loc = "s2" then
         if ethDst = 00:00:00:00:00:01 then loc := "h1"
    else if ethDst = 00:00:00:00:00:02 then loc := "h2"
    else loc := "s1"
else if loc = "s3" then
         if ethDst = 00:00:00:00:00:03 then loc := "h3"
    else if ethDst = 00:00:00:00:00:04 then loc := "h4"
    else loc := "s1"
else

[jnfoster]

Sounds cool to me. Anything to prevent us from merging this @smolkaj ?

[smolkaj]

Cool, looks good!