Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

WAVED: Principled Identification of Off-Path Exploitable Weak Verifications within the TCP/IP Protocol Suite

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

problem and result

The paper studies off-path attacks that exploit a packet-processing path whose checks are too weak before a risky operation such as modifying shared routing or path-MTU state. Its central operational definition measures the attacker’s required knowledge by the input bytes that are strongly constrained on a path. A one-sided or unbounded comparison leaves many satisfying packets; a bounded equality or range check constrains a small space. The tool, WAVED (WeAk Verification Exploitation Detector), combines pointer analysis, byte-level taint, direction-sensitive branch analysis, and path search.

The paper states its key insight: “Our key insight is that the strength of a path constraint is proportional to the knowledge an off-path attacker must possess to satisfy it.” (section 1, p. 3640). It reports 19 weak-verification vulnerabilities, 14 previously unknown, across Linux 5.15, Linux 6.8, and FreeBSD 14.1 (16 in Linux, 3 in FreeBSD; section 6.2, p. 3649). The introduction states: “We implement WAVED based on the framework of LLVM [26] and the SVF (Static Value-Flow) analysis tool [39].” (section 1, p. 3640). Inference: for agent-written verified Rust, the transferable lesson is to make the security-relevant precondition explicit, then quantify which attacker-controlled bytes the precondition actually fixes rather than treating every data dependency as equally protective.

technique 1: protocol-oriented pointer analysis

What it is. WAVED extends SVF’s flow-sensitive whole-program analysis with context-sensitive call contexts and byte-offset field handling. The paper motivates it by kernel pointer arithmetic such as container_of() and by SVF’s lack of context sensitivity and its “coarse-grained flattened field indices”, which cause imprecision for casts and negative-offset GEPs (section 3.3, p. 3642; section 4.1, p. 3644).

How to do it, as described by the paper:

  1. Compile the protocol implementation to LLVM bitcode and run Andersen-style points-to analysis (section 3.4, p. 3643; section 4.1, p. 3644).
  2. Build a sparse value-flow graph from those points-to results and propagate points-to information (section 4.1, p. 3644).
  3. Collect possible call contexts by walking the context-insensitive call graph from the entry; each context contains at most three call sites (section 4.1, p. 3644).
  4. Duplicate each SVFG node for every context, then copy intra-context edges and add inter-context edges for direct calls, resolving indirect calls later via the on-the-fly context-sensitive call graph; only edges that obey context composition rules are kept (section 4.1, p. 3644; Algorithm 1, Appendix A, p. 3658).
  5. Replace field-index GEP arithmetic with byte-offset arithmetic: translate a field index to a byte offset, add the offset, and map back to a field index while retaining a per-type bidirectional map (section 4.1, p. 3644).

Verus form. Inference: Verus ordinarily reasons about typed Rust references and permissions, so this LLVM pointer graph does not carry over directly. The analogous review step is to preserve distinct ownership/borrow contexts and prove that byte offsets used for packet parsing stay within the intended slice. If raw pointers or FFI are used, isolate them behind a small unsafe boundary with an external_body only for code that is genuinely trusted, and prove the safe wrapper’s requires/ensures; do not treat external_body as proof of the wrapped implementation.

Evidence and limits. The implementation is built on SVF 3.0 (commit a68b293), modifies SVF’s GEP interfaces, extends the ExtAPI module for external memory functions, and uses a Clang plugin to turn C unions into structs except for network packet headers and system header files; SVF patch plus plugin is about 4.9k lines of C++ (section 5, p. 3648). The paper calls the SVF base analysis “a widely recognized, sound MOP solution” (section 4.1, p. 3644). Inference: precision still depends on how well the LLVM/kernel constructs are modeled.

technique 2: byte-granularity MOP taint propagation

What it is. Object-level taint only says that a branch depends on an input object. WAVED tracks which packet bytes flow to which value bytes. It builds a Taint Propagation Graph (TPG), with an 8-by-8 bitmap on each edge under LP64; matrix composition models byte-to-byte propagation (section 4.2, pp. 3644–3645).

How to do it:

  1. Construct TPG edges from explicit IR data dependencies of all program instructions and sparse value-flow edges for address-taken variables, using the pointer results; keep statements in different contexts as different nodes (section 4.2, p. 3644; section 5, p. 3648).
  2. Assign one of seven propagation maps to each edge: LowToHigh, Copy, LogicOff, ArithOff, And(const), Or(const), or Full (Table 1, p. 3645). The map records whether source byte i can taint destination byte j.
  3. Compose edge maps by Boolean matrix multiplication (equation (1), section 4.2, p. 3644); pack each 8-by-8 map into a 64-bit integer so one multiplication costs Θ(nÂČ) with bitwise masks, and memoize products (section 4.2, p. 3645; Algorithm 2, Appendix A, p. 3658).
  4. Run CFL-reachability over the TPG to add call-return-matched summary edges, avoiding false flows caused by bounded call-context depth (section 4.2, p. 3645).
  5. For each packet-header byte, traverse the graph and aggregate all reachable original offsets into Taint(n), yielding a meet-over-all-paths result (section 4.2, p. 3645).

