论文标题
剩下的不可能：迈向可验证的网络服务
The Remaining Improbable: Toward Verifiable Network Services
论文作者
论文摘要
现代网络服务的可信赖性太重要了，无法偶然。我们需要牢记特定属性设计这些服务，并验证该属性是否拥有。在本文中，我们认为，基于分层的概念，每个层都是为特定目的定制的完整网络，是使网络服务可验证的唯一合理方法。现实的示例显示了如何使用体系结构以模块化的方式推理有关复杂网络属性的原因。我们还描述了一个原型，在该原型中，在有效的P4代码中为可编程数据平面实现架构模型的基本结构，然后解释该脚手架如何拟合到集成的规范过程中，代码生成，实现其他网络功能以及自动验证。
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.
