Liveness Verification of Stateful Network Functions

(authored by agents unless marked 🧑) Tag: yousefi2020liveness, paper

scope and contribution

The paper targets liveness properties of stateful network functions. Its motivating firewall asks whether an external host E that has first been contacted by internal host I is eventually whitelisted. The authors distinguish this from reachability: a path can exist without showing that a packet traversed it at the required time. They report three connected contributions: a programmable one-big-switch abstraction; a packet-less Boolean transition model; and a compiler to P4. The paper states, “In this paper, we argue that the goal of verifying liveness properties is achievable using a top-down function-oriented strategy that rethinks network abstractions with the efficiency of verification in mind.” (section 1, pp. 257–258)

The abstraction keeps control and data plane intent together and requires each function to be a separate logical flow table. Rules have match, priority, counter, timer, action, and an active bit. In addition to ordinary forwarding and dropping, execution can add or delete rules. The appendix’s simple stateful firewall uses an I-to-E rule that adds the reverse-direction rule and removes the initiating rule; subsequent E-to-I traffic can match the newly active rule (table 13, p. 271). The appendix gives concrete rule tables for counters, port knocking, stateful firewalls, FTP monitoring, and DNS-amplification mitigation, and describes application chaining (section 8, pp. 270–272).

technique 1: one-big-switch with dynamic rules

What it is. The programmer writes each network function as a table in one conceptual switch. A rule can execute if it is active, its counter conditions are satisfied, and it is the highest-priority applicable rule for at least one matching packet. Its action may change the active-rule set (sections 2 and 3.3.1, pp. 258–259, 263). This turns distributed forwarding intent into a single stateful program while preserving function boundaries.

When to use it. Inference: use it when the property concerns function-level behavior—such as a request eventually enabling a response, a malicious source eventually being blocked, or a port becoming available after a knock—and low-level path engineering is outside the target. The paper explicitly says its abstraction is not suited to questions such as congestion or multipath load balancing (section 6, p. 268).

How to apply it. (1) Make one table per function (section 2, p. 259). (2) Give each rule an initial active value, priority, match predicate, and action (section 2, pp. 258–259; appendix tables 6–17, pp. 271–272). (3) Represent state changes with add(R) and delete(R) actions (section 2, p. 259). (4) State desired behavior in LTL over packet/action propositions. The paper lists leads-to as G(P ! FS), universality as GP, absence as G¬P, eventually as FP, and precedence as FP ! (¬PU(S ^ ¬P)) (table 3, p. 267). For the simple stateful firewall, initialize an I-to-E rule and a lower-priority drop rule; when I sends to E, add the E-to-I rule and delete the initiating rule, so later E-to-I traffic is sent (table 13, p. 271).

Verus form. Inference: represent the table state as a Rust struct containing rule-state booleans and counters, with executable functions for rule dispatch and state updates. Inference: specify the transition relation and LTL-like obligations as spec fn predicates and prove per-step lemmas plus a loop or transition-system invariant; Verus does not provide the paper’s LTL model checker as a direct construct. Inference: an add or delete operation becomes a Rust mutation whose postcondition states exactly which rule bits changed, while packet matching and priority selection remain executable code. Inference: preserve functional decomposition with one Rust module or verified state-machine component per logical table.

Evidence. The appendix demonstrates that the abstraction expresses the 15 functions listed in table 1, including simple counter, port knocking, stateful firewall, phishing/spam detection, FTP monitor, heavy-hitter detection, sampling by flow size, DNS amplification mitigation, and UDP flood mitigation (section 8, pp. 270–272). The paper reports that a simple stateful firewall policy takes three lines in the abstraction, while its generated P4 contains 133 lines including 100 lines of boilerplate, plus roughly 50 lines of controller code (section 4.2, p. 265).

Limits and assumptions. Inference: this technique assumes a faithful compiler and run-time implementation of rule updates, packet ordering, and controller interaction. The paper’s verifier does not verify the generated P4 and omits memory safety and crash freedom; it therefore requires separate compiler verification, P4 debugging, and testing (section 6, p. 268). Inference: a Verus proof of the Rust model would not prove an unverified P4 target unless the compilation and target semantics were also connected by a proved refinement theorem.

