Programming and Reasoning with KAT - Lab 2

This lab consists of an interactive tutorial that introduces some convenient syntactic sugar, followed by exercises encoding network topologies and forwarding tables in NetKAT

Encoding If-Then-Else

NetKAT can express conditional logic (if-then-else) by combining tests, assignments, and choice. The general pattern for "if C then P1 else P2" is: (C; P1) + (not C; P2).

Test Negation (!)

KATch² provides the ! operator for negating test conditions. This operator can only be applied to test expressions (not arbitrary NetKAT programs):

Test Negation Examples

!(x0 == 1) - True when x0 is NOT 1 (equivalent to x0 == 0)
!(x0 == 1 & x1 == 1) - True when NOT both are 1
!!(x0 == 1) - Double negation, same as x0 == 1

The negation is implemented using De Morgan's laws during desugaring.

!(x0 == 1) !(x0 == 1 & x1 == 1)

If-Then-Else Syntactic Sugar

Instead of manually encoding conditionals with choice operators, KATch² provides convenient if-then-else syntax:

If-Then-Else Syntax

if condition then expr1 else expr2

This is automatically desugared to: (condition; expr1) + (!condition; expr2)

The condition must be a test expression (something that filters packets).

if x0 == 1 then x1 := 1 else x1 := 0 if x0 == 1 & x1 == 0 then x2 := 1 else if x0 == 0 then x2 := 0 else x2 := 1

If-Then-Else Decision: if x0 == 1 then x1 := 1 else x1 := 0

          Input Packet
        
↓

          Test: x0 == 1?
        
↙
              YES (x0 == 1)
            
↓
x1 := 1
Then branch
↘
              NO (!(x0 == 1))
            
↓
x1 := 0
Else branch
↓

          Result: x1 matches x0
        

Compare the manual encoding with the syntactic sugar:

(x0 == 1; x1 := 1) + (!(x0 == 1); x1 := 0) if x0 == 1 then x1 := 1 else x1 := 0 if x1 == 0 then x0 := 1 else x0 := 0

Syntactic Sugar for Modeling Real Networks

KATch² provides additional syntactic constructs to make it easier to work with real network packets, which often contain multi-bit fields like IP addresses, ports, and protocol numbers.

Bit Range Tests and Mutations

Instead of testing or modifying individual bits, you can work with ranges of bits that represent packet fields:

Bit Range Syntax

x[start..end] - References bits from position start (inclusive) to end (exclusive)
x[0..8] ~ 255 - Tests if the first byte equals 255
x[0..8] := 10 - Sets the first byte to 10

The bit range notation follows Rust-style syntax where the end index is exclusive.

x[0..8] ~ 255 x[8..16] := 192

Working with Different Literal Formats

Bit ranges can be tested or set using various literal formats:

x[0..4] ~ 0b1010 x[0..8] := 0xFF x[0..32] ~ 192.168.1.1

Let Aliases for Bit Ranges

To make policies more readable, you can create named aliases for bit ranges using the let syntax:

Alias Syntax

let alias = &x[start..end] in expression

Creates an alias that can be used in tests and assignments within the expression.

let ip = &x[0..32] in ip ~ 192.168.1.1 let src_ip = &x[0..32] in let dst_ip = &x[32..64] in src_ip ~ 10.0.0.1 & dst_ip ~ 10.0.0.2 let port = &x[64..80] in port := 8080

Real-World Example: Simple Firewall Rule

Here's how you might model a firewall rule that accepts HTTP traffic (port 80) from a specific subnet:

let src_ip = &x[0..32] in let dst_port = &x[48..64] in // Accept if source is in 192.168.1.x and destination port is 80 (src_ip ~ 192.168.1.1 + src_ip ~ 192.168.1.2 + src_ip ~ 192.168.1.3) & dst_port ~ 80

Let Bindings for Expressions

