NetKAT Surface Syntax

The NetKAT "native" syntax is used for the Frenetic subcommands dump, compile-server and shell. It's also printed in log files when the verbosity=debug option for the http-controller subcommand. NetKAT surface syntax files are usually stored in .kat files, but this extension is not required.

This syntax has the following benefits:

• It's the most compact, least "noisy" of the NetKAT syntax choices
• It's easy to write experimental programs in it. These programs can be fed to dump or shell to quickly examine the resulting flow tables.
• It's the syntax used in the Frenetic research papers (http://frenetic-lang.org)

And the following limitations:

• It cannot express dynamic programs. The rules expressed in a .kat file are fixed.
• It does not have any variables, loops, or other constructs. However, you can use OCaml tied with NetKAT surface syntax.
• It requires careful examination of precedence rules

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

Predicate	Matches Packets With...
false	matches no packets
ethDst = 01:4a:6f:22:1f:42	Ethernet destination address: most common format is 6-byte colon-separated hex
ethSrc = 01:4a:6f:22:1f:42	Ethernet source address
ethType = 0x800	Ethernet type. For VLAN packets, this is the type of the inner packet, per OpenFlow 1.0
ip4Dst = 192.168.57.100	IPv4 desintation address: either host 192.168.57.100 or a CIDR-format network 192.168.57.0/24
ip4Src = 192.168.57.100	IPv4 source address: either host 192.168.57.100 or a CIDR-format network 192.168.57.0/24
ipProto = 6	IPv4 protocol number or ARP opcode. Must be decimal and fit in 16 bits.
port = 2	Ingress port number. Must be less than 65520
switch = 1981745	Ingress switch datapath ID.
tcpSrcPort = 12834	TCP/UDP source port
tcpDstPort = 80	TCP/UDP destination port.
true	matches all packets
vlan = 1000	VLAN id.
vlanPcp = 1	VLAN PCP. priority code point.

Combinations

Predicate	Matches Packets With...
( pred )	the given predicate matching. The parentheses technically do not nothing, but override precedence rules
not pred	the given predicate not matching
pred1 and pred2	both pred1 and pred2 matching
pred1 or pred2	either pred1 or pred2 matching

not has highest precedence, meaning it binds the most tightly and is executed first, followed by and then or. This is the precedence order found in most programming languages as well.

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
ethDst := 01:4a:6f:22:1f:42	Sets the ethernet destination address: most common format is 6-byte colon-separated hex
ethSrc := 01:4a:6f:22:1f:42	Sets the ethernet source address
ethType := 0x800	Sets the ethernet type. For VLAN packets, sets inner packet type
filter pred	Accepts all packets that meet the predicate. Drops any other packets
id	Accepts all packets
ip4Dst := 192.168.57.100	Sets the IPv4 desintation address. The address must be a 4-byte dotted notation host
ip4Src := 192.168.57.100	Sets the IPv4 source address. The address must be a 4-byte dotted notation host
ipProto := 6	Sets the IPv4 protocol number or ARP opcode. Must be decimal and fit in 16 bits.
port := 3	Send packet to a particular egress port, an integer less than 65520
port := pipe("tag")	Sends packet to the OpenFlow controller.
port := query("tag")	Counts packet in a statistics bucket named tag.
tcpSrcPort := 12834	Sets the TCP/UDP source port
tcpDstPort := 80	Sets the TCP/UDP destination port.
vlan := 1000	Sets the VLAN id. Implicitly wraps the packet in a VLAN header
vlanPcp := 1	Sets the VLAN PCP, priority code point. Implicitly wraps the packet in a VLAN header.

Combinations

Policy	Does This With a Packet...
( pol )	Executes pol. Technically the parentheses do nothing but overrides precedence rules.
pol1 ; pol2	Executes pol1, then (possibly) pol2 in sequence.
`pol1	pol2`
begin pol end	Executes pol. Like parentheses, technically the begin/end does nothing but overrides precedence rules.
if pred then truepol else falsepol	Evaluates the predicate and, if true, executes truepol. Otherwise it executes falsepol

; has the highest precedence, meaning it binds tighter than other operators and is executed first. | has next highest, followed by if-then-else.

Example

filter switch = 1; begin
  if ethSrc=00:00:00:00:00:01 then port := 1
  else if ethSrc=00:00:00:00:00:02 then port := 2
  else if ethSrc=00:00:00:00:00:03 then port := 3
  else port := 4
end
|
filter switch = 2; begin
  filter (ethTyp=0x800 and ip4Src = 192.168.0.1); port := 1
  | filter (ethTyp=0x800 and ip4Src = 192.168.0.2); port := 2
  | filter (ethTyp=0x800 and ip4Src = 192.168.0.3); port := 3
end

Some more examples are in the code repository under /examples. You can run these with frenetic shell using the given Mininet canned or custom topology, then use ping in Mininet to test.

NetKAT File	Mininet Canned Toplogy	Mininet Custom Topology
abfattree-test1.kat	--topo=single,2 --mac
abfattree-testlocal.kat		sudo python examples/abfattree-testlocal.mn.py
diamond.kat		sudo python examples/diamond.py
drop.kat	Any	Any
example1.kat	--topo=single,3
test.kat	--topo=single,2
tree-2-2.kat	--topo=tree,2,2

Special Predicates and Policies for Global Compilation

The following policy can be used in a global NetKAT file for frenetic dump global.

Policy	Does This To a Packet...
sw1@p1 => sw2@p2	Establishes a link between switch sw1, port p1 and switch sw2, port p2.

Some example global compilations files are in the code repository under /examples/global. See the README file there for directions.

Special Predicates and Policies for Virtual Compilation

Virtual predicates are generally used in the vtopo, ving veg and vrel files for frenetic dump virtual. They can also be used in filter and if-then-else in the ving_pol and vpol files.

Predicate	Matches This Packet...
vfabric = 1	With the given virtual fabric
vport = 2	With the given virtual port
vswitch = 98745	With the given virtual switch DPID

Virtual policies are generally used in the ving_pol and vpol files for frenetic dump virtual.

Policy	Does This With a Packet...
vsw1@vp1 => vsw2@vp2	Establishes a virtual link between vswitch vsw1, port vp1 and vswitch vsw2, port vp2.
vfabric := 1	Sets the virtual fabric for the packet
vport := 2	Sets the virtual port for the packet
vswitch := 98745	Sets the virtual switch DPID for the packet

Some example global compilations files are in the code repository under /examples/virtual. See the README file there for directions.