Nate Foster: Verifying Programmable Network Data Planes

I have been an OCaml programmer for a long time, and I appreciate the tools and the work supported by Jane Street. I want to begin with the original ARPANET topology from the late 1960s and the design choices behind the internet.

Early architects faced a shift from circuit-switched telephone networks to packet switching. They also had to connect networks with different hardware and packet formats. The protocols they designed made this possible with decentralization and robustness as organizing principles.

Modern data-center networks are much larger and more complex. Operators manage thousands of switches running multiple protocols while facing demands for performance and sophisticated processing. An outage can cascade through a data center and affect services that depend on a public cloud.

Operators use practical techniques: high-level policy languages generate device configurations, monitoring and analysis examine those configurations, and tools such as ping and traceroute probe behavior. These methods work well much of the time, but high-profile failures still occur.

Could we bring software verification techniques to networking? We might automatically check connectivity, redundancy, isolation, forwarding loops and traffic balancing. An audience member observes that modern infrastructure is less decentralized; I distinguish the global internet from huge networks owned by individual organizations, which have different management needs.

Software-defined networking has created a new opportunity. Abstractions, APIs and languages now have reasonably precise semantics, so we can consider automatically checking network properties. I will describe a tool for verifying programmable data planes.

A caution: a proof is only as useful as its model and assumptions. A recently disclosed wireless protocol weakness illustrates how a correct formal proof can coexist with an end-to-end attack when the verification model does not match reality. We want practical tools connected to actual implementations rather than merely idealized models.

Our tool, developed with colleagues at Barefoot, checks properties of P4 programs. I will first explain software-defined networks and P4, then review program verification, and finally describe the tool.

Traditional network devices have two parts. The control plane runs software and protocols such as BGP and OSPF to discover topology, compute paths and manage policies. The data plane uses specialized hardware to apply those decisions and forward packets at high speed.

Software-defined networking tries to generalize packet-processing primitives and separate control from the devices. A controller can run on ordinary servers and direct many data planes; centralization of the controller is common but not essential. This makes it possible to express some network algorithms as ordinary programs rather than a separate distributed protocol on every device.

The early vision had a problem: common standards such as OpenFlow did not expose enough data-plane functionality in practice, and sophisticated switch support was difficult to obtain. Hardware designers pursued a more programmable data plane, resulting in fast chips programmable in the domain-specific P4 language.

The RMT architecture has two pipelines around a traffic manager. A parser extracts fields from arriving packets; ingress stages use memory, arithmetic units and state to process them. The traffic manager schedules traffic, an egress pipeline can modify headers after scheduling, and a deparser reconstructs the outgoing packet.

P4 provides a higher-level way to program such devices and can also target software switches and other architectures. It has familiar types and control flow as well as packet parsers and match-action tables. The design aims for predictable work and time per packet: state is bounded, pointers and complex data structures are absent, and ordinary program loops are excluded.

A program can exceed hardware resources and fail to compile, but on the chip I describe, a successfully compiled program runs at line rate. This predictability is central to the architecture. It also makes the programs especially interesting for verification.

A match-action table specifies which fields to read, how to match them, and which actions can run. For an Ethernet source address, a table might use exact matching and select either a learn action, which sends a digest to the control plane, or a no-op. It can also specify a default action and table size.

The P4 program defines the table schema, not the actual entries. The control plane fills in the matching rules and action choices at runtime. This division will matter when we try to verify a program without knowing how its tables will be populated.

A small Ethernet switch program declares headers and metadata, defines a parser and actions, and connects its tables in ingress and egress controls. A standard language and semantics make the packet-processing behavior explicit, rather than hiding it in device-specific configuration.

Programmability can enable more than conventional switching. One project placed a key-value cache on a switch in front of Memcached servers. The P4 program parses requests and uses switch memory for cached values, returning a hit immediately without contacting a server.

Programmability also opens up new errors. To reason about network-wide behavior we need to understand each device, and P4 programs can have subtle bugs. A header may be invalid, much as an object reference can be null; accessing an invalid header can produce an undefined value.

Dynamic validity checks can cost performance, which motivated this unsafe language design, though I dislike undefined values. Other problems include unhandled exceptions, incorrect metadata, inconsistent parsing and deparsing that creates malformed packets, and paths that bypass an access-control table.

The open-source switch.p4 parser illustrates the complexity: its state machine has roughly 50 states to handle Ethernet, VLAN stacks, IPv4, IPv6 and tunnels. A packet without a VLAN tag leaves that header invalid; reading it later may produce undefined behavior. The type system does not precisely document all such validity conditions.

In the demo I use a smaller IPv4 router. Its parser extracts an Ethernet header and branches on its type field: IPv4 packets get an additional IP header, while other Ethernet packets proceed without one. The controls apply tables for routing and rewriting addresses.

Running our verifier without requesting a property succeeds trivially. Enabling the header-validity check instead fails and produces a counterexample: a trace of parser states, packet fields, tables and actions leading to an invalid access. The first failure involves the IPv4 checksum on an Ethernet-only packet.

I add a condition so checksum processing runs only when the IPv4 header is valid. A second counterexample reveals another unguarded IPv4 table access. Adding a validity guard there makes the check succeed: all analyzed paths now access valid headers.

Another property concerns standard metadata specifying the output port or a drop decision. That field is initially undefined, so a program must set it before the traffic manager needs it. The tool finds a path to the end of ingress on which the field has not been defined.