Beyond bit range aliases, let can bind any NetKAT expression to a variable for reuse:

Expression Binding Syntax

let var = expression1 in expression2

Binds expression1 to var, which can be used in expression2.

let is_local = x[0..8] ~ 192 & x[8..16] ~ 168 in is_local; x[32..40] := 1 let setup_defaults = x[0..8] := 10; x[8..16] := 0; x[16..24] := 0; x[24..32] := 1 in x[32..40] ~ 80; setup_defaults

Combining Features: NAT Example

Here's a more complex example that combines bit ranges, aliases, and let bindings to model a simple NAT (Network Address Translation) rule:

let src_ip = &x[0..32] in let dst_ip = &x[32..64] in let is_private = src_ip ~ 192.168.1.1 + src_ip ~ 192.168.1.2 in let is_external = dst_ip ~ 8.8.8.8 + dst_ip ~ 1.1.1.1 in // If source is private and destination is external, rewrite source to public IP is_private & is_external; src_ip := 203.0.113.1

Pattern Matching with the ~ Operator

KATch² supports flexible pattern matching for IP addresses and bit ranges using the ~ operator. This makes it easy to express common network matching patterns without writing complex bit-level tests.

Exact IP Matching

The simplest form matches an exact IP address:

let src = &x[0..32] in src ~ 192.168.1.100

CIDR Notation (Prefix Matching)

Use CIDR notation to match IP prefixes/subnets:

let src = &x[0..32] in src ~ 192.168.1.0/24 + // Matches 192.168.1.0 - 192.168.1.255 src ~ 192.168.2.0 let dst = &x[32..64] in // Match private networks dst ~ 10.0.0.0/8 + dst ~ 172.16.0.0/12 + dst ~ 192.168.0.0/16

IP Range Matching

Match arbitrary IP ranges using the hyphen syntax:

let src = &x[0..32] in // Match IPs from 10.0.0.1 to 10.0.0.10 src ~ 10.0.0.1-10.0.0.10

This works efficiently even for very large ranges:

let ip = &x[0..32] in // These large ranges are handled efficiently without expanding to millions of tests ip ~ 10.0.0.0-10.255.255.255 + // 16 million IPs ip ~ 172.16.0.0-172.31.255.255 + // 1 million IPs ip ~ 192.168.0.0-192.168.255.255 // 65 thousand IPs

Wildcard Masks

For complex patterns, use wildcard masks (similar to Cisco ACLs):

let dst = &x[32..64] in // Match 192.168.X.1 where X can be any value dst ~ 192.168.1.1 mask 0.0.255.0

Pattern Matching with Different Literal Formats

Patterns work with all literal formats, not just IP addresses:

let port = &x[0..16] in let proto = &x[16..24] in // Match port ranges using decimal port ~ 1024-65535 & // Unprivileged ports // Match using hex (e.g., protocol numbers) proto ~ 0x06 + // TCP (6) proto ~ 0x11 + // UDP (17) proto ~ 0x01 // ICMP (1)

Combining Patterns

Build complex filters by combining patterns:

let src = &x[0..32] in let dst = &x[32..64] in let port = &x[64..80] in // Allow internal to DMZ on web ports (src ~ 192.168.1.0/24) & // Internal network (dst ~ 10.0.1.0/24) & // DMZ network (port ~ 80 + port ~ 443) + // HTTP/HTTPS // Allow established connections back (src ~ 10.0.1.0/24) & // From DMZ (dst ~ 192.168.1.0/24) & // To internal (port ~ 1024-65535) // High ports (established)

Performance Note

All pattern matching is optimized to use efficient algorithms. Even patterns matching millions or billions of IP addresses (like 0.0.0.0-255.255.255.255) are handled efficiently without expanding into huge expressions. The implementation uses binary decision techniques that keep the expression size proportional to the number of bits, not the number of addresses matched.

Practical Applications

These features make it much easier to:

