MatchKAT: An Algebraic Foundation For Match-Action

TL;DR

MatchKAT introduces an algebraic framework for formal reasoning about match-action packet processing in network switches, providing a foundation for verifying network programs.

Contribution

It presents the first formal algebraic semantics for match-action rules, including a sound and complete equational theory and complexity analysis.

Findings

MatchKAT's equational theory is sound and complete.

Deciding equivalence in MatchKAT is PSPACE-complete.

Provides a formal basis for reasoning about network switch programs.

Abstract

We present MatchKAT, an algebraic language for modeling match-action packet processing in network switches. Although the match-action paradigm has remained a popular low-level programming model for specifying packet forwarding behavior, little has been done towards giving it formal semantics. With MatchKAT, we hope to embark on the first steps in exploring how network programs compiled to match-action rules can be reasoned about formally in a reliable, algebraic way. In this paper, we give details of MatchKAT and its metatheory, as well as a formal treatment of match expressions on binary strings that form the basis of "match" in match-action. Through a correspondence with NetKAT, we show that MatchKAT's equational theory is sound and complete with regards to a similar packet filtering semantics. We also demonstrate the complexity of deciding equivalence in MatchKAT is PSPACE-complete.