The Remaining Improbable: Toward Verifiable Network Services
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.
Cite
@article{arxiv.2009.12861,
title = {The Remaining Improbable: Toward Verifiable Network Services},
author = {Pamela Zave and Jennifer Rexford and John Sonchack},
journal= {arXiv preprint arXiv:2009.12861},
year = {2020}
}
Comments
6 pages with 4 figures, plus references. This paper has been reviewed extensively as a conference submission. Although some reviewers have found it cryptic due to its length (small) and scope (large), we are satisfied that it contains no factual errors. We welcome your questions!