SPAR: Generating Precise Format Specification for Network Protocols Through Adversarial LLM Interactions

SPAR automatically generates verified protocol specifications from natural-language descriptions. It leverages Large Language Models (LLMs) and adversarial refinement to verify and produce precise specifications.

Built on EverParse (verifier), Z3 (SMT solver), and the autogen framework (LLM orchestration).

Paper: Generating Precise Format Specification for Network Protocols Through Adversarial LLM Interactions. Submitted to USENIX Security 2026.

Artifact Claim: The tool can automatically produce a precise protocol format specification from an RFC. This artifact demonstrates the BFD protocol generation and verification. Evaluators can run main.py on BFD and then use eval_3d.py to check the structural match against the ground truth. Due to the inconsistencies introduced by LLM providers and LLM models themselves, the artifact focuses on demonstrating the end-to-end workflow and providing a framework for evaluation, rather than guaranteeing exact numeric reproduction of paper results.

Open Science

The artifact includes all components described in the paper's Open Science section:

Component	Location	Description
Format & parser generation	src/agent/, src/doc_graph/, main.py	LLM-driven generation of initial 3D format specifications and Python parsers from RFC documents, borrowed from ParCleanse
Adversarial refinement loop	src/refine/, src/encode/, src/fsm/, src/hybrid_fuzz/	Automated test-case generation, and adversarial refinement
Three optimizations	main.py (flags --disable-opt-i/ii/iii)	Path-cover optimization, linear constraint negation, and slicing-based RFC section tracing
RFC documents	data/RFC/	8 protocol RFC texts used as input to the pipeline
Ground-truth specifications	data/ground_truths/	15 hand-written reference .3d specifications for evaluation
Pre-computed results	data/packaged_results/	Generated outputs for all 8 RFC-backed protocols
Setup & evaluation scripts	scripts/	setup_everparse.sh for setting up everparse, run_eval.sh for API-free offline evaluation

Repository Structure

SPAR-AE/
├── main.py                 # CLI entry point
├── eval_3d.py              # Metrics evaluator (generated vs. ground truth)
├── pyproject.toml          # Project metadata & dependencies (uv-managed)
├── README.md               # This file
├── LICENSE                 # MIT
├── everparse/              # EverParse library (see Setup §2)
├── scripts/
│   ├── setup_everparse.sh  # Automated EverParse download
│   └── run_eval.sh         # Offline evaluation of all protocols
├── data/
│   ├── RFC/                # Protocol RFC text files (BGPv4, NTP, IGMP, BFD, BABEL, SCTP, DNS, HTTP2)
│   ├── DSL/                # DSL references (3d_syntax_check.txt, python_coding_style.txt)
│   ├── example/            # Example format/parser files per protocol as 3D coding guide
│   ├── ground_truths/      # 15 ground truth .3d specification files, some unused in the evaluation
│   └── packaged_results/   # Pre-computed outputs for offline evaluation (8 protocols)
└── src/
    ├── secret/             # LLM credentials (see Configuration)
    ├── driver/             # Pipeline driver
    ├── doc_graph/          # Document graph construction
    ├── refine/             # Refinement loop (verifier, tester, auto_evaluator)
    ├── parse3d/            # 3D format parser and AST
    ├── encode/             # Test case generation
    ├── fsm/                # Finite state machine extraction
    ├── hybrid_fuzz/        # Concolic fuzzing engine including program slicing
    ├── agent/              # LLM agent wrappers
    ├── ablation/           # Ablation study 1. Others are controlled by flags in main.py
    ├── tool/               # Utility functions and prompts
    ├── log/                # Logging infrastructure
    └── parallel_work/      # Parallel processing support (Unused)

Setup & Prerequisites

1. Python & Dependency Management

This project uses uv for deterministic dependency management.

Install uv (Linux):

curl -LsSf https://astral.sh/uv/install.sh | sh

Alternatively, pip install uv works on any platform. See the official installation guide for other options.

Sync dependencies:

uv sync

This creates a virtual environment and installs all required packages at pinned versions.

2. EverParse Verifier

SPAR uses EverParse to formally verify the syntax of generated protocol specifications.

Automated setup (recommended):

bash scripts/setup_everparse.sh

