Automated Verification of Network Function Binaries

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

Klint verifies network-function binaries without source code or debug symbols. Its abstraction boundary is the network function’s environment: calls to packet I/O and data-structure operations reveal types and control-flow constraints. Data structures are specified with “ghost maps,” abstract maps used only in contracts. The paper’s abstract says: “We implement our technique in Klint, a tool with which we verify, in minutes, that 7 NF binaries satisfy their specifications” (Abstract, p. 585). The approach is symbolic execution plus map-based contracts and inferred invariants; the evaluation includes C and Rust implementations, DPDK and BPF environments, and full-stack verification.

technique 1: environment-driven binary verification

Inference: Use this when operators receive a binary and need functional, memory-safety, or crash guarantees without trusting the compiler for the network-function code. Require a binary with explicit calls to environment and data-structure operations, a Python specification, and Python contracts for each data structure (Section 1, pp. 585–586). Dynamically linked symbols identify environment interactions. Klint replaces data-structure implementations and fundamental networking operations with contracts, symbolically executes initialization, infers packet-loop invariants, and checks every packet-processing path against the specification (Section 5, p. 593). It returns a proof or counterexample, subject to a user-defined execution limit if single-packet processing does not terminate (Section 1, p. 586). Without a high-level specification it can still check crashes and out-of-bounds accesses (Section 5, p. 593).

The model assumes single-threaded initialization and packet processing. Persistent state is accessed through environment capabilities acquired only during initialization; timers must be checked while processing packets (Section 2.1, p. 587).

Inference: a proposed Verus adaptation could describe firewall behavior with a spec fn and packet-processing preconditions and postconditions with requires and ensures. Connecting such source-level contracts to a deployed binary would require a separate proof or assumption relating machine behavior to those contracts. This paper does not evaluate Verus or provide that connection.

technique 2: ghost maps as a universal abstract data structure

Inference: use maps when a data structure’s concrete layout is irrelevant to the network-function specification but operations need precise abstract effects. Klint exposes length(M) → Int, get(M,K) → V | None, set(M,K,V) → M′, remove(M,K) → M′, and forall(M, λ(k,v) → Bool) → Bool (Listing 1, p. 589). It tracks explicitly accessed known items as (key,value,presence) triples and summarizes all other entries by one unknown item plus an invariant. get reuses an item when its key must match under the recursion condition; otherwise it adds a fresh item and constraints for key consistency, the unknown-item invariant, and a bound on the number of distinct present known items. set layers a changed item over the prior map and increases length only for a previously absent key; remove clears presence and decreases length only for a present key (Section 3.4, pp. 590–591; Appendix B, p. 600). forall checks the predicate on present known and unknown items and constrains future unknown items if its result is true. A false result leaves future items unconstrained, making this case sound but incomplete (Section 3.4, p. 591). This avoids branching over every array cell. The paper explains the tradeoff: “Ghost maps are an intermediate step between quantifier-free bit vectors, which are decidable due to their finite size but not expressive enough, and arrays with universal quantifiers, which are more than expressive enough but undecidable” (Section 3.2, p. 589).

Map layers preserve dependencies between versions by sharing a base map; items and invariants discovered by get and forall are added to the bottom layer. A condition and value hint stop invariant recursion in common cases, but do not guarantee termination: “This strategy avoids recursion in common cases such as our example of maps with reciprocal keys and values, but it is not complete, as the engine may recurse infinitely” (Section 3.4, p. 591). The translation produces formulas over quantifier-free bit vectors. The authors believe ordered structures such as queues and stacks may be a poor fit for invariant inference (Section 3.4, p. 591).

Inference: a proposed Verus adaptation could represent abstract state with a ghost Map, specify operation effects, and prove that concrete operations preserve the relation between implementation state and the map. This would transfer the abstraction idea; the paper does not establish an equivalent Verus encoding or solver behavior.

technique 3: fixed-point invariant inference

After initialization, start with the strongest invariant describing the exact initial state. Symbolically execute one packet-processing iteration; relax invariants when resulting states violate them; execute again with the relaxed set; repeat until all invariants hold on the resulting states (Algorithm 2, Section 4, p. 592). Relaxation can discover relationships such as equal map lengths or “all keys of table are also keys in statistics.” The set can only shrink, so the algorithm converges, possibly to no invariants. Known items provide candidate relationships, and unknown-item constraints validate candidates across unobserved entries. The paper’s key operational statement is: “The key to inferring useful invariants is to use ghost maps’ known items to form invariant candidates, and then check whether these candidates hold using the unknown items” (Section 4, p. 592).

Inference: a proposed VL workflow could state an invariant as a Verus spec fn, then prove initialization and preservation through one packet-processing iteration. Any proposed invariant would need those proofs; assuming it would leave an additional trusted premise. The paper does not implement this workflow.

technique 4: full-stack contracts and hardware actions

Klint can verify a network driver and most of a minimal operating system. It models heap memory as maps, matches register writes to hardware actions using a NIC description, checks action preconditions, and applies postconditions for register effects (Section 5, p. 593). The authors state: “while the network function and its network driver can be compiled together, the environment has to be compiled separately and then linked together without link-time optimizations, ensuring the symbols corresponding to environment operations exist and can be given as an input to Klint” (Section 5, p. 593). Full-stack verification substitutes contracts only for data structures and the memory allocator; the authors report machine-checked proofs that these implementations obey their contracts (Section 5, p. 593).

Inference: a proposed Verus model could expose NIC state as ghost state and specify driver operations with preconditions and postconditions. A proof against that model would still depend on its agreement with the hardware and foreign-code behavior. Those assumptions should be stated separately from the verified driver obligations.

technique 5: specification extraction from standards and RFCs

Klint specifications can be written directly from standards while abstracting implementation state to maps. Appendix A models a bridge from IEEE 802.1D, a router from RFC 1812, a NAT as a flow-to-update-time map, a policer as bucket-to-token and address-to-bucket maps, and Maglev as flow-to-backend and backend-to-heartbeat maps (Appendix A, pp. 599–600). The bridge specification checks that a transmitted frame does not leave through its reception port; translating the standard exposed one implementation bug. The BPF programs lacked formal specifications, so the authors checked only memory safety and crash freedom.

Inference: VL can follow this extraction pattern by freezing a standard-derived spec fn contract, then proving Rust code against it with requires/ensures. The standard interpretation and any omitted edge cases are still specification assumptions; a successful proof does not validate the standard itself.

evidence and limits

The evaluation verifies six network functions (bridge, firewall, Maglev, NAT, policer, router) from binaries without debug symbols. Total verification times range from one second for the router to 119 seconds for the bridge on an Intel i7-7700HQ; the bridge has 32 inferred invariants and firewall 20 (Table 1, p. 594). Full-stack verification adds 15 minutes per function, mainly driver-action inference (Section 6.1, p. 594). Five existing BPF programs receive memory-safety and crash-freedom checks without functional specifications: bridge and firewall in seconds, CRAB and Suricata in under two minutes, and Katran in almost four hours because packet contents were modeled as a large ghost map (Section 6.3, p. 596). The paper reports 10 Gb/s without loss for all five Klint network functions in its single-link benchmark, while Vigor baselines range from 3.47 to 9.12 Gb/s; latencies are measured with 1 Gb/s background load and reported at the 50th and 99th percentiles (Table 2, p. 595).

Klint found and fixed two implementation bugs using specifications based on standards (Section 6.1, p. 594). Limits include no shared-state multithreading, dynamically linked data structures, packet-arrival-only triggers, and no verification of protocol-level properties or data-structure implementations by Klint itself (Section 7, p. 597). Specification structure fields must currently match the order of implementation fields (Section 6.1, p. 594). Total verification time can vary by dozens of seconds with minor Klint or Z3 changes (Section 6.1, p. 594). The seven functionally verified binaries are six in C and one in Rust (Section 9, p. 597); Section 6.3 describes the Rust policer, while Table 1 lists six network functions.

Inference: Klint suggests a possible extension for VL: connect source-level proofs to deployed binaries through explicit environment contracts and a proof relating source and binary behavior. The paper demonstrates binary checking under its assumptions; it does not establish the feasibility or cost of such a Verus pipeline.

what is proved, measured, and trusted

Klint uses angr and Z3 to establish path obligations under supplied contracts (Section 5, p. 593). The paper explicitly lists the full-stack trusted computing base as “Klint itself, including angr and Z3; the bootloader; the hardware; and the VeriFast [25] theorem prover we use to verify the memory allocator and data structures” (Section 5, p. 593). It additionally trusts the C compiler for the data structures and allocator because VeriFast verifies their source code. Measured evidence covers verification time, invariant counts, throughput, latency, and BPF applicability (Section 6, pp. 594–596). Inference: guarantees are relative to the supplied specifications, contracts, and environment and hardware models; proving conformance does not establish that those descriptions capture every intended requirement.

techniques for the catalog

• environment-driven binary checking — infer types and control flow from linked environment interactions and symbolically execute all binary paths
• ghost-map abstraction — summarize data structures expressible by map-based contracts with known items, an unknown-item invariant, and map-operation contracts
• fixed-point invariant inference — relax strongest initial invariants through packet-loop executions until a stable sufficient set remains
• contract-based full-stack verification — model memory, drivers, and NIC actions with preconditions and postconditions down to the hardware boundary Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “During symbolic execution, memory allocations return symbolic pointers, ensuring that Klint will explore all paths even if some paths depend on the value of pointers.”): checked all paper text, study claims, quotations, numbers, section and page references, technique steps, and the publisher link; corrected recursion limits, full-stack scope and linking requirements, trusted components, page references, and unsupported Verus claims; did not check the implementation, reproduce experiments, or independently validate proposed Verus adaptations.

Last edited: 2026-10-16