KATch² NetKAT Tutorial

This tutorial will guide you through the basics of NetKAT.

Packets and Variables

In NetKAT, a packet is represented as a sequence (or vector) of bits. We use variables like x0, x1, x2, and so on, to refer to these bits. For example, if a packet is 101, then:

x0 would be 1 (the first bit)
x1 would be 0 (the second bit)
x2 would be 1 (the third bit)

Real-World Example: Ethernet Frame

In real networking, packets have structured fields. Here's a simplified Ethernet frame showing how packet bits correspond to actual network data:

Ethernet Frame (simplified)
Dest MAC
48 bits
Src MAC
48 bits
EtherType
16 bits
Payload
46-1500 bytes

                Bit mapping: x0=first bit of Dest MAC, x1=second bit of Dest MAC, x2=third bit, etc.
            

In this example:

x0-x47 would represent the 48-bit destination MAC address
x48-x95 would represent the 48-bit source MAC address
x96-x111 would represent the 16-bit EtherType field
x112 and beyond would be the start of the payload data, but the payload is typically not modeled in NetKAT

NetKAT policies can test or modify any of these bits to implement network behavior like filtering, forwarding, or packet transformation.

Tests (Packet Filters)

Tests are conditions that check the value of a packet bit. They act as filters: if the condition is true, the packet passes through; otherwise, it is dropped (or "filtered out").

Test Filtering: x2 == 1

                101
                →
                ✓ PASS
                →
                101
            

                010
                →
                ✗ DROP
                →
                (no output)
            

                111
                →
                ✓ PASS
                →
                111
            

Try this example in the interactive editor below:

// You can edit this to test different programs x2 == 1 // The analysis results will be displayed here:

You can also test for equality to 0, like x3 == 0.

x1 == 0

Note that the examples displayed are as wide as the largest bit mentioned in the program.

Assignments

Assignments modify the packet's bits. The expression x2 := 1 sets the third bit of the packet to 1, regardless of its previous value.

Assignment Effect: x2 := 1
Before

                            x0=0
                            x1=1
                            x2=0
                        
010
→After

                            x0=0
                            x1=1
                            x2=1
                        
011

Experiment with this assignment in the editor below:

x2 := 1 x2 := 0

Sequential Composition

Sequential composition, denoted by a semicolon ;, combines two NetKAT expressions by executing them one after the other. The packet output by the first expression becomes the input to the second.

Sequential Flow: x2 == 1; x1 := 0
Input
111
→Test x2 == 1
✓ PASS
→Assign x1 := 0
101
→Output
101

See this sequential flow in action in the editor below:

x2 == 1; x1 := 0 x0 == 1; x2 := 0

You can also chain multiple assignments together:

x0 := 1; x2 := 0

Choice (Union)

Choice, denoted by a plus sign +, combines two NetKAT expressions and can be interpreted in two ways:

Nondeterministic Interpretation: The network can choose to follow either path - it's an "either/or" decision where one path is selected.

Multicast Interpretation: The network simultaneously sends copies of the packet down both paths - it's a "both" scenario. This is useful for modeling broadcast scenarios, load balancing, or redundant forwarding where you want a packet to reach multiple destinations.

A + B (Union)
All traces from both sets

x0 := 1 + x1 := 1

Watch the effect of branching in the editor below:

x0 := 1 + x1 := 1 x0 == 1 + x1 := 0

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

Dup (Logging)

The dup keyword is a special NetKAT operator that records the current packet state to the trace output without modifying it. This is extremely useful for observing the packet state at various points in your NetKAT expression.

Dup Logging: x1 := 1; dup; x2 := 1
Input
000
→Assign x1 := 1
010
→dup (log)
010 logged
→Assign x2 := 1
011
→Output
011
Trace Result:
000 → 010 → 011
Three entries: input → logged state → final output

See how dup creates intermediate trace entries in the editor below:

x1 := 1; dup; x2 := 1 x0 := 1; dup; x1 := 1; dup

Iteration (Kleene Star)

Iteration, denoted by an asterisk * (Kleene star) after an expression e (i.e., e*), allows an expression to be executed zero or more times.

Iteration Paths: (x0:=1 + (x0==1;x1:=1) + (x1==1; x2:=1))*

                    Input: 000
                