This downloads the v2025.06.05 release for Linux and extracts it to everparse/.

Manual setup:

1. Download the v2025.06.05 release of EverParse for your platform from GitHub.
2. Extract the archive into the project root.
3. Rename the extracted directory to everparse.

Make sure the internal structure looks like everparse/bin/..., not everparse/everparse-v2025.06.05-linux-x86_64/bin/.... If the archive extracts to a nested subdirectory, move the contents up so that the bin/ directory is directly under everparse/.

After correct extraction, the directory layout is:

SPAR-AE/
├── everparse/
│   └── bin/        <-- EverParse binaries here
├── src/
├── main.py
└── ...

Verification: Confirm EverParse is working by running ./everparse/everparse.sh --version.

Troubleshooting: If the EverParse binary fails with a library error, ensure required system libraries are installed (glibc on Linux).

System Requirements

• OS: Linux x86_64 (tested on Ubuntu 22.04). This artifact only supports Linux.
• Python: 3.12
• RAM: ~4GB (varies by protocol complexity).
• Storage: ~500MB for dependencies and generated artifacts.
• Network: Required for LLM API calls and uv sync. If using pre-computed outputs, network access is not needed for LLM interactions.
• API Access: An API key for a supported LLM provider is required to run the full pipeline. See Configuration below.
• Runtime: BFD example takes 5 to 20 minutes depending on LLM response times and adversarial interaction rounds. Full ablation suite takes around 6 to 8 hours.

Configuration

API credentials are not included in this artifact. Edit src/secret/secret.py and populate config_list and config_list_reasoner with your own LLM provider credentials.

Usage

Once dependencies are installed and credentials configured, run:

uv run python main.py --help

for a complete list of arguments and flags.

Basic Generation

To generate a verified specification for a protocol, provide the protocol name, its RFC document, and a data directory containing the DSL reference files and examples. For example:

uv run python main.py \
  --protocol-name BFD \
  --rfc-path data/RFC/BFD.txt \
  --data-directory data/

The pipeline builds a document graph from the RFC, generates an initial format and parser via the LLM, then enters a refinement loop: the verifier tests the parser against generated test cases, and counterexamples drive the LLM to fix discovered bugs until no failures remain. Generated artifacts (format, parser, and document graph) are written under <data-directory>/packaged_results/.

Optimization Flags

Three optimizations are enabled by default. Each can be turned off individually:

Flag	Effect
--disable-opt-i	Disable path-cover optimization (test all paths exhaustively)
--disable-opt-ii	Disable linear constraint negation (explore all constraint combinations)
--disable-opt-iii	Disable slicing-based RFC section lookup (fall back to FSM-diff based lookup)

Ablation Studies

Flag	Ablation	Description
--run-wo-rfc	Ablation 1	Generate format and parser without the RFC text, using only the protocol name and DSL syntax reference
--disable-opt-i	Ablation 2	Run with Optimization I disabled (full path enumeration instead of path cover)
--disable-opt-ii	Ablation 3	Run with Optimization II disabled (exhaustive constraint-negation exploration)
--disable-opt-iii	Ablation 4	Run with Optimization III disabled (FSM-diff fallback instead of slicing-guided)

Ablation 1 is a standalone run (--run-wo-rfc skips the normal refinement pipeline entirely). Ablations 2–4 are the optimization flags above, reused as ablation conditions to measure each optimization's contribution.

Evaluating Generated Specifications

eval_3d.py measures structural similarity and constraint equivalence between a generated specification and the ground truth:

uv run python eval_3d.py --ground-truth path/to/reference.3d --generated path/to/output.3d

It reports the overall match score, strict pass/fail, and a per-definition breakdown of type and constraint-level alignment for every field. The automated evaluator is conservative and may report false negatives for structurally different but semantically equivalent representations (e.g., inline structs vs. named struct references). Human auditing is recommended to verify the nature of reported mismatches.

Quick-Start (No API Keys)

Evaluate pre-computed SPAR results for all 8 protocols against their ground truth specifications. No API keys or network access required. Ensure you have run uv sync (see Setup & Prerequisites) beforehand.

bash scripts/run_eval.sh

Each protocol prints detailed results. Per-protocol output looks like:

═══════════════════════════════════════
  BFD
  Ground truth: data/ground_truths/BFD.3d
  Generated:    data/packaged_results/BFD_3c74bfa1/BFD_CONTROL.3d
═══════════════════════════════════════
Ground truth:   BFDControlPacket
Generated:      BFDControl
Overall score:  0.849
Strict pass:    False
Definitions:    7 (5 full, 1 partial)
...

Scores being lower than expected and strict: False are primarily due to the evaluator's conservative comparison logic (see Evaluating Generated Specifications above). Generated specifications may still be semantically correct — review the per-definition breakdown for each protocol to confirm. Common false negatives include: inline struct definitions vs. named casetype references, and field decomposition into sub-structs vs. flat inlining.

Full Generation (Requires API Keys)

To run the full pipeline from scratch (BFD example):

# 1. Edit src/secret/secret.py with your API credentials
# 2. Generate the specification and parser, then refine via adversarial testing:
uv run python main.py \
  --protocol-name BFD \
  --rfc-path data/RFC/BFD.txt \
  --data-directory data/

# 3. Evaluate the generated specification against ground truth:
GEN_DIR=$(ls -dt data/packaged_results/BFD_*/ | head -1)
GEN_FILE=$(find "$GEN_DIR" -maxdepth 1 -name "*.3d" ! -name "initial_*" | head -1)
uv run python eval_3d.py \
  --ground-truth data/ground_truths/BFD.3d \
  --generated "$GEN_FILE"

Ground truth specification files for all 15 protocols are located in data/ground_truths/. The 8 protocols with RFC files available under data/RFC/ are: BFD, BGPv4, DNS, HTTP2, IGMP, NTP, SCTP, BABEL. To run a different protocol, substitute the protocol name and RFC path accordingly.

Output Files

After a successful run, generated artifacts are written to data/packaged_results/<protocol>_<uuid>/:

File	Description
<name>.3d	Final verified format specification (e.g., BFD_CONTROL.3d)
<name>.py	Final parser implementation (e.g., MERGED_BFD_PARSER.py)
<name>.json	Document graph (intermediate representation)

Bug Detection

We can use OSS-Fuzz (libFuzzer) to fuzz protocol daemons in the FRRouting (FRR) network routing suite and the Holo routing suite. libFuzzer is the underlying fuzzing engine of OSS-Fuzz; the experiments use it directly rather than through the OSS-Fuzz's Docker-based integration, so no Dockerfiles or OSS-Fuzz project configuration are required. No custom testing harness is being withheld — the bug-triggering packets and proofs-of-concept (PoCs) are the only components not released, per the ethical considerations discussed in the paper. Fuzzing is seeded with packets generated by SPAR's SMT-based encoder (src/encode/) from verified .3d format specifications.

FRR's upstream fuzz branch already ships with libFuzzer targets for several daemons (bgpd, ospfd, etc.), but does not include targets for BABEL or BFD. The sections below add LLVMFuzzerTestOneInput entry points for these two protocols.

Adding BABEL Fuzzing to FRR

Apply the following changes to the upstream FRR fuzz branch (FRRouting/frr branch fuzz).

1. Add the fuzzer entry point in babeld/babel_main.c

Insert the following block before main() (e.g., after the FRR_DAEMON_INFO declaration at ~line 138):

#ifdef FUZZING
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size);

static bool FuzzingInit(void)
{
	int rc;
	const char *name[] = { "babeld" };

	frr_preinit(&babeld_di, 1, (char **)&name);

	gettime(&babel_now);
	unsigned int seed = 42;
	srandom(seed);

	parse_address("ff02:0:0:0:0:0:1:6", protocol_group, NULL);
	protocol_port = 6696;

	snprintf(state_file, sizeof(state_file), "%s/%s",
		 frr_vtydir, "babel-state");

	master = frr_init();
	babel_error_init();

	resend_delay = BABEL_DEFAULT_RESEND_DELAY;
	change_smoothing_half_life(BABEL_DEFAULT_SMOOTHING_HALF_LIFE);

	if_zapi_callbacks(babel_ifp_create, babel_ifp_up,
			  babel_ifp_down, babel_ifp_destroy);
	babeld_quagga_init();
	babelz_zebra_init();

	rc = resize_receive_buffer(1500);
	if (rc < 0)
		return false;

	return true;
}

