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 AbstractLocation and From headers. Here, both AbstractLocation 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_Portless.policy
• topo = Frenetic_NetKAT_Portless.topo
• portful_policy = Frenetic_NetKAT.policy

---

Files Added

• lib/Frenetic_NetKAT_Portless.ml

  This modile has the Portless NetKAT language defined. This modile also defines topo which is a simple representation of a topology.

• lib/Frenetic_Portless_Fdd.ml

  Similar to lib/Frenetic_Fdd.ml, this module is used in the compilation process of converting a portless policy into a portful one. We use an FDD to reorder the policies such that all tests come first and all the modifications at the end. This process helps getting rid of corner edge cases that might produce incorrect policies if done naively.

• lib/Frenetic_NetKAT_Portless_Optimize.ml

  Module similar to lib/Frenetic_NetKAT_Optimize.ml and us used by the compiler as a module with some helper functions.

• lib/Frenetic_NetKAT_Portless_Compiler.ml

  This is the module that has functions to compile the local portless NetKAT to a portful one.

• lib/Frenetic_NetKAT_Portless_Generated_Parser.cppo.mly

  Generated parser file similar to lib/Frenetic_NetKAT_Generated_Parser.cppo.mly.

• lib/Frenetic_NetKAT_Portless_Lexer.ml

  The Portless NetKAT Lexer.

• lib/Frenetic_NetKAT_Portless_Parser.ml

  The Portless NetKAT Parser.

• lib/Portless_Parser.cppo.mly

  The grammar file for parsing the Portless NetKAT policies.

• frenetic/Topologies.ml

  Module with simple topologies generation that are the same as mininet default topologies. It can generate minimal, simple, linear, and tree topologies.

Files Modified

• lib/Parser.cppo.mly

  As the tokens are generated only from the lib/Parser.cppo.mly, have added ABSTRACTLOC, FROM ,SWITCHPREFIX, and HOSTPREFIX tokens. The grammar to parse them is all in lib/Portless_Parser.cppo.mly.

• frenetic/frenetic.ml

  Added a start-controller command to frenetic.native that takes in a topology name and a portless policy and installs the tables to the switches on the network. Here the topology name is exactly as put in --topo= argument of mininet.

• _oasis

  OASIS stuff becuase new files were added.

• lib/frenetic.mldylib

  OASIS stuff becuase new files were added.

• lib/frenetic.mllib

  OASIS stuff becuase new files were added.

• lib/frenetic.odocl

  OASIS stuff becuase new files were added.

• setup.ml

  OASIS stuff becuase new files were added.

---

Start Controller Command

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

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

Sample Policies for Fully Connected Networks

$ sudo mn --controller=remote --topo=<topo-name> --mac --arp
$ frenetic start-controller --topo <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

[smolkaj]

Very cool!

May I suggest some modifications? I am a little worried about the amount of (essentially) duplicated code...any change we make in the lexer, parser, compiler, ... now has to be mirrored in a second file. That will quickly lead to bugs and makes hacking a pain.

Here are my suggestions:

• The NetKAT parser already uses macros. Instead of duplicating it, let's just add another macro PORTLESS and generate all three parsers (portfull, portfull ppx, portless) from a single definition.
• Would you be happy with the syntax from = "h1" instead of the current syntax, from = h1? If so, we can reuse the current parser and just add from and loc tokens (that will be rejected by the portfull parser).
• We can exploit an existing feature called "meta fields" (or "logical fields") to dramatically simplify the portless to portful compilation. In fact, it can be done fully syntactically and doesn't require FDDs at all. The feature is explained in some detail here: global meta fields #517. Here is how the compilation will work in pseudo code

portless : portful -> portless
portless(p) = (let `from := port in portless'(p))  (* this is NetKAT syntax *)
where
portless'(from = name) = (sum_{sw} switch = sw; `from = name2srcport(name, sw))
portless'(from := name) = failwith "illegal"
portless'(loc = name) = (switch = name2switch(name))
portless'(loc := name) =  (sum_{sw} switch = sw; port := name2dstport(name, sw))

(EDIT: to avoid blowup in the policy size, we can pull the sum_{sw} all the way to the top)

The function portless' depends on 4 topology dependent primitives:

• summing over all switches of the topology (sum_{sw})
• translating names to switch ids (name2switch : string -> int)
• translating source name, switch id pairs to inport ids (name2srcport : string * int -> int)
• translating destination name, switch id pairs to outport ids (name2dstport : string * int -> int)

With these simplifications, I think we should be able to reduce your PR from +1300 lines of code to about +130.

Does that make sense? I'm happy to help with implementing (any subset of) my proposed changes.

[smolkaj]

@poddarh: I took the liberty to refactor the parser and lexer in the way I described, see frenetic-lang:portless_netkat. All that's left to do is to refactor the portless compiler, now.