Axiom: a logic programming language to express and enforce network designs

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.