↓
0 loops
000
‖1 loop
100
‖2 loops
110
‖3+ loops
111

                        Nondeterministic iteration count produces several execution paths
                    
↓

                    Multiple Possible Outputs
                

Explore the multiple iteration paths in the editor below:

((x0:=1 + (x0==1;x1:=1) + (x1==1; x2:=1)); dup)*

This shows multiple paths in the trace, corresponding to 0, 1, 2, etc., iterations, up to a limit defined by the analyzer to prevent infinite loops in the visualization.

((x0 := 0 + x0 := 1); dup)*

Logical Operators

NetKAT expressions represent sets of traces (sequences of packet transformations). NetKAT's logical operators correspond to set operations on these trace sets, making them powerful tools for both constructing complex policies and verifying network properties.

Union (+)

We've already seen the union operator +. From a formal perspective, this represents the set union of traces from both expressions - the result contains all traces that are generated by either the left or right expression. This gives us a third interpretation alongside the nondeterministic and multicast views:

Nondeterministic: Choose one path
Multicast: Send packets down both paths
Set-theoretic: Union of two trace sets

A + B (Union)
All traces from both sets

x0 := 1 + x1 := 1

Intersection (&)

The intersection operator & represents the set intersection of traces. A trace appears in the result only if it's generated by both expressions.

A & B (Intersection)
Only traces in both sets

(x0 == 1) & (x1 == 0)

Symmetric Difference / XOR (^)

The XOR operator ^ represents the symmetric difference of trace sets - traces that are in one set but not both.

A = B when A ^ B is empty

(x0 == 1; x1 == 1) ^ (x0 == 1 ; x1 := 1)

Difference (-)

The difference operator - represents the set difference - traces that are in the first set but not in the second set.

A - B (Difference)
Traces in A but not in B

(x0 == 1) - (x1 == 1)

Using Logical Operators for Verification

These set operations are particularly powerful for network verification:

Subset Check (A ⊆ B)

To verify that the trace set of A is a subset of the trace set of B, check if A - B is empty. If it's not empty, the analyzer will show you traces that are in A's set but not in B's set.

A ⊆ B when A - B is empty

(x0 == 1) - (x0 == 1 + x1 == 1)

Equality Check (A = B)

To verify that two expressions generate the same trace set, check if A ^ B is empty. If it's not empty, the traces show you which traces appear in one set but not the other.

A = B when A ^ B is empty

(x0 == 1; x1 == 0) ^ (x1 == 0 & x0 == 1)

Additional Examples

Click examples on the left to load them into the practice editor, or write your own expressions:

Examples (click to load):

Basic Operations:

x0 := 1 x1 == 0 x0 := 1; x1 := 0

Choice Operations:

x0 := 1 + x1 := 1 (x0 == 1; x1 := 1) + x1 := 0

Iterations:

(x0 == 0; x0 := 1)* ((x0 == 0; x0 := 1); dup)*

Complex Policies:

// Bit flipper with logging (x0 == 0; x0 := 1 + x0 == 1; x0 := 0); dup; x1 := 1 // Conditional assignment chain x0 == 1; (x1 == 0; x2 := 1 + x1 == 1; x2 := 0); dup

Practice Editor

Click examples on the left to load them:

// Click an example to load it x1 == 0

Additional Exercises

Click exercises on the left to load them into the analysis editor with equivalence checking:

Additional Exercises:

(x0 == 0; x0 := 1) + (x0 == 1; x0 := 0) (x0 == 1; x1 := 1) + (x0 == 0; x1 := 0) (x0 == 0; x1 == 0) + (x0 == 1; x1 == 1) (x0 == 0; x1 == 1; x0 := 1; x1 := 0) + (x0 == 1; x1 == 0; x0 := 0; x1 := 1) + (x0 == 0; x1 == 0) + (x0 == 1; x1 == 1)

Exercise Editor:

// Click an exercise to load it x1 == 0

This concludes the basic NetKAT tutorial. Experiment with these constructs to build more complex network policies!

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

With these syntactic extensions, KATch² bridges the gap between the theoretical NetKAT language and practical network programming!

View KATch2 source on GitHub

KATch2 NetKAT Tutorial