Iceberg: Automated Verification of DNS Authoritative Engines via Just-in-Time Summarization

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

problem and result

Iceberg verifies DNS authoritative engines through refinement proofs without per-layer manual specifications below the top level. Its central claim is: “we propose just-in-time (JIT) summarization, a refinement-proof approach that utilizes invariants from DNS zones to enable the use of automated summaries throughout verification.” It parses LLVM IR and spec, a Rust-like functional specification language, then symbolically executes top-down from an entry function, building a summary for each callee in the context where it is called (§4, §5).

technique: invariant-driven JIT summarization

The paper motivates it by DNS engines operating “with pre-configured DNS zones, which provide rich state and type invariants in the form of fixed arguments, constant memory, and well-formed data structures” (§1, §3.3). Inputs: a top-level specification, LLVM IR, library emulations and stubs in spec, and a JSON memory dump of the configured zones that sets up the initial memory state (§4.2). Symbolic execution walks each function’s control flow graph depth-first and grows a tree of effects: Assume on entering a feasible branch, Return plus nodes for heap (de)allocations and memory writes on return, Panic on erroneous operations such as out-of-bound access (§5.2, Table 2). JIT state splitting limits a state to individual concrete values and grows a Specialize node when the state is (a) used as a pointer offset or array index, (b) dereferenced as a pointer, (c) evaluated against a Specialize during summary application, or (d) marked with the specialize primitive in a stub (§5.2). At a call, Iceberg builds the callee’s summary if none exists, using the current state with its invariants, then applies it; recursive calls are inlined (§5.2, Algorithm 1).

The paper’s workflow is explicit: “Step 1. Supply a top-level specification in spec”; “Step 2. Supply the target program as LLVM IR files”; “Step 3. Supply library specifications for emulated library calls and stub functions”; “Step 4. Supply zone invariants”; “Step 5. Initiate push-button summarization of the entry function”; and “Step 6. Check the summary of the entry function for any specification violations.” When applying a summary, a Specialize node checks that the summary was built in the same context as the call site; if all sibling Specialize nodes fail to match, Iceberg re-summarizes the callee in the current context and merges the result into the existing summary tree (§5.3, Algorithm 2).

Inference: In Verus, the top-level specification maps to requires/ensures and ghost state; state-splitting facts map to branch-specific proof obligations. A spec fn can describe the ideal DNS response, but executable lookup code still needs ordinary Rust. Verus does not provide Iceberg’s LLVM summary engine, so this workflow is a design analogy rather than a direct port.

technique: unified region-based memory model

Represent memory as disjoint regions, each state identified by a region and an integer offset, with Stack, Global, Const, and Heap regions and lifetime tracking “to model behaviors such as dangling pointers, memory leaks, and more complex memory management issues” (§5.1). Region layout is tracked down to the scalar level using the LLVM data layout string; the paper says this “induces less overhead than the byte-addressable memory in KLEE, while remaining more flexible than the typed memory in DNS-V, which is often confused by LLVM’s aliased or untyped memory addressing.” Symbolic regions make pointer summaries reusable: during building, actual stack and heap regions are replaced by incremental integer IDs; during application, the IDs are bound one-to-one to concrete regions when evaluating Specialize nodes, and binding failure triggers the same re-summarization (§6.1).

Inference: Verus’s ownership and borrowing remove many runtime aliasing cases, but unsafe FFI or raw pointers still require explicit ghost region invariants. Model memory safety with requires pointer validity and ensures preservation; leave allocator correctness trusted unless separately verified.

technique: summary optimization and stubs

Summary optimization passes transform summary trees into “more verification-friendly forms” to reduce back-end solver overhead (§6.2). MinimizeAssume removes Assume nodes implied by earlier branch conditions (nodes without feasible siblings); MergeAssume recursively merges subtrees with identical effects, “eliminating the preceding Assume conditions entirely.” The paper states: “none of the verification processes in §7 terminates without these optimizations.” A stub function in spec shares the interposed function’s parameters and “always returns a boolean”; Iceberg evaluates it right before summarizing the original function and uses its return value as an extra path constraint; stubs can hint extra invariants, force state splitting with specialize, or print debug information (§6.3). The paper applies stubs “to limit the verification scope or hint JIT state splitting”, found the need for them through “timeouts and inspection of summaries” (§7.1), and used them, “especially the specialize hints”, for HickoryDNS’s async state transitions (§7.2). Library calls are emulated separately in spec (Figure 9).

