  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.