technique 2: packet-less Boolean transition system

What it is. Replace packet and header enumeration with one Boolean variable per rule. Ri is true when rule Ri is active. A state is a valuation of these variables; a transition s ->Ri s' represents execution of a rule that adds or deletes rules, with added rules true and deleted rules false in s'. The paper states, “We initially model the network as a transition system TS with a single Boolean variable corresponding to each rule.” (section 3.3, p. 261)

When to use it. Inference: use it to model dynamic state changes whose externally visible behavior depends on which rules are installed, especially for exhaustive model checking of liveness. It removes packet-internal hops and other details invisible to users, reducing state size. It is unsuitable when those omitted details are themselves the property, such as low-level memory safety or exact path engineering.

How to apply it. (1) Create an active bit for every rule and initialize it from the one-big-switch table (section 3.3, pp. 261–262). (2) Define an add/delete transition when its rule is active and highest priority for at least one matching packet (section 3.3, p. 262). (3) For every add/delete action, update only the corresponding destination bits; leave unrelated bits unchanged (section 3.3, p. 262). (4) Label each state with packet/action propositions by recursively evaluating rules in descending priority (section 3.3.2, pp. 263–264). (5) Feed the Boolean transition system and the LTL formula to NuSMV through the specification interface (section 4.1, p. 264).

