Project Overview

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.

Contributors

Pamela Zave

Relevant Links

The remaining improbable: Toward verifiable network services Paper