Source-linked AI summary
Axiom: a logic programming language to express and enforce network designs
Tibor Schneider, Laurent Vanbever
TL;DR
Network verifiers face difficulty accurately modeling devices, scaling, and pinpointing faulty commands because they do not know how operators intend to implement network behavior. Axiom expresses those design choices as rules over configurations and checks them through a single Datalog program. It checks TopologyZoo networks with route reflection in 0.3 seconds, including the largest 754-router network, and specific designs identify responsible commands.
Problem
Network verifiers struggle to model deployed devices accurately, scale to large networks, and report which configuration commands cause misbehavior.
Source: §1 · p. 1Method
Axiom expresses operators’ design decisions as rules over configuration commands and compiles them into a network-wide Datalog check on configurations.
Source: §1 · p. 1Results
0.3 seconds sufficed for Axiom to check every TopologyZoo network with route reflection, including the largest 754-router network, while specific designs pinpoint responsible commands.
Source: §5 · p. 5Takeaways & Limitations
Negative provenance is a first step toward suggesting commands and, through repeated suggestions, completing configurations from the design.
Source: §7 · p. 6Operators must write the design and ensure it is correct, since Axiom guarantees that configurations implement the design but not that the design itself is correct.
Source: §1 · p. 2
Abstract
from arXiv · showhide
Human errors remain the leading cause of network outages. To prevent them researchers propose general verifiers that analyze the network behavior. Yet, their (symbolic) models struggle to accurately reflect network devices, they fail to scale to large networks, and report misbehavior, not what configuration line caused it. We attribute all three challenges to specifications that describe the intended behavior but not how operators intend to achieve it---the network's design: which protocols to run and how to combine them. We present Axiom, a language for expressing network designs, and a checker that finds every violation and the responsible commands. Operators state their design decision as rules over configuration commands. Axiom then compiles them into a single Datalog program that checks the entire network directly on its configurations, not on the state they produce. Our prototype checks a 754-router network within seconds. Ultimately, a design enforced on every keystroke could give network operators the integrated development environment that programmers have long enjoyed.
1 INTRODUCTION
Network verifiers struggle with device fidelity, scale, and actionable debugging because they must accept many possible implementations without knowing the operator’s design. Axiom makes that design explicit as rules over configuration commands, enabling network-wide checks that locate violations at their source.
1 INTRODUCTION
- Verifiers struggle to model deployed devices accurately, scale to large networks, and identify the commands responsible for misbehavior.The paper attributes these challenges to verifiers accepting many possible implementations without knowing how operators intend to achieve the behavior.Source: §1 · p. 1
- A design specifies how operators intend to implement behavior, letting checks focus on the protocols and implementation choices actually used.For example, the design can require iBGP sessions to form a route-reflection topology rather than merely requiring reachability.Source: §1 · p. 1
- Axiom lets operators express their own design decisions as Datalog rules over configuration commands and checks the resulting design across the network.It checks configurations directly rather than modeling the network state they produce.Source: §1 · pp. 1–2
- Axiom requires operators to write and validate the design, but they need model only the commands and decisions they use, not forwarding-state computation.Explicit designs may also support configuration tools, including command-level feedback, fix suggestions, and constrained generation.Source: §1 · p. 2
2 AXIOM BY EXAMPLE
The example turns router configuration into relations, joins those relations to identify iBGP peers, and checks that each router has a session with every other router in its AS.
2 AXIOM BY EXAMPLE
- Axiom combines set statements that store configuration-derived facts with assert statements that check properties over those facts.For the example, it generates one network-wide Datalog program.Source: §2 · p. 2
- Datalog joins address and AS relations across routers to derive iBGP sessions and check whether a configured neighbor has the stated remote AS.If no router owns the configured neighbor IP, no session is derived and an assertion catches the case.Source: §2 · pp. 2–3
- The full-mesh assertion requires every router to maintain a session with every other router in its AS and reports the offending command for each failure.Distinct failures include a mismatched remote AS, an unowned neighbor IP, and a missing session.Source: §2 · p. 3
3 CHECKING A NETWORK DESIGN
Axiom trades generality for expressivity: a specific design checks a chosen implementation cheaply and precisely, while a generic specification accepts more implementations but can be costly and less diagnostic. Designs can also check global properties directly from configuration when they fix how those properties are implemented.
3 CHECKING A NETWORK DESIGN
- A specific design is cheap to check and points errors to concrete commands, but rejects otherwise-correct configurations that use a different design.Generic specifications accept a broader range of configurations, but are weakly tied to configuration edits, making checks expensive and violations hard to attribute.Source: §3 · p. 3
- Axiom can express generic route propagation and specific iBGP full-mesh designs, with the specific design using simple joins to identify a missing session directly.The generic version checks route propagation recursively but reports the symptom rather than why propagation failed.Source: §3 · p. 3
- For IPv6 segment-routing waypoints, a design checks IGP configuration, firewall-segment insertion, and the absence of static-route overrides directly on configuration text.The stated guarantee covers every failure that leaves the network connected, without an explicit failure model.Source: §3 · p. 3
- Designs can enforce performance objectives such as forwarding-table limits through route filters, OSPF route caps, and a default route, but the approach’s limits remain open.The authors conjecture that most reachability and security properties can be expressed by trading generality for expressivity.Source: §3 · p. 3
4 AXIOM
Axiom accepts a network description, device configurations, and design files, then maps configuration matches and design rules into Datalog. Its stratified Datalog machinery supports network-wide relations and absence checks, while the prototype executes the generated program but does not yet evaluate incrementally.
4 AXIOM
- Axiom takes network topology, device configuration paths and parsers, and design files as inputs, and matches a common tree representation of configurations.The language can match router, switch, and application configurations and express dependencies across them; semantics remain in vendor-specific designs.Source: §4 · pp. 3–4
4.1 Stratified Datalog with Lattices
- Datalog joins connect configuration facts across devices, recursion expresses global properties, and stratification permits checks for absent facts after relations are evaluated.Lattices support best-value operations such as selecting a longest prefix or shortest path; the language can encode prefixlists and route-maps, though not always conveniently, and some features remain missing.Source: §4.1 · p. 4
4.2 Execution
- The prototype matches design blocks against parsed configurations to generate Datalog, then evaluates the program by strata and checks assertions after referenced relations are complete.It uses a custom engine for lattice semantics, but does not yet evaluate incrementally.Source: §4.2 · p. 4
5 EARLY RESULTS
The evaluation tests design concision, scalability, and differences between specific and generic designs using generated Cisco configurations across TopologyZoo networks, including one with 754 routers.
Specific designs
- The specific designs use 140 lines, 19 templates, and 18 rules to check configurations exceeding four million lines.The designs cover interfaces, OSPF, and iBGP.Source: §5 · p. 5
Generic design
- The generic design accepts propagation-dependent OSPF and iBGP alternatives using 162 lines and eight more rules than the specific design.It constructs a propagation graph and checks for valid paths between router pairs.Source: §5 · p. 5
Scaling
- Route-reflection checks finish within 0.3 seconds even for 754 routers, while full-mesh checks take up to five seconds and Batfish takes over two orders of magnitude longer.The full-mesh configuration grows to 4.57 million lines, almost 100 times more than with route reflection.Source: §5 · p. 5, Figure 3 · p. 5
Specific versus generic designs
- Specific designs check almost 2× faster for iBGP full mesh and 10× faster for route reflection, using a tenth of the memory required by generic designs.The comparison is on the largest network in the dataset.Source: §5 · p. 5, Table 1 · p. 5
Error localization
- Specific designs identify the missing OSPF interface or exact missing iBGP session, whereas generic designs report only reachability symptoms.A verifier would report both cases as the same externally advertised-route reachability failure.Source: §5 · p. 5
6 RELATED WORK
Axiom checks configuration directly and adds recursive design checks beyond existing configuration-query tools, while complementing behavioral verification, synthesis, and network programming languages.
Query-based configuration checking
- Configuration-query tools check predefined faults, consistency, or operator-written conditions, but NCGuard and Concord lack recursive queries for graph properties that Axiom can check.Rcc, SelfStarter, NCGuard, and Concord represent different approaches to querying or checking configurations.Source: §6 · p. 6
Behavioral verification and synthesis
- Simulation and verification assess network behavior, synthesis generates configurations from intended behavior, and LLM management invokes verifiers; Axiom instead checks how configurations implement designs.These tools can complement Axiom by validating designs or producing configurations held to them.Source: §6 · p. 6
Programming languages for networks
- Propane, NetKAT, and NDlog capture network behavior or computation, whereas Axiom captures the network’s design.NDlog models route computation and derives routing state as a fixpoint.Source: §6 · p. 6
7 DISCUSSION AND OUTLOOK
Axiom’s discussion identifies two language gaps in representing configuration behavior and describes how negative provenance could support explanations and synthesis. Reversing command-matching templates could eventually let suggestions complete configurations from a design.
Missing language features
- Ordered configuration lists such as route-maps currently require a lattice and recursive rules to recover order and walk the list.The authors propose mapping these objects to custom functions callable by the checker.Source: §7 · p. 6
- Axiom cannot yet reason about properties of embedded regular expressions that require inspecting the regex state machine, such as whether a filter drops every route containing AS 666.Concrete-string evaluation is straightforward, but answering this property requires inspecting the regex itself.Source: §7 · p. 6
Negative provenance and synthesis
- Negative provenance could explain a violated assertion by identifying missing facts, with a design narrowing explanations to intended mechanisms such as a missing iBGP session.The discussion contrasts this with NDlog, where a missing route can be forced by any configuration that produces it, including unintended mechanisms.Source: §7 · p. 6
- Reversing templates that match commands could turn missing facts into suggested commands, potentially completing a configuration from the design alone.The discussion frames negative provenance as the first step toward this synthesis.Source: §7 · p. 6