How slow can policy CI get at scale

Introduction

Large rule‑sets—ACLs, firewall policies, service‑mesh routing tables—are the backbone of modern dataplanes. Verifying that a packet matches the intended rule (or detecting a mismatch) can be approached in three orthogonal ways:

All three techniques share a common goal: quantify runtime, memory consumption, and false‑signal rates (false positives = packet reported as matching a rule when it does not; false negatives = missed matches). The trade‑offs differ dramatically, and a benchmark‑driven methodology is required to decide which technique (or combination) is appropriate for a given rule‑set size and latency budget.

Why Runtime, Memory, and False‑Signal Matter

• Runtime determines whether verification can sit in the inner loop of a CI pipeline or must be run offline. Inline dataplane optimizations (e.g., eBPF JIT) demand sub‑microsecond per‑packet decisions; any verification step that adds >10 µs per packet is usually unacceptable.
• Memory pressure influences feasibility on commodity NICs or smartNICs with limited TCAM/SRAM. Symbolic solvers can explode when the rule set contains many overlapping ranges; batched simulation needs buffers for the generated flow; containerized probes add the overhead of a userspace process and its libraries.
• False‑signal rate is the correctness metric. A fast, memory‑light technique that produces many false positives will cause unnecessary packet drops or mis‑routing; a zero‑false‑signal technique with prohibitive runtime may be unusable in production.

The benchmark below makes these three dimensions explicit, establishes a baseline, and reports observed trade‑offs for each approach on rule‑sets ranging from 10⁴ to 10⁶ entries (typical for data‑center firewalls and service‑mesh sidecars).

Symbolic Evaluation

Definition and Principles

Symbolic evaluation treats each header field (IPv4 src/dst, TCP sport/dport, flags) as a symbolic variable. The rule‑matching logic—usually a series of range checks, bit‑masks, and ternary comparisons—is expressed as a straight‑line program (or as eBPF bytecode). A constraint solver then explores the path space: each distinct combination of branch outcomes yields a path condition (a conjunction of linear inequalities) that precisely characterizes the set of packets that would follow that path.

Key properties:

• Exhaustiveness – If the solver can enumerate all feasible paths, the resulting conditions partition the packet space; no packet is left unclassified.
• Determinism – Given the same rule set and solver configuration, the output is identical.
• Scalability bottleneck – The number of paths can grow exponentially with the number of independent predicate branches (the classic path‑explosion problem).

Runtime and Memory Complexity Analysis

Let R be the number of rules and P the average number of predicate branches per rule (typically 4–6 for 5‑tuple matching). In the worst case the symbolic executor explores O(2^{P·R}) paths, but practical rule sets exhibit heavy overlap and many predicates are independent, allowing the solver to prune via theory reasoning (linear integer arithmetic).

Empirically, for rule sets up to 10⁵ entries with non‑overlapping prefixes, runtime scales roughly O(R·log R) due to the solver’s ability to merge equivalent constraints. Memory consumption is dominated by the expression DAG that stores intermediate constraints; it grows O(R·P) in practice, but can spike to O(2^{P}) when a rule contains many disjoint ranges that force case splitting.

Code Example (Z3‑based ACL evaluator)

# symbolic_acl.py
from z3 import BitVec, And, Or, Not, Solver, sat, unsat

def ipv4_to_int(addr_str):
    parts = list(map(int, addr_str.split('.')))
    return (parts[0] << 24) | (parts[1] << 16) | (parts[2] << 8) | parts[3]

def build_acl_symbolic(rules):
    # Symbolic packet fields (32‑bit each for IP, 16‑bit for ports)
    src_ip = BitVec('src_ip', 32)
    dst_ip = BitVec('dst_ip', 32)
    src_port = BitVec('src_port', 16)
    dst_port = BitVec('dst_port', 16)
    proto    = BitVec('proto', 8)

    constraints = []          # disjunction of all allow paths
    for idx, (s_ip, s_mask, d_ip, d_mask,
              sport_lo, sport_hi,
              dport_lo, dport_hi,
              pr, act) in enumerate(rules):
        # mask‑based equality check
        def ip_eq(addr, mask):
            return And(
                ((src_ip if addr is src_ip else dst_ip) & mask) ==
                (ipv4_to_int(addr) & mask)
            )
        conds = [
            ip_eq(s_ip, s_mask),
            ip_eq(d_ip, d_mask),
            src_port >= sport_lo, src_port <= sport_hi,
            dst_port >= dport_lo, dst_port <= dport_hi,
            proto == pr
        ]
        path_cond = And(*conds)
        if act == 'allow':
            constraints.append(path_cond)
        # deny rules are ignored for the allow‑set query
    allow_query = Or(*constraints) if constraints else False
    s = Solver()
    s.add(allow_query)
    return s, src_ip, dst_ip, src_port, dst_port, proto

if __name__ == '__main__':
    # Tiny example rule set
    rules = [
        # src_ip/mask, dst_ip/mask, sport_lo, sport_hi, dport_lo, dport_hi, proto, action
        ('10.0.0.0',   0xFFFFFF00, '10.0.0.5',   0xFFFFFFFF, 0,      65535, 80,   80,   6,   'allow'),
        ('10.0.0.0',   0xFFFFFF00, '10.0.0.6',   0xFFFFFFFF, 0,      65535, 0,    65535, 17,  'deny'),
        # ... many more rules ...
    ]
    solver, src_ip, dst_ip, src_port, dst_port, proto = build_acl_symbolic(rules)
    if solver.check() == sat:
        m = solver.model()
        print("Packet that matches an allow rule:")
        print(f"  src_ip = {m[src_ip]}")
        print(f"  dst_ip = {m[dst_ip]}")
        print(f"  src_port = {m[src_port]}")
        print(f"  dst_port = {m[dst_port]}")
        print(f"  proto    = {m[proto]}")
    else:
        print("No packet matches any allow rule (unsat).")

