StacKAT: Infinite State Network Verification

Proceedings of the ACM on Programming Languages, vol. 9, pp. 277–300

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.

Authors 7

1. Jules Jacobs

   Cornell University

   Affiliation as printed

   Cornell University, Ithaca, USA

2. Nate Foster

   Cornell University

   Affiliation as printed

   Cornell University, Ithaca, USA

3. Tobias Kappé Aachen

   Leiden University

   Affiliation as printed

   Leiden University, Leiden, Netherlands

4. Dexter C. Kozen

   Cornell University

   Affiliation as printed

   Cornell University, Ithaca, USA

5. Lily Saada

   Cornell University

   Affiliation as printed

   Cornell University, Ithaca, USA

6. Alexandra Silva

   Cornell University

   Affiliation as printed

   Cornell University, Ithaca, USA

7. Jana Wagemaker

   Radboud University Nijmegen

   Affiliation as printed

   Radboud University, Nijmegen, Netherlands