WAVED (WeAk Verification Exploitation Detector)

WAVED is a static-analysis framework for identifying off-path exploitable weak-verification paths in kernel TCP/IP implementations. Given a linked LLVM bitcode module, packet-header definitions, and user-selected risky operations, WAVED produces an HTML report that describes candidate paths and the constraints guarding them.

WAVED was developed for the paper accepted at the 35th USENIX Security Symposium (USENIX Security '26):

• USENIX paper page
• Prepublication paper included in this repository

Overview

WAVED explores paths from protocol-stack packet-processing entries to semantically risky operations, such as shared routing-state updates or packet-delivery points. Its analysis consists of four main components:

1. Protocol-oriented pointer analysis extends SVF with flow, context, and field sensitivity, including byte-offset-aware handling of kernel pointer arithmetic.
2. Byte-granularity taint analysis constructs a Taint Propagation Graph (TPG) and tracks how individual packet bytes propagate through data-flow and arithmetic operations.
3. Direction-sensitive constraint analysis computes branch impacts that distinguish between strong and weak branch strength.
4. Weak-path identification composes constraints along candidate paths and finally reports the weak-verification paths.

WAVED reports candidate weak-verification paths rather than automatically confirmed vulnerabilities. Each report must be inspected in its source-code and protocol context before drawing a security conclusion.

Evaluated Targets

Kernel	IP variants	Evaluated protocols	Included configurations
Linux 5.15	IPv4 and IPv6	ICMP/ICMPv6, TCP, UDP, SCTP, DCCP	config/file_range/linux_5.15_* and config/risky_operation/linux_5.15_*
Linux 6.8	IPv4 and IPv6	ICMP/ICMPv6, TCP, UDP, SCTP, DCCP	config/file_range/linux_6.8_* and config/risky_operation/linux_6.8_*
FreeBSD 14.1	IPv4 and IPv6	ICMP/ICMPv6, TCP, UDP, SCTP	config/file_range/freebsd_14.1_* and config/risky_operation/freebsd_14.1_*

The repository provides configuration files for these evaluated targets. Applying WAVED to another kernel version or protocol requires compatible bitcode, updated configuration files, and independent validation.

Repository Layout

WAVED/
|-- config/
|   |-- file_range/       # Kernel source files included in each bitcode module
|   |-- header_def/       # Packet-header definitions for Linux and FreeBSD
|   `-- risky_operation/  # Functions or instructions treated as risky operations
|-- include/              # WAVED C++ headers
|-- src/                  # Main executable and analysis implementations
|-- tools/
|   |-- BCBuilder/        # Linux kernel bitcode-generation helper
|   |-- SVF/              # Modified SVF used by WAVED
|   `-- UnionToStruct/    # Clang plugin for union-to-structure transformation
|-- build.sh              # Builds the bundled analysis stack and WAVED
`-- WAVED_Security_26.pdf # Prepublication paper

System Requirements

The commands below assume a Debian- or Ubuntu-based Linux environment. WAVED requires:

• CMake 3.23 or later;
• a C++17-capable compiler and standard build tools;
• Python 3 for the Linux bitcode builder;
• network access during the initial build; and
• substantial memory, CPU time, and disk space for whole-stack analysis.

A baseline package set is:

sudo apt update
sudo apt install -y \
    bc binutils bison build-essential cmake curl dwarves flex git \
    libelf-dev libncurses-dev libpcre2-dev libssl-dev libtinfo6 \
    libzstd-dev openssl perl-base pkg-config python3 unzip xz-utils \
    zip zlib1g-dev

Confirm that the installed CMake satisfies the repository requirement:

cmake --version

The exact dependencies needed to compile a kernel vary with its version and configuration. Consult the Linux kernel build documentation if the kernel preparation stage reports a missing tool or library.

Whole-stack analysis is resource intensive. The paper's evaluation used a server with an Intel Xeon Gold 5418Y processor and 500 GB of RAM. This describes the evaluation environment; it is not a measured minimum hardware requirement.

Build WAVED

Run the top-level build script from the repository root:

./build.sh

The script:

• downloads and builds LLVM 14.0.6 and Z3 4.8.8 under tools/SVF/ when they are not already available;
• rebuilds the bundled, modified SVF implementation;
• recreates the top-level build/ directory; and
• writes the WAVED executable to build/bin/WAVED.

These dependencies are kept inside the repository and are not installed system-wide. The first build can take considerable time because LLVM and Z3 may be built from source.

After the build completes, inspect the available command-line options with:

./build/bin/WAVED --help

Prepare Kernel Bitcode

WAVED consumes one linked LLVM bitcode module containing the target protocol-stack implementation.

Linux

The repository includes tools/BCBuilder/build-linux.py to prepare Linux bitcode. The following example builds the configured Linux 6.8 IPv4 input:

mkdir -p /path/to/kernels
cd /path/to/kernels
git clone --branch v6.8 --depth 1 \
    https://github.com/torvalds/linux.git linux-6.8

cd /path/to/WAVED
python3 tools/BCBuilder/build-linux.py \
    -k /path/to/kernels/linux-6.8 \
    -i config/file_range/linux_6.8_ipv4.txt \
    -o bcfiles/linux-6.8-ipv4

The final linked module is written to:

bcfiles/linux-6.8-ipv4/all-linked.bc

The helper copies the supplied kernel source tree to kernel_tmp/<kernel-name> before configuring it, so the original source tree is not built in place. It uses allyesconfig, compiles the selected source files with the bundled LLVM toolchain, applies the UnionToStruct plugin, and links the resulting modules.

Warning: If the path passed to -o already exists, the helper deletes and recreates that directory. Use a dedicated output path and do not point -o at a directory containing unrelated files.

To prepare an IPv6 input, use the corresponding file-range configuration, for example config/file_range/linux_6.8_ipv6.txt.

FreeBSD

The repository does not include an automated FreeBSD bitcode builder. Prepare a single LLVM 14-compatible linked bitcode module with debug information on a suitable FreeBSD build environment, using the relevant file list under config/file_range/. The resulting module can then be analyzed by WAVED with --freebsd.

Configure the Analysis

WAVED uses two configuration inputs in addition to the bitcode module.

Packet-Header Definitions

The YAML files in config/header_def/ describe packet-header structures and how their fields enter the analysis:

• struct_name: packet-header structure name in the kernel source;
• is_outer_header: whether the structure represents the outer or encapsulated header;
• ignored_fields: fields excluded from constraint evaluation, such as checksums or header lengths;
• critical_fields: fields whose strong verification is treated as impractical for an off-path attacker to bypass;
• activate_funcs: functions that activate tracking for the header;
• type_cast_defs_in_funcs: functions in which type casts expose the header; and
• function_call_defs: helper functions that return or expose the header.

The supplied Linux and FreeBSD definitions cover the evaluated targets. Update them only when adapting WAVED to a different implementation or protocol.

Risky Operations

Files in config/risky_operation/ identify analysis destinations. Each non-comment line uses one of these forms:

Func: <function-name>
Inst: <source-file.c-or-h>:<line-number>

For example, the included Linux configurations use entries such as:

Func: update_or_create_fnhe

Blank lines are ignored, and lines beginning with # are comments. Function names and instruction locations must exist in the input bitcode module.

Run the Analysis

Command-Line Interface

Argument	Requirement	Description
<input-bitcode>	Required	Positional path to the linked LLVM bitcode module
--result-file=<path>	Optional	HTML output path; defaults to output.html
--risky-point-file=<path>	Required	Risky-operation configuration
--header-def-file=<path>	Required	Packet-header YAML configuration
--byte-threshold=<n>	Optional	Maximum number of strongly constrained bytes for weak-path reporting; defaults to 8
--linux	Exactly one kernel flag	Analyze a Linux module
--freebsd	Exactly one kernel flag	Analyze a FreeBSD module
--is-ipv6	Optional flag	Enable IPv6 analysis; omitted for IPv4

Example: Linux 6.8 IPv4

mkdir -p results

./build/bin/WAVED \
    --result-file=results/linux-6.8-ipv4.html \
    --risky-point-file=config/risky_operation/linux_6.8_ipv4.txt \
    --header-def-file=config/header_def/header_def_linux.yaml \
    --linux \
    bcfiles/linux-6.8-ipv4/all-linked.bc

For IPv6, use the matching IPv6 bitcode and risky-operation configuration and add --is-ipv6.

During preprocessing, WAVED also writes a transformed LLVM IR file named <input-bitcode>.waved.ll next to the input module.

Interpret the Results

The output HTML groups candidate paths by risky operation. For each candidate, WAVED reports:

• the functions traversed along the path;
• relevant control-dependent branches and their taken outcomes;
• resolved constraints at branches marked [Critical]; and
• the accumulated byte constraints for the complete path.

The underlying direction-sensitive taint tuple is represented as <L, G, E>. The HTML report presents four views:

• Relevant bytes: all bytes present in L, G, or E;
• Double-sided: bytes in E, corresponding to equality or bounded/range constraints and treated as strongly constrained;
• Left-sided: bytes in L, associated with less-than-style one-sided constraints; and
• Right-sided: bytes in G, associated with greater-than-style one-sided constraints.

These constraints explain why a path passed strength filtering; they do not by themselves establish exploitability. Validate path feasibility, protocol state, attacker capabilities, and the semantic impact of the risky operation manually.

Acknowledgments

WAVED is implemented using LLVM and a modified version of the SVF static value-flow analysis framework. The bundled SVF source and its third-party licensing information are under tools/SVF/ and tools/SVF/LICENSE.TXT.