I add a table that drops the relevant non-IPv4 packets and invoke it in an else branch. The verification then succeeds. The example shows how automatically inserted safety assertions and readable counterexamples can help harden even a small working router.

The verification method builds on Hoare and Dijkstra’s work on reasoning about programs with logic. We translate P4 into guarded commands, an idealized imperative language, and generate a first-order formula. If the formula is valid, the assertions and other encoded properties cannot fail under the modeled conditions.

A Hoare-style triple relates a precondition, a command and a postcondition. It says that if execution starts in a state satisfying the precondition and the command terminates, the resulting state satisfies the postcondition. The precondition captures the assumptions under which the claim is made.

The guarded-command language includes expressions and logical formulas, assertions, assumptions, assignments, sequencing and nondeterministic choice. An assertion must hold when reached; an assumption discards executions that do not satisfy it. Assuming false discards everything, which is why assumptions must be treated carefully.

A normal conditional can be represented as nondeterministic choice between two branches, one assuming the condition and the other assuming its negation. Only the branch whose assumption holds contributes an execution. This small language is enough to represent the control flow we need.

Weakest-precondition reasoning starts with a command and a desired postcondition and computes a formula describing sufficient starting states. If the starting state satisfies that formula and the command terminates, the postcondition holds. The calculation is a syntactic translation over the program.

Assertions contribute conjunctions, assumptions contribute implications, assignments substitute expressions, sequencing composes the transformations, and choice requires both branches to satisfy the property. A straightforward translation can create exponentially large formulas, so the tool uses a more efficient equivalent construction.

We use the Z3 SMT solver to check the resulting formula. Validity can be reduced to satisfiability by negating the formula: if the negation is unsatisfiable, verification succeeds; if it is satisfiable, its model supplies a counterexample from which we can construct a trace.

A P4 program is only part of the overall behavior: it defines the processing pipeline and table schemas, but the control plane supplies table entries. Checking every possible table configuration can fail for real programs that depend on unstated control-plane assumptions. We need a way to describe those assumptions explicitly.

Consider VLAN decapsulation from switch.p4. Actions remove zero, one or two tags, and a table reads header-validity bits to choose among them. We want the packet to have no valid VLAN headers after the table runs.

Without assumptions the property fails: the control plane could install a rule that selects no-op for a packet with two tags. The intended behavior depends on the control plane pairing each pattern of validity bits with the right action. That relationship must be captured for the proof to mean what we intend.

We instrument the program with additional ghost state, which we call zombie state. It records table applications, hits, actions and data read. We can then state assumptions such as a particular table hitting or a double-tagged packet receiving the double-tag-removal action, and verify the data plane under those assumptions.

The implementation uses OCaml and libraries including Core and Async; its front end handles the full language. The tool produces human-readable counterexamples and includes optimizations needed for scale. A design goal is to minimize annotations so non-experts can use it.

Built-in flags check standard properties such as valid header access and arithmetic overflow. With the optimizations, Foster reports that a large real program can be checked in well under a minute. The occasional annotations that remain express assumptions about the driver and control plane.

Ongoing work includes synthesizing control-plane assumptions from counterexamples, automatically generating test cases, and checking equivalence or differences between P4 program versions. Restricting the assumption language may make it possible to propose useful assumptions to programmers.

More broadly, networking is beginning to adopt techniques from programming languages: precise abstractions, compilers and runtimes. Important open problems include reasoning across multiple devices and shared state, quantitative properties such as congestion and load balancing, and tools usable by network engineers who are not formal-methods experts.

An audience member asks whether the demonstration verifies only specific inputs. I clarify that, for a single stateless device, the tool symbolically considers every possible execution within its model. The counterexample is a concrete witness to failure, not the only input examined.

The qualification is the control-plane assumptions. We exclude traces that violate stated assumptions, for example assumptions about table hits or action choices. A proposed runtime monitor could check those assumptions at the boundary between control and data planes, but we have not built it; alternatively, a verified control plane could establish them.

Asked about queuing and state, I explain that the traffic manager handles queues and that P4 communicates with it through metadata. Our tool can reason about those metadata bits, but it does not directly prove distributional claims such as weighted fair queuing or the absence of hot spots.

More detailed analysis would need an encoding of input packet distributions and their effect on outputs. At the time of the talk, most targets use fixed-function scheduling; programmable packet scheduler research could make verification of scheduling algorithms an interesting future direction.

An audience member asks why these checks are not expressed as a type system. I initially tried a type-based approach, inspired by work on typed assembly language. Existing P4 programs rely on invariants not captured by a simple compositional type system, so program-logic verification seemed more practical for current users.

With a fresh language design, a type-safe and memory-safe packet-processing language might deliver many standard safety properties while remaining efficient. It might require more annotations or runtime checks when programmers step outside the type system. That would be an appealing direction.

P4 generally excludes loops; parsers are an exception, but implementations typically unroll parser loops statically and reject programs that cannot be bounded appropriately. This restriction is one reason the data-plane analysis is tractable.

Could similar restrictions make control planes easy to verify? I am skeptical about push-button verification of existing control planes. Their software stacks are much larger than P4 data planes and are commonly written in general-purpose languages such as C and Java. A clean-slate design might provide better abstractions, but verifying existing stacks remains difficult.

Finally, an audience member asks how the checked properties are expressed. We work with Barefoot engineers to identify recurring bugs, then traverse the program’s abstract syntax tree and insert assertions—for example, before each header access. At present these visitors are ad hoc rather than a general domain-specific language for properties.