The Remaining Improbable: Toward Verifiable Network Services

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.