Scalable Testing of Context-Dependent Policies over Stateful Data Planes with Armstrong

TL;DR

Armstrong is a system that enables scalable testing of context-dependent policies in networks with stateful data planes, overcoming expressiveness and scalability limitations of existing verification tools.

Contribution

It introduces an abstract I/O model, a finite state machine abstraction for complex network functions, and scalable symbolic execution techniques.

Findings

Armstrong is several orders of magnitude faster than existing mechanisms.

It effectively models context-dependent policies in stateful networks.

The system handles complex network functions with improved scalability.

Abstract

Network operators today spend significant manual effort in ensuring and checking that the network meets their intended policies. While recent work in network verification has made giant strides to reduce this effort, they focus on simple reachability properties and cannot handle context-dependent policies (e.g., how many connections has a host spawned) that operators realize using stateful network functions (NFs). Together, these introduce new expressiveness and scalability challenges that fall outside the scope of existing network verification mechanisms. To address these challenges, we present Armstrong, a system that enables operators to test if network with stateful data plane elements correctly implements a given context-dependent policy. Our design makes three key contributions to address expressiveness and scalability: (1) An abstract I/O unit for modeling network I/O that encodes policy-relevant context information; (2) A practical representation of complex NFs via an ensemble of finite state machines abstraction; and (3) A scalable application of symbolic execution to tackle state space explosion. We demonstrate that Armstrong is several orders of magnitude faster than existing mechanisms.