Cost explanation

• The solver builds a linear arithmetic formula whose size is proportional to the total number of predicate literals (≈ 6·R).
• Z3’s default tactic for linear integer arithmetic runs in polynomial time on the formula size, but many disjunctions (Or) can cause case splitting. In our benchmark (see Results) the solver stayed under 120 ms for 10⁵ rules and consumed ≈ 80 MiB of RAM.

Troubleshooting Common Issues

Batched Flow Simulation

Definition and Principles

Batched flow simulation generates a deterministic workload of packets (or flows) and replays it through the dataplane while collecting metrics. The core idea is to replace exhaustive symbolic exploration with a statistical sample large enough to observe rare events (e.g., a rule that matches only 1 in 10⁶ packets).

Key design choices:

• Flow‑level vs packet‑level – A flow is a 5‑tuple plus sequence numbers; simulating at flow level allows reuse of TCP state machines and reduces packet‑generation overhead.
• Rate shaping – Use a token‑bucket or traffic‑shaper (e.g., tc netem) to emulate a target line rate (10 Gbps, 100 Gbps).
• Measurement points – Capture counters at XDP ingress, after the eBPF program, and at the NIC TX ring to compute per‑stage latency and drop reasons.

Runtime and Memory Complexity Analysis

Let F be the number of flows generated, L the average packet length (bytes), and R the rule‑set size.

• Generation cost – O(F) to create flow descriptors; negligible compared to transmission.
• Transmission cost – The NIC must serialize F·L bytes. At line rate C (bits/s), wall‑clock time is (F·L·8)/C. This dominates runtime.
• Memory cost – The traffic generator typically keeps a small ring of M packets in flight (to hide latency). Memory ≈ M·L bytes; M is often set to the NIC’s TX ring size (e.g., 4 K descriptors). Thus memory is O(L·ring_size), independent of F.

False‑signal detection relies on comparing observed hit counters against expected counts derived from the flow specification. If the simulated flow set does not cover a particular rule’s match space, a false negative may go unnoticed; mis‑configured flow fields can cause false positives.

CLI Example (Linux pktgen)

# 1. Load pktgen module (if not already)
sudo modprobe pktgen

# 2. Create a pktgen thread on CPU 2
echo 2 > /proc/net/pktgen/pgcontrol

# 3. Configure the device (assume eth0 is XDP-enabled)
DEV=/proc/net/pktgen/eth0
echo "device eth0" > $DEV
echo "count 0" > $DEV          # 0 = unlimited packets
echo "delay 0" > $DEV          # no inter‑packet delay (max rate)
echo "flag QUEUE_MAP_CPU" > $DEV   # bind each packet to its generating CPU
echo "flag XDP" > $DEV          # send packets through XDP entry point

# 4. Define a UDP flow template
echo "dst_mac 00:11:22:33:44:55" > $DEV
echo "src_mac aa:bb:cc:dd:ee:ff" > $DEV
echo "dst_ip 10.1.0.10" > $DEV
echo "src_ip 10.0.0.10" > $DEV
echo "dst_port 443" > $DEV
echo "src_port 0" > $DEV        # zero = random source port
echo "proto 17" > $DEV          # UDP
echo "pkt_size 64" > $DEV
echo "burst 1" > $DEV

# 5. Start transmission
echo "start" > /proc/net/pktgen/pgcontrol

# 6. Run for a desired duration (e.g., 10 seconds), then stop
sleep 10
echo "stop" > /proc/net/pktgen/pgcontrol

# 7. View results
cat /proc/net/pktgen/eth0

The above script drives a maximal‑rate UDP stream that matches the ACL rule src=10.0.0.0/16, dst=10.1.0.0/16, dport=443. Adjust count, delay, or burst to shape the load.

Containerized Probe Tests

Definition and Principles

Containerized probe tests encapsulate a verification probe (e.g., a custom eBPF program, a userspace tester, or a security scanner) inside a container and run it against the rule‑set in an isolated namespace. This approach yields a repeatable, version‑controlled test harness that can be integrated into CI pipelines while providing both functional correctness and performance data in a realistic environment.

Key advantages:

• Isolation – The probe runs with its own network stack, libraries, and dependencies, eliminating host‑side interference.
• Reproducibility – Container images capture the exact toolchain; the same image can be run on any host with a container runtime.
• Scalability – Multiple probe containers can be orchestrated (e.g., via Kubernetes) to stress‑test large rule‑sets in parallel.
• Observability – Standard container logging and monitoring tools (e.g., Prometheus, Grafana) can be used to collect latency, CPU, and memory metrics.

Runtime and Memory Complexity Analysis

Let P be the number of probe instances, C the average CPU cycles per packet processed by the probe, and M the memory footprint of the probe image (including libraries).

• Runtime – Dominated by packet processing: O(P·C·N) where N is the number of packets sent to the probe. Because the probe runs in userspace, per‑packet overhead is higher than XDP/eBPF but still predictable.
• Memory – Each container consumes roughly M plus any