Inference: In Verus, stubs correspond to trusted external specifications only when their contracts are explicit. Keep them small and annotate assumptions; external_body on the function being verified would defeat the proof and is not an equivalent technique.

technique: top-level reference checking

“For simplicity, users can write a wrapper function that compares the results of the ideal model and the implementation, picking the wrapper function as the entry. Bugs then manifest as branches with unequal results.” (§4.2) Safety violations “manifest as failed paths in the top layer” (§9). The base reference model comes from RFCs covering the core algorithm, DNS records, error clarification, wildcards, rcode clarification, DNAME redirection, and glue clarification; because RFCs are not exhaustive, each implementation gets its own top-level specification derived from that model (§7.1). Iceberg emulates “a small subset of the Go runtime, the C and C++ standard libraries, and Rust intrinsics”, adds an extension emulating C++ exceptions with a Throw effect, and handles Rust async state machines through state splitting plus stubs (§7.1, §7.2).

evidence, trust, and limits

Iceberg is over 16,000 lines of Rust. It verifies CoreDNS (Go), Bind 9 (C), PowerDNS (C++), and HickoryDNS (Rust), whose verified code Figure 8 sizes as O(2,000), O(10,000), O(5,000), and O(4,000) LOC respectively. It reports 12 new bugs: 8 CoreDNS, 2 PowerDNS, and 2 HickoryDNS; 7 are acknowledged by developers; no new Bind 9 bugs were found on the test zones (§8.1). SCALE, run on the same zones, finds only 2 of the 12 (Table 4). Table 5 reports specification-to-code ratios, computed with stubs, of 9.6% (CoreDNS), 7.5% (Bind 9), 5.8% (PowerDNS), and 7.8% (HickoryDNS). The paper reports “an initial porting time of one person-week upfront for all verified engines, with subsequent retrofitting across versions taking as little as one person-hour” (§8.2). Simple and complex zones finish in under half an hour; real zones take a few hours (§8.3).

The trusted base includes the LLVM toolchain, Z3, Iceberg itself (JIT summarization implementation, library emulations, top-level specifications), and memory management intrinsics and language-level APIs (§9). Verification covers core lookup logic, “excluding file I/O, networking, concurrency, and other peripheral features such as rate limiting” (§7). Modeling shortcuts include an abstract hashmap for Go’s map in CoreDNS, Bind 9’s hash function replaced by an identity function, and 7 manual type annotations added to Bind 9’s IR (§7.2). Functional correctness holds only up to the top-level specification; lower layers are not checked for functional correctness, though safety is ensured in all layers (§9). The modeled RFCs omit DNS updates, caching, and security aspects, which the paper attributes to specification effort, “not a hard restriction”; rate limiting or cache invalidation over time “are indeed too complicated for Iceberg” (§9). Inference: agent-written verified Rust benefits from invariant-driven summaries when state is fixed and structured, but product risk remains high for mutable configuration, concurrency, and underspecified reference models. VL should reuse the idea of specializing proofs from concrete configuration while separately verifying the summary engine and its trusted specifications.

techniques for the catalog

• invariant-driven JIT summarization — specialize symbolic states with concrete configuration invariants only in the calling contexts actually reached
• effect-tree summaries — record assumptions, specializations, memory stores, allocations, frees, returns, and panics as reusable path summaries
• symbolic memory regions — abstract stack and heap identities to make pointer summaries reusable across calls
• summary optimization — remove implied assumptions and merge identical-effect branches before solver use
• interposing stubs — inject invariants, specialization hints, debug output, and scope limits into top-down verification
• reference-wrapper checking — compare implementation and ideal DNS responses and treat unequal branches or failed paths as violations Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “In this case, Iceberg resorts to re-summarization of the function and merges the resulting summary (containing the current context) into the existing summary (containing all past contexts).”): read all 1052 lines of the paper text and checked every quotation, number, section reference, and technique step; changed the link to the paper’s USENIX presentation page, listed the four JIT state-splitting rules, corrected the memory-model comparison (less overhead than KLEE’s byte memory, not more precise), corrected re-summarization (all sibling Specialize nodes must fail), removed unsupported stub uses (library modeling, unsupported runtime behavior), corrected the wrapper (zone is concrete), attributed LOC sizes to Figure 8, split omitted features into effort-limited and too-complicated, and added the scope exclusions and modeling shortcuts; did not check figures’ graphical content (Figure 10 timings) beyond the text, nor the Verus inferences.

Last edited: 2026-10-17