static struct interface *FuzzingCreateBabel(void)
{
	struct prefix p;
	struct interface *ifp = if_get_by_name("fuzziface", 0, "default");

	ifp->mtu = 1500;
	SET_FLAG(ifp->flags, IFF_UP);
	SET_FLAG(ifp->flags, IFF_RUNNING);
	SET_FLAG(ifp->flags, IFF_BROADCAST);
	SET_FLAG(ifp->flags, IFF_MULTICAST);

	str2prefix("10.0.2.0/24", &p);
	connected_add_by_prefix(ifp, &p, NULL);

	babel_ifp_up(ifp);

	return ifp;
}

static struct interface *FuzzingBabel;
static bool FuzzingInitialized;

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size)
{
	if (!FuzzingInitialized) {
		FuzzingInit();
		FuzzingInitialized = true;
		FuzzingBabel = FuzzingCreateBabel();
	}

	if (size < 4 || size > 1500) {
		return 0;
	}

	struct interface *ifp = FuzzingBabel;

	if (!ifp)
		return 0;

	unsigned char from[16];
	memset(from, 0, sizeof(from));
	from[0] = 0xfe;
	from[1] = 0x80;
	from[15] = 0x01;

	uint8_t *buf = (uint8_t *)malloc(size);
	memcpy(buf, data, size);

	parse_packet(from, ifp, buf, size);

	free(buf);
	return 0;
}
#endif /* FUZZING */

Wrap main() with #ifndef FUZZING_LIBFUZZER / #endif:

#ifndef FUZZING_LIBFUZZER
int
main(int argc, char **argv)
{
    // ... existing main() body ...
}
#endif /* FUZZING_LIBFUZZER */

Helper functions defined after main() (e.g., babel_save_state_file, babel_exit_properly, show_babel_main_configuration) do not need to be moved — they are compiled for both fuzzer and non-fuzzer builds and are unaffected by the guards.

2. Update the build system

In configure.ac, inside the if test "$enable_libfuzzer" = "yes" block (around line 436), add:

BABELD_SAN_FLAGS="-fsanitize=fuzzer"

and add AC_SUBST([BABELD_SAN_FLAGS]) to the corresponding AC_SUBST section below (around line 445).

In babeld/subdir.am, add before the LDADD line:

babeld_babeld_LDFLAGS = $(AM_LDFLAGS) $(BABELD_SAN_FLAGS)

3. Build & Run

git clone --branch fuzz --depth 1 https://github.com/FRRouting/frr
cd frr
# (apply the changes above)
export ASAN_OPTIONS=detect_leaks=0
export CFLAGS="${CFLAGS} -g -DFUZZING_OVERRIDE_LLVMFuzzerTestOneInput"
export CC=clang
./bootstrap.sh
./configure --enable-libfuzzer --enable-address-sanitizer \
            --enable-static --enable-static-bin
make -j$(nproc)
sudo make install     # optional: installs config files to /usr/local/etc