Model real packet headers with meaningful field names
Write readable policies that match how network engineers think
Test complex network configurations with actual IP addresses and ports
Build reusable components with let bindings

Network Verification in NetKAT

In the rest of this tutorial, we will assume that packets have four fictitious headers:

switch a 4-bit value encoding the switch where the packet is located,
port a 4-bit value encoding the port where the packet is located,
src a 32-bit value encoding the packet's source address, and
dst a 32-bit value encoding the packet's destination address.

let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in sw ~ 0x1 & pt ~ 0xF For the remaining exercises, we will use this topology:

let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in sw ~ 0x1 & pt ~ 0x1 + sw ~ 0x2 & pt ~ 0x2 + sw ~ 0x3 & pt ~ 0x3 let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in let topo = if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 in let switch = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let edge = sw ~ 0x1 & pt ~ 0x1 + sw ~ 0x2 & pt ~ 0x2 + sw ~ 0x3 & pt ~ 0x3 in let net = edge; (switch; topo)*; switch; edge in net let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in sw ~ 0x1 & pt ~ 0x1 & dst ~ 10.0.3.3; sw := 0x3; pt := 0x3 let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in let topo = if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 in let switch = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let edge = sw ~ 0x1 & pt ~ 0x1 + sw ~ 0x2 & pt ~ 0x2 + sw ~ 0x3 & pt ~ 0x3 in let net = edge; (switch; topo)*; switch; edge in let spec = sw ~ 0x1 & pt ~ 0x1 & dst ~ 10.0.3.3; sw := 0x3; pt := 0x3 in sw ~ 0x1 & pt ~ 0x1 & dst ~ 10.0.3.3; net ^ spec let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in let topo = if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 in let switch = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let edge = sw ~ 0x1 & pt ~ 0x1 + sw ~ 0x2 & pt ~ 0x2 + sw ~ 0x3 & pt ~ 0x3 in let net = edge; (switch; topo)*; switch; edge in let spec = if edge then if dst ~ 10.0.1.1 then sw := 0x1; pt := 0x1 else if dst ~ 10.0.2.2 then sw := 0x2; pt := 0x2 else if dst ~ 10.0.3.3 then sw := 0x3; pt := 0x3 else 0 else 0 in net ^ spec let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in let topo = if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 in let switch1 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let switch2 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let switch3 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x2 else 0 in let switch = sw ~ 0x1; switch1 + sw ~ 0x2; switch2 + sw ~0x3; switch3 in let edge = sw ~ 0x1 & pt ~ 0x1 + sw ~ 0x2 & pt ~ 0x2 + sw ~ 0x3 & pt ~ 0x3 in let net = edge; (switch; topo)*; switch; edge in net let sw = &x[0..4] in let pt = &x[4..8] in let src = &x[8..40] in let dst = &x[40..72] in let topo = if sw ~ 0x1 & pt ~ 0x2 then sw := 0x2; pt := 0x1 else if sw ~ 0x1 & pt ~ 0x3 then sw := 0x3; pt := 0x1 else if sw ~ 0x2 & pt ~ 0x1 then sw := 0x1; pt := 0x2 else if sw ~ 0x2 & pt ~ 0x3 then sw := 0x3; pt := 0x2 else if sw ~ 0x3 & pt ~ 0x1 then sw := 0x1; pt := 0x3 else if sw ~ 0x3 & pt ~ 0x2 then sw := 0x2; pt := 0x3 else 0 in let switch1 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let switch2 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x3 else 0 in let switch3 = if dst ~ 10.0.1.1 then pt := 0x1 else if dst ~ 10.0.2.2 then pt := 0x2 else if dst ~ 10.0.3.3 then pt := 0x2 else 0 in let switch = if sw ~ 0x1 then switch1 else if sw ~ 0x2 then switch2 else if sw ~ 0x3 then switch3 else 0 in let net = switch; topo in 1 & (net; net*)