StacKAT: Infinite State Network Verification

TL;DR

StacKAT is a novel network verification language that incorporates stack operations, enabling modeling of complex network behaviors like parsing and routing, with a decision procedure for program equivalence.

Contribution

We introduce StacKAT, a new language for network verification with stack features, and develop a decision procedure and axiomatization for program equivalence.

Findings

Decidable program equivalence using finite automata

Complete axiomatization of StacKAT equivalence

Expresses complex network behaviors like parsing and routing

Abstract

We develop StacKAT, a network verification language featuring loops, finite state variables, nondeterminism, and - most importantly - access to a stack with accompanying push and pop operations. By viewing the variables and stack as the (parsed) headers and (to-be-parsed) contents of a network packet, StacKAT can express a wide range of network behaviors including parsing, source routing, and telemetry. These behaviors are difficult or impossible to model using existing languages like NetKAT. We develop a decision procedure for StacKAT program equivalence, based on finite automata. This decision procedure provides the theoretical basis for verifying network-wide properties and is able to provide counterexamples for inequivalent programs. Finally, we provide an axiomatization of StacKAT equivalence and establish its completeness.