# Place SPAR-generated seed packets in a corpus directory
mkdir -p babel_seeds
cp <seed_packets>/* babel_seeds/

# Run the fuzzer
./babeld/babeld babel_seeds/ -rss_limit_mb=0

Adding BFD Fuzzing to FRR

Apply the following changes to the same FRR fuzz branch checkout.

1. Add the fuzzer entry point in bfdd/bfdd.c

Insert the following block before main() (at ~line 319, after bg_init()):

#ifdef FUZZING
int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size);

static bool FuzzingInit(void)
{
	const char *name[] = { "bfdd" };

	bg_init();
	frr_preinit(&bfdd_di, 1, (char **)&name);

	master = frr_init();
	bfd_initialize();

	return true;
}

static struct interface *FuzzingCreateBfd(void)
{
	struct prefix p;
	struct interface *ifp = if_get_by_name("fuzziface", 0, "default");

	ifp->mtu = 1500;
	SET_FLAG(ifp->flags, IFF_UP);
	SET_FLAG(ifp->flags, IFF_RUNNING);

	str2prefix("10.0.2.0/24", &p);
	connected_add_by_prefix(ifp, &p, NULL);

	return ifp;
}

static struct interface *FuzzingBfd;
static bool FuzzingInitialized;

int LLVMFuzzerTestOneInput(const uint8_t *data, size_t size)
{
	if (!FuzzingInitialized) {
		FuzzingInit();
		FuzzingInitialized = true;
		FuzzingBfd = FuzzingCreateBfd();
	}

	if (size < BFD_PKT_LEN) {
		return 0;
	}

	struct bfd_pkt *cp = (struct bfd_pkt *)data;

	if (BFD_GETVER(cp->diag) != BFD_VERSION)
		return 0;

	if (cp->detect_mult == 0)
		return 0;

	if (cp->len < BFD_PKT_LEN || cp->len > size)
		return 0;

	if (cp->discrs.my_discr == 0)
		return 0;

	struct sockaddr_any peer = {};
	struct sockaddr_any local = {};
	peer.sa_sin.sin_family = AF_INET;
	local.sa_sin.sin_family = AF_INET;
	inet_pton(AF_INET, "10.0.2.1", &peer.sa_sin.sin_addr);
	inet_pton(AF_INET, "10.0.2.2", &local.sa_sin.sin_addr);

	struct bfd_session *bfd = ptm_bfd_sess_find(cp, &peer, &local,
						    FuzzingBfd, VRF_DEFAULT,
						    false);
	if (bfd != NULL) {
		bfd->remote_timers.desired_min_tx =
			ntohl(cp->timers.desired_min_tx);
		bfd->remote_timers.required_min_rx =
			ntohl(cp->timers.required_min_rx);
		bfd->remote_detect_mult = cp->detect_mult;

		bs_state_handler(bfd, BFD_GETSTATE(cp->flags));
	}

	return 0;
}
#endif /* FUZZING */

Wrap main() with #ifndef FUZZING_LIBFUZZER / #endif:

#ifndef FUZZING_LIBFUZZER
int main(int argc, char *argv[])
{
    // ... existing main() body ...
}
#endif /* FUZZING_LIBFUZZER */

2. Update the build system

Same pattern as BABEL. In configure.ac:

BFDD_SAN_FLAGS="-fsanitize=fuzzer"
AC_SUBST([BFDD_SAN_FLAGS])

In bfdd/subdir.am, add before the LDADD line:

bfdd_bfdd_LDFLAGS = $(AM_LDFLAGS) $(BFDD_SAN_FLAGS)

3. Build & Run

Same build steps as BABEL — rerun ./configure after adding the configure.ac changes, then make -j$(nproc).

# Place SPAR-generated seed packets in a corpus directory
mkdir -p bfd_seeds
cp <seed_packets>/* bfd_seeds/

# Run the fuzzer
./bfdd/bfdd bfd_seeds/ -rss_limit_mb=0

Holo (BFD)

Holo already ships with built-in libFuzzer targets via cargo-fuzz. No source modifications are needed.

# 1. Install cargo-fuzz
cargo install cargo-fuzz

# 2. Clone Holo and list available fuzz targets
git clone --depth 1 https://github.com/holo-routing/holo
cd holo
cargo fuzz list                          # bfd_packet_decode is the BFD target

# 3. Place SPAR-generated seed packets in the corpus directory
mkdir -p fuzz/corpus/bfd_packet_decode
cp <seed_packets>/* fuzz/corpus/bfd_packet_decode/

# 4. Run the BFD fuzz target
cargo fuzz run bfd_packet_decode

The fuzzer runs indefinitely (stop with Ctrl+C). See Holo's fuzz/README.md for additional options such as timeouts, parallel fuzzing, and code-coverage reports.

Seed Corpus

Similar to prior work (ParCleanse), SPAR's generated format specifications and the SMT-based encoder (src/encode/) can produce valid protocol packets and fine-grained invalid test cases from the 3D specification. These generated packets serve as high-quality initial seeds for libFuzzer:

1. Run SPAR on the target protocol to generate a verified .3d specification and parser.
2. Use the encoder to generate packet byte sequences from the specification's field constraints.
3. Save each generated packet as a file in a corpus directory (libFuzzer consumes this directory as a seed corpus).

License

This project is licensed under the MIT License — see the LICENSE file for details.