Verus form. Inference: a Rust/Verus implementation can model each parsed field as a sequence index or bit-vector and state which output bytes depend on which input bytes in a spec fn; proofs can use forall/exists quantification and sequence slicing. Verus does not provide WAVED’s static LLVM taint engine, so this is a design-time analysis around the verified parser, not a replacement for the parser’s functional proof.

Evidence and limits. The authors reject path-sensitive taint as too expensive and choose MOP as a scalable compromise (section 4.2, p. 3644). The taint component is roughly 4.1k lines of C++, with CFL-reachability restricted to TPG nodes on an object-granularity forward slice from taint sources (section 5, pp. 3648–3649). Limited context depth still creates possible false positives, motivating CFL summaries and later header activation.

technique 3: direction-sensitive branch impact and implicit control flow

What it is. Direction-sensitive taint distinguishes bytes constrained by less-than, greater-than, and equality/range outcomes. A taint tuple is 〈L,G,E〉; L and G record less-than and greater-than outcomes, while E records equality or bounded outcomes, “which are considered as strong constraints”. If the same byte occurs in both L and G, equation (2) moves it into E (Definition 1 and equation (2), section 4.3, pp. 3645–3646).

How to do it:

  1. Map each comparison outcome to a taint tuple: a < b gives 〈Taint(a), Taint(b), Ï†ă€‰, a > b gives 〈Taint(b), Taint(a), Ï†ă€‰, a = b puts both operands’ bytes in E, and a ≠ b gives ă€ˆÏ†, φ, Ï†ă€‰ (Table 2, p. 3645).
  2. Represent each conditional branch as a pair 〈B1,B0〉 for the True and False outcomes, where a branch impact is a disjunction of taint tuples; combine tuples by conjunction and branch impacts by disjunction and conjunction (Definition 1, equations (3)–(5), section 4.3, pp. 3645–3646).
  3. Resolve branch impact backward over TPG instructions (Cmp, binary/unary operations, Phi, Select, Cast, and Call) using Table 3’s rules; other instructions conservatively get double-sided constraints on both B1 and B0 (section 4.3, p. 3646; Table 3, p. 3648).
  4. For helper functions whose return value hides checks, associate each return value with impacts for nonzero and zero/null. For Phi, carry predecessor path constraints into the returned value (section 4.3, pp. 3646–3647).
  5. Traverse basic blocks breadth-first from the function entry, ignore loop edges, and maintain a function summary of path transitions and impacts. Keep a stack of active branch impacts, pop a branch at its immediate post-dominator, and hash the stack to deduplicate equivalent path states reaching the same block (section 4.3, p. 3647; Figure 4, p. 3647; Algorithm 3, Appendix A, p. 3658).

The paper’s Linux example is tcp_sequence(), where internal sequence-window checks return constants. The authors explain: “Crucially, since all exit paths return untainted constant integers, standard taint analysis fails to track the implicit dependency between the input sequence and the validation result, inevitably resulting in false negatives.” (section 4.3, p. 3646). Their backward resolution aggregates the one-sided after()/before() comparisons and distinguishes strong in-window checks from weak out-of-window checks (Figure 5, section 4.3, p. 3647).

Verus form. Inference: express helper validity as a predicate over packet bytes and return a Boolean or enum with an ensures clause connecting the result to that predicate. Callers should require the predicate corresponding to the accepted branch; a proof function can establish that a range check implies the predicate. Verus’s old expression is used in postconditions when pre-state values matter; the paper’s branch-impact tuples are an analysis abstraction, not Verus syntax.

technique 4: weak-path identification and filtering

WAVED builds a context-sensitive Summary Graph whose edges are summarized intra-function paths. A depth-first search starts at the packet receiving entry and accumulates branch impacts until a labeled risky operation. It applies three reductions: header activation (track a protocol’s fields only after execution enters that protocol’s context), constraint deduplication (exclude branch outcomes that add no constraint from the sub-path hash), and strength filtering (flag the path if its weakest constraint, the one with minimum |E|, falls below a threshold) (section 4.4, pp. 3647–3648; Algorithm 4, Appendix A, p. 3658). The evaluation labels two patterns as risky operations: FNHE/routing cache poisoning (update_or_create_fnhe(), rt6_insert_exception(), and FreeBSD’s rib_add_redirect() plus tcp_hc_updatemtu()) and packet injection (protocol data-receiving points) (section 6.1, p. 3649).