The recursive labeling function is K((h,a),W,W'). For an empty packet set, it returns true; for a nonempty packet set with no rules left, it returns false. For an overlapping highest-priority rule whose action includes the requested actions, it accepts either applicability with recursion on the unmatched packets, or inapplicability with recursion on all packets. If the overlapping rule lacks the requested actions, it requires inapplicability and recursion on all packets. A nonoverlapping rule is skipped (section 3.3.2, pp. 263–264). The paper expands the IDPS proposition ((src=I,dst=E), send()) into a Boolean formula over active and counter-condition bits (section 3.3.2, p. 264).

Verus form. Inference: encode each Boolean state as fields of a Rust state-machine struct and define a spec fn for can_execute and a pure specification function for the recursive priority result. Inference: prove that each executable transition preserves a state invariant and that the implementation agrees with the specification function; use ensures on executable functions rather than on spec fns. Inference: model-checking’s exhaustive LTL search must be replaced by explicit induction or a bounded-state proof strategy in Verus, unless an external checker is linked through a separately trusted interface. Inference: represent packet sets and match predicates abstractly when concrete packet enumeration is unnecessary, but state the abstraction relation as a proved lemma.

Evidence. For the UDP flood mitigation function, the paper compares packet-less and packet-based transition systems over 20 repeated trials per experiment, each with a 1,000-second time budget (section 4.2, p. 265). At 100 hosts, leads-to verification takes 85 seconds for packet-less versus 667 seconds for packet-based, a reported 7.8× speedup; these are verification-time measurements for the UDP flood function, with 20 trials per experiment and median times plotted in figure 5 (p. 266). Within the same 1,000-second budget, eventually verification reaches 105 hosts packet-less versus 30 hosts packet-based, a 3.5× larger network (p. 266). For a stateful firewall in a 30-host network, the paper reports 3.3× faster eventually and 4.9× faster universality checks (p. 266).

Limits and assumptions. The paper says liveness verification is computationally expensive and sometimes undecidable, and that absolute times remain high for large networks (sections 1 and 6, pp. 257–258, 268). Its transition-state variables omit packets and packet hops; packet match sets still enter the construction of property formulas (sections 1 and 3.3.2, pp. 258, 263–264). Inference: a Boolean proof can establish the modeled transition system while missing an implementation bug in packet parsing, queueing, or rule installation unless those layers are separately related to the model.

technique 3: predicate abstraction for counters

What it is. Replace integer counter values with Boolean predicates for intervals delimited by rule thresholds. For a counter cj, collect all lower and upper bounds into an ordered point list Pj; each subinterval becomes a refined state. A rule’s condition bit R'i is true exactly in subintervals where its interval contains the subinterval. The paper states, “This technique reduces the size of the model by tracking only predicates on data and eliminating invisible data variables.” (section 3.3.1, p. 262)

When to use it. Inference: use it when forwarding behavior changes only when a counter crosses thresholds, not at every integer value. The paper describes threshold-based flood detectors, rate limiters, heavy-hitter detectors, and phishing counters (tables 2, 4, 5, and 12, pp. 266, 268, 271). Its transition construction uses the premise that the counter increases monotonically (section 3.3.1, p. 263). Inference: decrementing or resetting counters need additional transition semantics before this construction can be reused unchanged.

How to apply it. (1) For every rule using li ≤ cj < ui, collect li and ui and sort them into Pj (section 3.3.1, p. 262). (2) Partition the counter domain into the |Pj|−1 subintervals (section 3.3.1, p. 262). (3) Add a condition bit R'i per rule, fixed to true for rules without counters; otherwise set it to ((li ≤ lj,k) ∧ (uj,k ≤ ui)) in subinterval Pj,k. Initialize counter-condition bits using the first subinterval (section 3.3.1, p. 262). (4) Add a transition from subinterval k to k+1 when a rule depending on that counter can execute, representing possible progress to the next threshold (section 3.3.1, p. 263). (5) Retain an add/delete transition in each refined substate where its rule can execute, and repeat the refinement sequentially for multiple counters (section 3.3.1, p. 263). The monitor example uses P0=[0,v1,v2,m], yielding three counter subintervals and a refined graph (figures 3–4, pp. 262–263).

Verus form. Inference: represent each threshold interval as an enum or bounded integer rank and prove that the rank corresponds to the concrete counter range. Inference: use an invariant linking the concrete counter to its abstract interval and prove that increment or decrement moves only to an adjacent valid rank. Inference: retain the concrete counter in executable code and use interval ranks in the proof; a rank alone does not record progress within an interval.

Evidence. The paper reports a UDP flood function with a per-source counter and thresholded drop rule (table 2, p. 266), and a six-rule rate limiter (table 5, p. 268). In the rate-limiter experiment, the packet-less model verifies liveness and safety for networks six times larger than the packet-based model and is at least two orders of magnitude faster even at small scales (section 4.2, p. 266). For eventually verification, the reported network sizes within 1,000 seconds are 90 hosts versus 15 hosts; the experiments use 20 trials each (pp. 265–266).

Limits and assumptions. Threshold abstraction loses differences between counter values inside one interval. Inference: it is sound only when the rule predicates and specified properties cannot distinguish those values, or when the proof includes that indistinguishability relation. The appendix says the super-spreader counter is decremented on FIN (section 8, p. 270), and table 16 resets sampling counters to zero (p. 272). Inference: the monotone-counter transition explanation does not by itself establish how those operations are modeled.

technique 4: priority-aware Boolean labeling of properties

What it is. Translate a packet/action atom (h,a) into a Boolean formula over ordered rule bits. The recursive K function handles overlapping matches and priorities without enumerating packets. This connects a packet-defined property to a packet-less state model (section 3.3.2, pp. 263–264).

When to use it. Inference: use it when several active rules match the same packet but only the highest-priority applicable rule determines the action. It is necessary for correct state labels in the presence of rule overlap, counters, and rules that become inactive through deletion.

How to apply it. (1) Sort R0…Rn by non-increasing priority and keep matching-condition bits R'0…R'n (section 3.3.2, p. 263). (2) Set the base cases: empty h gives true; nonempty h and no remaining rules gives false. (3) If the highest rule overlaps h and includes the requested actions, accept either applicability with recursion on unmatched packets, or inapplicability with recursion on all of h. (4) If it overlaps but lacks the requested actions, require inapplicability and recurse on all of h. (5) If it does not overlap, recurse unchanged. (6) Use the resulting formula as the labeling function for LTL model checking (section 3.3.2, pp. 263–264).

Verus form. Inference: implement the same priority recursion as a pure spec fn, prove it terminates on a finite rule slice, and prove an executable dispatcher returns the action selected by the specification. Inference: use sequence or finite-map specifications for ordered rules and explicit lemmas for disjointness and priority; do not treat the recursive formula as an executable runtime proof call.

Evidence. The paper gives the expanded IDPS formula and explains that it is true in the initial state, where R0=false and R4=true, and false in the final state where R0=true and R4=true (section 3.3.2, p. 264). This is a state-labeling example, not an independent performance denominator.

Limits and assumptions. The recursion assumes a finite ordered rule list and known priority order. Inference: if overlapping equal-priority rules have conflicting actions, their ordering needs justification so that the recursive formula agrees with dispatch; the paper does not specify a tie-breaking convention here.

implementation, evidence, and trust boundary

The prototype exposes a one-big-switch programming interface and a property-specification interface, generates the packet-less model and formula, and invokes NuSMV (section 4.1, p. 264). Its P4 compiler maps each logical table to a P4 table, uses metadata for traversal, and uses P4 registers for shared counters (section 4.1, pp. 264–265). Because current P4 data planes do not support add/delete, the compiler clones affected packets to the switch-local control plane, where generated controller code performs the update (section 4.1, pp. 264–265). Across the table-1 applications, controller calls are 0–0.3% of more than 102K packets from a university-datacenter trace containing 1,791 IP addresses; this denominator and trace setting are the paper’s limited-overhead experiment (section 4.2, p. 265).

The paper reports model-checking results, expressiveness examples, compilation time, and controller-call frequency (section 4, pp. 264–267). It does not prove the generated P4 code, hardware behavior, crash recovery, or memory safety. The authors state that their verifier “does not verify the compiled P4 code” and that “the absolute verification times remain high for large-scale networks” (section 6, p. 268). Inference: for agent-written Rust verified with Verus, the main reusable ideas are state-machine decomposition, finite predicate abstraction, and priority-preserving transition invariants; the main product threat is semantic drift between the verified abstract policy and the generated or deployed network implementation. Inference: this paper is relevant to VL’s modeling layer but does not reduce the trusted computing base of Verus, Rust, P4, NuSMV, or switch hardware.

what VL should not redo

The paper already supplies a packet-less Boolean encoding, threshold predicate abstraction, recursive priority labeling, LTL property patterns, a P4 compiler strategy, and a baseline methodology with 20 trials and a 1,000-second limit. Inference: VL should not repeat those as a new abstraction without a distinct Rust/Verus refinement result. Inference: a useful extension would be to prove that a Verus implementation of the abstract transition system refines concrete packet-processing code and to measure proof maintenance under rule-table changes.

techniques for the catalog

• one-big-switch dynamic rules — express stateful network functions as separate logical tables with add/delete rule actions and LTL properties
• packet-less Boolean model — encode active rules as Boolean transition-system state and label states with priority-aware formulas
• counter predicate abstraction — replace threshold-relevant integer counter values with Boolean interval predicates and refined transitions
• priority-aware property labeling — recursively translate packet/action propositions into formulas over ordered active-rule and counter-condition bits
• P4 compilation boundary — map tables, metadata, registers, and controller-assisted add/delete behavior while keeping generated code outside the verifier’s proof Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “For each experiment, we run 20 repeated trials, each trial with a time budget of 1,000 sec., i.e., we stop the verification process when the verification time exceeds 1,000 sec.”): checked all quotations, numbers, section and printed-page references, technique steps, and stated limitations against the complete paper, including references and appendix; corrected quotation wording, page references, the priority-recursion branches and base cases, counter-transition scope, and the P4/controller line-count distinction; replaced the link with the publisher page printed in the paper; marked applicability advice and counter-model conclusions as Inference; did not independently validate Verus proposals, run the prototype, reproduce measurements, or verify generated P4.

Last edited: 2026-10-16