Skip to content

NetKAT OCaml Syntax

Craig Riecke edited this page Jun 21, 2016 · 3 revisions

You have two options for creating SDN applications in OCaml:

  • You can create NetKAT predicates and policies through function calls.
  • The NetKAT Surface Syntax can be used as a camlp4 extension.

NetKAT With Function Calls

This requires the Frenetic_NetKAT module in your code.

Predicates

A predicate is a boolean condition for matching packets. It's generally used in filter and IfThenElse policies, outlined in the next section.

Primitives

All primitives require integer (int32 or int64) values. You can use OCaml hex constants, or convert MAC address colon-separated hex by calling Frenetic_Packet.mac_of_string(str), or IPv4 dotted notation with Ipaddr.V4.to_int32(str).

Predicate Matches Packets With...
False matches no packets
Test(EthDst 1824509238475L) Ethernet destination address: a 48-bit integer.
Test(EthSrc 1824509238475L) Ethernet source address: a 48-bit integer.
Test(EthType 0x800) Ethernet type. For VLAN packets, this is the type of the inner packet, per OpenFlow 1.0
Test(IP4Dst (245323452345l,32l)) IPv4 desintation address and mask
Test(IP4Src (245323452345l,32l)) IPv4 source address and mask
Test(IPProto 6) IPv4 protocol number or ARP opcode. Must be decimal and fit in 16 bits.
Test(Location (Physical 2)) Ingress port number. Must be less than 65520
Test(Switch 1981745) Ingress switch datapath ID.
Test(TCPSrcPort 12834) TCP/UDP source port
Test(TCPDstPort 80) TCP/UDP destination port.
True matches all packets
Test(Vlan 1000) VLAN id.
Test(VlanPcp 1) VLAN PCP. priority code point.

Combinations

Predicate Matches Packets With...
Neg pred equivalent to not pred
And (pred1, pred2) both pred1 and pred2 are true
Or (pred1, pred2) either one of pred1 or pred2 or both are true

Policies

A NetKAT policy directs the switch to perform an action on a packet.

Primitives

Policy Does This With a Packet...
drop Drops the packet
Filter(pred) Accepts all packets that meet the predicate. Drops any other packets
id Accepts all packets
Mod(EthDst 1824509238475L) Ethernet destination address: a 48-bit integer.
Mod(EthSrc 1824509238475L) Ethernet source address: a 48-bit integer.
Mod(EthType 0x800) Ethernet type. For VLAN packets, this is the type of the inner packet, per OpenFlow 1.0
Mod(IP4Dst (245323452345l,32l)) IPv4 destination address and mask
Mod(IP4Src (245323452345l,32l)) IPv4 source address and mask
Mod(IPProto 6) IPv4 protocol number or ARP opcode. Must be decimal and fit in 16 bits.
Mod(Location (Physical 2)) Send to egress port number. Must be less than 65520
Mod(Location (Pipe "tag")) Send to controller
Mod(Location (Query "tag")) Send to statistics bucket
Mod(TCPSrcPort 12834) TCP/UDP source port
Mod(TCPDstPort 80) TCP/UDP destination port.
Mod(Vlan 1000) VLAN id.
Mod(VlanPcp 1) VLAN PCP. priority code point.

Combinations

Policy Does This With a Packet...
Seq(pol1, pol2) Do pol1, then (possibly) pol2 in sequence
Union(pol1, pol2) Make copy of a packet, then simultaneously execute pol1 and pol2 on the copies

Example

Seq (
  Filter (Test (Switch 2)),
  Union(
    Union(
      (Seq (Filter (And (Test (EthType 0x800)) (Test (IP4Src 9834579087L))) (Mod (Location (Physical(1)))),
      (Seq (Filter (And (Test (EthType 0x800)) (Test (IP4Src 9834579088L))) (Mod (Location (Physical(2))))
    ),
    (Seq (Filter (And (Test (EthType 0x800)) (Test (IP4Src 9834579089L))) (Mod (Location (Physical(3))))
  )  
)

NetKAT With camlp4 Syntax Extension

The NetKAT camlp4 Syntax Extension currently doesn't work. See https://github.com/frenetic-lang/frenetic/issues/507

This option is the easier, but uses camlp4 which has been effectively deprecated by the OCaml programming community. To use it in the Frenetic User VM, simply compile your program with the supplied netkat-build command. This loads the syntax extension and applies it to your code.

To use NetKAT inside your OCaml program, you use <:natkat<...>> and the NetKAT Surface Syntax inside:

open Frenetic_NetKAT
  (* ... *)
  let out_port = 5 in 
  let pol = <:netkat< filter(port = 1) ; port := $out_port >> in ...

You can pass variables into the NetKAT policy and predicates, as we did with $out_port above. You can form combinations of policies in loops and conditionals. This turns the NetKAT Surface Syntax into a full-blown dynamic language.

To compile the program:

   $ netkat-build Your_Program.d.byte
   $ ./Your_Program.d.byte

Alternatively, you can compile the program into native machine language by using the .native suffix. This is similar to other OCaml framework tools like core-build.

Generally, you use the NetKAT extensions in an OCaml SDN program, which we discuss here.