The Remaining Improbable: Toward Verifiable Network Services
Pamela Zave, Jennifer Rexford, John Sonchack

TL;DR
This paper advocates for a layered, compositional network architecture to enhance the verifiability of network services, demonstrating its implementation and benefits for reasoning about complex properties.
Contribution
It introduces a modular, layered architecture for verifiable network services and provides a prototype implementation using P4 code for programmable data planes.
Findings
Modular architecture enables reasoning about complex network properties.
Prototype demonstrates practical implementation in programmable data planes.
Supports automated verification of network service properties.
Abstract
The trustworthiness of modern networked services is too important to leave to chance. We need to design these services with specific properties in mind, and verify that the properties hold. In this paper, we argue that a compositional network architecture, based on a notion of layering where each layer is its own complete network customized for a specific purpose, is the only plausible approach to making network services verifiable. Realistic examples show how to use the architecture to reason about sophisticated network properties in a modular way. We also describe a prototype in which the basic structures of the architectural model are implemented in efficient P4 code for programmable data planes, then explain how this scaffolding fits into an integrated process of specification, code generation, implementation of additional network functions, and automated verification.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSoftware-Defined Networks and 5G · Distributed systems and fault tolerance · Security and Verification in Computing