The reporting threshold is eight bytes, “calibrated to the most rigorous known weak verification case (4 bytes for src/dst ports and 4 bytes for the target gateway address) [20]” (section 6.1, p. 3649). Paths with strong constraints on highly secure fields (e.g., TCP/DCCP seq/ack, SCTP vtag) are also excluded, as such fields are “usually impossible for an off-path attacker to eavesdrop or brute-force” (section 4.4, p. 3648). Inference: a Verus checker for a protocol handler can use the same workflow by identifying state-mutating postconditions, listing attacker-controlled inputs in each requires, and rejecting a path whose only proof obligations are public or one-sided values. The threshold and “secret” list must be chosen for the deployment; Verus itself does not infer exploitability.

evidence, measurements, and failures

The evaluation covers both IPv4 and IPv6 in three kernels: ICMP, TCP, UDP, SCTP and DCCP for Linux, and the same without DCCP for FreeBSD (section 6, p. 3649). The paper reports 43 unique weakly constrained paths; Table 7 lists 12 false positives among them, and “Most FPs (8 of 12) arise from redundant branches incorrectly implemented in Linux”; the remaining 4 come from repetitive type/state checks (section 6.4, p. 3651). Running time is 22 and 30 minutes for Linux 5.15 IPv4/IPv6, 11 and 21 minutes for Linux 6.8, and 42 and 125 minutes for FreeBSD 14.1 (section 6.2, p. 3649). Constraint deduplication reduces path counts by 95% for Linux 5.15 IPv4/IPv6, 95% for Linux 6.8 IPv4, 96% for Linux 6.8 IPv6, 71% for FreeBSD 14.1 IPv4, and 61% for FreeBSD 14.1 IPv6 (section 6.4, p. 3651; Table 8, p. 3652). Strength filtering gives average reductions of 52% for Linux-IPv4, 55% for Linux-IPv6, 58% for FreeBSD-IPv4, and 48% for FreeBSD-IPv6 (section 6.4, p. 3651). Inference: these are reductions in path counts, not vulnerability rates; the paper does not state exactly what the averages are taken over.

The two packet-injection findings (#18, #19) are Linux DCCP paths where a socket in DCCP_REQUESTING does not verify the sequence number of incoming RESET/CLOSEREQ/CLOSE packets; per address family WAVED reports 7 paths, consolidated into 4 unique reports with 3 true positives and 1 false positive (section 6.3.1, p. 3651; section 7.2, p. 3653). Cache-poisoning cases include seven zero-checked cases and UDP-based cases where, since the server’s port is typically known, an attacker needs at most 2^16 packets even when the socket is connected (section 7.1, p. 3652). The paper says: “WAVED relies on static taint analysis and cannot capture the actual runtime state at each program point” (section 8, p. 3653). It also tests only two known semantically risky patterns and does not support tunneling protocols such as GRE, IPSec, or VPN (section 8, pp. 3653–3654). Inference: these are substantial threats to agent-written verified Rust when specifications omit cross-layer state or permit public packets to mutate global state; a local functional proof cannot establish that an attacker cannot reach the state transition unless that reachability and attacker model are specified.

What is proved and trusted. The paper says the 14 new vulnerabilities were manually validated “in a controlled local environment” (section 6.2, p. 3649) and responsibly disclosed to the Linux and FreeBSD security teams (abstract, p. 3639; section 8, p. 3654). Inference: WAVED’s outputs are static reports, not machine-checked proofs; trusted components include LLVM/SVF, the source-to-bitcode build, the risky-operation labels, the strength threshold, and human interpretation of reports. Inference: VL should already have ordinary precondition/postcondition proofs for local Rust behavior; it should add adversarial reachability and cross-component state specifications rather than redo this paper’s C/LLVM implementation.

techniques for the catalog

  • context-sensitive byte-offset pointer analysis — duplicate value-flow nodes by bounded call context and resolve GEP using concrete byte offsets
  • byte-granularity MOP taint — compose 8-by-8 byte-flow maps over a TPG with CFL call-return summaries
  • direction-sensitive branch impact — represent one-sided versus bounded constraints as taint tuples and recover implicit helper-function checks
  • weak-path identification — traverse summarized paths to risky operations, activate protocol fields, deduplicate equivalent constraints, and filter by strong-byte count Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Loop edges are ignored since they always incur stronger constraints, thus we can process basic blocks in topological order.”): what I checked: every quotation, number, section and page reference, and technique step against the paper text (pp. 3639–3658, incl. Appendix A); what I changed: link to the USENIX presentation page given in the paper text, fixed quote wording and the misattributed first-contribution and abstract quotes, corrected page/section refs (e.g. threshold and risky-operation labels are section 6.1, algorithms are in Appendix A p. 3658), fixed the DCCP consolidation (7 paths into 4 unique reports), the false-positive attribution, the risky-operation list, and added FreeBSD running times; marked my own conclusions as Inference; what I did not check: figures and tables against the PDF rendering beyond the text extraction, the Verus-specific inferences, and the released artifact.

Last edited: