Source-linked AI summary
SymNet: scalable symbolic execution for modern networks
Radu Stoenescu, Matei Popovici, Lorina Negreanu, Costin Raiciu
TL;DR
Network static analysis needs scalable symbolic execution for complex packet-processing boxes, but direct execution of network code branches too heavily. SymNet addresses this with SEFL, a symbolic-execution-friendly modeling language, and reports fast, broad analysis of large networks. The evaluation covers real middlebox behavior and networks, while the approach remains limited to sequential, single-packet-at-a-time processing.
Problem
Direct symbolic execution of network code scales poorly, while existing static-analysis tools cannot model functions such as dynamic tunneling and encryption.
Method
SymNet uses SEFL, a minimalist imperative language that ties packets to execution paths and provides explicit path control for symbolic network analysis.
Results
SymNet captures most real-life network interactions, analyzes large networks with runtimes in the order of seconds, and scales seamlessly with near-optimal branching factors per box.
Takeaways & Limitations
The evaluation shows that symbolic execution can analyze large networks and middlebox behavior beyond simple packet reachability.
Takeaways & Limitations
SymNet processes packets sequentially and keeps only one packet active at a time, so multi-packet processing such as segment splitting or coalescing cannot be modeled.
Abstract
from arXiv · showhide
We present SymNet, a network static analysis tool based on symbolic execution. SymNet quickly analyzes networks by injecting symbolic packets and tracing their path through the network. Our key novelty is SEFL, a language we designed for network processing that is symbolic-execution friendly. SymNet is easy to use: we have developed parsers that automatically generate SEFL models from router and switch tables, firewall configurations and arbitrary Click modular router configurations. Most of our models are exact and have optimal branching factor. Finally, we built a testing tool that checks SEFL models conform to the real implementation. SymNet can check networks containing routers with hundreds of thousands of prefixes and NATs in seconds, while ensuring packet header memory-safety and capturing network functionality such as dynamic tunneling, stateful processing and encryption. We used SymNet to debug middlebox interactions documented in the literature, to check our department's network and the Stanford backbone network. Results show that symbolic execution is fast and more accurate than existing static analysis tools.
1. INTRODUCTION
SymNet addresses the scalability limits of symbolic execution for network analysis with SEFL, a modeling language designed for fast packet-oriented execution. The resulting tool analyzes large networks and captures functionality beyond reachability.
- Motivation: Network static analysis can verify deployed-network properties exhaustively, but modeling complex network boxes remains difficult.Relevant properties include TCP reachability, loop absence, and bidirectional forwarding.
- Motivation: Symbolic execution relates outgoing packets to incoming packets but scales poorly because branching can grow exponentially.This limits direct execution on actual network code and motivates execution on specialized models.
- Approach: SEFL is a network modeling language developed from scratch to enable fast symbolic execution, and SymNet executes SEFL models of network boxes.The approach targets large networks and properties including tunnel safety, MTU issues, and stateful processing.
- Usability: Parsers automatically generate SEFL models from switch tables, router forwarding tables, firewall configurations, and Click configurations.The authors also manually modeled a large subset of Click elements and built a testing tool for SEFL models.
- Evaluation: SymNet was evaluated on documented middlebox interactions, a departmental network, and the Stanford backbone.The reported results describe greater power than existing static analysis tools, broad coverage of real-life interactions, and runtimes in the order of seconds.
2. MOTIVATING EXAMPLES
Existing network-analysis tools and direct symbolic execution struggle with heterogeneous functionality, complex packet processing, and large router tables. SymNet’s motivating design target is packet-oriented symbolic execution whose branching scales with network structure rather than implementation detail.
- Existing tools: Existing static-analysis tools make different tradeoffs among policy expressiveness, modeling language, modeling effort, and checking speed.They also cannot model widely used functions such as dynamic tunneling and encryption.
- Tunneling: HSA represents headers as fixed-size bit sequences, making tunnel modeling possible but limiting analysis of packet contents beyond reachability.The motivating tunnel example asks whether packet contents are preserved through encapsulation and decapsulation.
- Tunneling: NOD can compute tunnel invariants, but its models depend on topology, other boxes, and higher-level protocol headers.This makes modeling cumbersome for heterogeneous topologies and multiple protocols.
- Routing: Hundreds of thousands of prefixes can make router symbolic execution intractable because branching is at least as large as the number of prefixes.The desired alternative is branching that depends on router links rather than prefixes.
- TCP options: C-based symbolic execution becomes costly because branches exponentially increase paths, while simplifying loops and data structures trades complexity for runtime.The motivating target is two orders of magnitude higher than the scale achievable with the shown approach.
- Design target: The target is one or two paths for the TCP-options model, with paths ideally comparable to a box’s outgoing links.This makes symbolic execution tractable on very large networks by focusing on packet-determining paths.
- Design target: C fails to tie packets to execution paths: dropping a packet does not stop execution, and its data structures create additional modeling problems.These limitations motivate a network-specific modeling language.
3. DESIGN OVERVIEW
SEFL treats symbolic execution as part of network modeling, using an imperative language tailored to packet paths and tractable execution. Its packet layout and control primitives provide memory safety, bounded behavior, and explicit path management.
- Design rationale: SEFL was designed as an imperative, verification-driven language that incorporates symbolic execution into network modeling.The goal is to use networking knowledge to simplify the symbolic executor’s task.
- Packet model: Unlike HSA and NOD, SEFL models packets with individually allocated headers at explicit absolute offsets that mimic real implementations.Allocation sizes are explicit and symbolic sizes are disallowed to preserve tractability.
- Path semantics: SEFL ties each packet to an execution path, and unsatisfiable header constraints terminate that path.This differs from C, where packet headers are ordinary variables and paths terminate only at program exit.
- Control primitives: SEFL provides maps, non-branching bounded loops, and explicit drop and fork instructions to control symbolic paths.These features support memory-safe models with bounded memory usage and guaranteed termination.
4. SEFL LANGUAGE
SEFL exposes instructions that operate on packet execution state, metadata, headers, tags, and path constraints. Its primitives encode packet processing directly while avoiding unnecessary symbolic branches.
- Instruction model: Every SEFL instruction consumes the current execution state and produces a new state containing header variables, map entries, values, and constraints.The instruction set is summarized in Figure 2 and Table 2.
- Memory and metadata: Allocate treats integer-valued locations as headers with memory checks and string-valued locations as metadata keys in SymNet’s map.This separates aligned packet memory from unaligned metadata.
- Header addressing: Tags support indexed addressing relative to dynamically defined layer boundaries, enabling encapsulation and decapsulation.SEFL can define tags absolutely or relative to other tags and provides shorthand names for header fields.
- Path control: Constrain filters the current path without branching, whereas Fail stops the path and reports an error.For non-HTTP packets, SEFL adds TcpDsp==80 to the current path instead of creating the two C execution paths.
- Path control: If forks execution into constrained branches, while For iterates over a snapshot of matching map keys without branching.InstructionBlock groups multiple instructions on a branch, and NoOp represents an empty branch.
5. SYMBOLIC EXECUTION
SymNet executes SEFL models by injecting symbolic packets and propagating feasible execution paths through network elements. Its value stacks, assignment histories, and simplified expressions support efficient, path-complete network analysis.
- SymNet execution: SymNet analyzes network configurations by executing models of elements connected through input and output ports.It begins with an empty packet, creates a symbolic packet of the requested type, and injects it at a user-specified input port.
- SymNet execution: Execution instructions modify path state, spawn paths, and forward feasible packets across linked output and input ports.Forward and fork instructions determine how packets move through the modeled topology.
- Symbolic state: Each symbolic or concrete value carries per-path constraints, while value stacks and assignment histories preserve evolving variable state.These structures support masking and restoration of variables and retain the history needed for network-wide reasoning.
- Symbolic state: SEFL simplifies symbolic execution by supporting only simple expressions, reducing state-representation complexity without path-prioritization heuristics.SymNet seeks all possible network execution paths rather than merely covering model instructions.
- Execution example: In the port-forwarding example, constraints split packets by destination port, with one path rewriting destination fields and another preserving the alternative case.The example uses symbolic IpDst and TcpDst fields and creates a second packet through the If instruction.
6. NETWORK VERIFICATION
SymNet verifies network behavior by propagating symbolic packets and inspecting path constraints, state histories, and header values. These mechanisms support reachability, loop detection, invariants, visibility checks, and header memory-safety analysis.
- Reachability: Reachability analysis injects a symbolic packet at a source port and inspects constraints and header values at every reached port.This reveals which packets can reach outputs and how their headers change along each feasible path.
- Reachability: In the port-forwarding example, output port 1 requires TcpDst==123 and rewrites destination fields, while output port 2 accepts TcpDst!=123.The path history exposes both the input condition and the resulting packet behavior.
- Loop detection: Loop detection compares saved and current execution states and uses a solver query to determine whether the new state contains the old state.The query !n & o searches for an old-state point excluded from the new state; no counterexample indicates a loop.
- Loop detection: The generic loop detector can identify forwarding loops when state comparison is restricted to destination and source IP addresses.Comparing the entire state misses traditional forwarding loops because TTL decreases on each hop.
- Additional checks: Value-stack inspection checks field invariance, header visibility across network hops, and memory safety during header creation and destruction.Incorrect header tags or assumptions about header locations cause execution paths to fail, exposing encapsulation problems in models.
7. MODELING NETWORKS WITH SEFL
SEFL models packet processing with symbolic tags, constraints, and state while controlling branching for switches, routers, NATs, and middleboxes. The models capture network behavior from forwarding and stateful translation to TCP-option filtering and encryption.
- Packet modeling: SEFL represents packet layers with tags that are allocated relative to one another as packets move through the modeled stack.Start and End tags are always present; other layer tags are set as processing advances.
- Switch modeling: Switch models group destinations by output port, achieving one execution path per output port with an egress model.The egress model also minimizes constraints when MAC-table constraints are mutually exclusive.
- Router modeling: Router models transform longest-prefix forwarding rules into constraints that preserve correct matching while reducing paths to the number of links.More-specific prefixes are constrained not to match when a more-specific rule has already been selected.
- NAT modeling: NAT models assign symbolic ports within the available range and store per-flow mappings for return-path restoration.The return path restores original addresses and ports only when matching metadata is present; the model creates no branches for this check.
- Stateful processing: Per-flow metadata also models stateful firewalls and related middleboxes without state explosion when state is independent across flows.This is explicitly identified as a strong assumption of the technique.
- ASA options parsing: The TCP-options model uses metadata variables so options can be stripped without branching while preserving which options pass and under what conditions.It always sets MSS and rewrites its value to at most 1380; the model captures more properties than Klee on the C code.
- Encryption: The encryption model replaces payload contents with a fresh symbolic variable and permits recovery only with the matching key.This captures confidentiality after encryption and correct decryption without predicting the ciphertext.
- ASA modeling: Accurately modeling ASA behavior remains difficult because sparse documentation obscures inspection behavior such as TCP connection interception.The ASA may act as a server until a connection is established, protecting machines behind it from TCP SYN floods.
8. EVALUATION
SymNet’s evaluation shows that symbolic-execution performance depends strongly on model structure, with grouped egress models scaling to large forwarding tables and outperforming more branching alternatives. The evaluation also demonstrates practical coverage, automated model checking, and discovery of configuration and implementation bugs in real networks.
- Performance evaluation: More than 90% of runtime is spent in Z3 as SymNet scales switch tables from 440 to 500,000 MAC entries.The experiments duplicated entries with unique destination MAC addresses to increase table size.
- Coverage analysis of TCP options code: SymNet identifies coverage differences with Klee: it runs the options code in 1s and captures option behavior, but not the C code’s memory-safety and bounded-execution properties.SymNet still ensures memory safety and bounded execution for the SEFL model by construction.
- Automated testing: The automated testing framework compares symbolic model paths with concrete Click or hardware executions, using solver-generated packets and captured outputs to report mismatches.It first explores all symbolic paths, then tests random inputs until stopped.
- Automated testing: Testing exposed incorrect mirroring, TTL underflow, field-checking, and classifier bugs, while ASA comparison found ingress drops and asymmetric VLAN traffic handling.The ASA model was enhanced to behave as a stateful firewall for office-to-lab traffic after the comparison uncovered incorrect return-traffic drops.
- Verifying the CS Department Network: The department-network model covers 21 devices, 235 ports, 6,000 MAC entries, and 400 routing entries, enabling reachability and TCP-option analysis.A purely symbolic office packet produced 3,000 paths in 42s; specializing addresses reduced this to 50 paths and 10s.
9. RELATED WORK
SymNet is compared with existing network verification approaches across modeling scope, scalability, and supported functionality. Its distinguishing strengths are memory correctness and broad coverage, although scalability depends on well-written models.
- Existing tools use Boolean formulas, Datalog, or model checking, while SymNet uses symbolic execution to model broader network behavior.The comparison includes AntEater, Network Optimized Datalog, and model checking for stateful middleboxes.
- SymNet’s memory correctness is identified as a differentiating feature among network verification tools.
- SymNet scales very well on optimized models, but poorly written models or inherently many branches can cause complexity to grow rapidly.The comparison classifies runtimes of seconds as high scalability, minutes as medium, and hours as low.
- SymNet has the broadest reviewed functionality coverage, but cannot model packet splitting or coalescing.
- SEFL is strictly more general than NetKAT and Frenetic because it can model middlebox behaviors as well as layer-two behavior.
10. LIMITATIONS
SymNet processes packets sequentially and keeps only one packet active at a time. These design constraints exclude parallel processing and operations spanning multiple packets, although multiple round trips can still be simulated.
- SymNet’s sequential packet processing does not model parallel processing, whose possible thread interleavings are significantly harder to check.
- Only one packet is active at a time, so processing across multiple packets cannot be modeled.
- TCP segment splitting and coalescing are excluded because they require processing across multiple packets.
- The single-packet limitation restricts in-flight packets but still permits simulation of any number of round-trip times.
11. CONCLUSIONS
The paper introduces SEFL and SymNet to make symbolic execution practical for production-network analysis. The resulting models cover diverse devices and behaviors, scale to large networks, and reveal concrete network properties and misconfigurations.
- SEFL is a minimalist imperative language designed specifically for scalable network symbolic execution, and SymNet executes SEFL models.
- SymNet models switches, routers, stateful middleboxes, TCP options, and a large subset of Click router elements.
- Near-optimal branching factors per box and seamless scaling to large networks characterize the evaluation results.
- SymNet captures middlebox behaviors reported in the literature and identifies interesting properties in the authors’ department network.
- SymNet is reported to be fast while exposing network properties through analysis of real network configurations.