We develop new data structures and algorithms for checking verification queries in NetKAT, a domain-specific language for specifying the behavior of network data planes. Our results extend the techniques obtained in prior work on symbolic automata and provide a framework for building efficient and scalable verification tools. We present KATch, an implementation of these ideas in Scala, featuring an extended set of NetKAT operators that are useful for expressing network-wide specifications, and a verification engine that constructs a bisimulation or generates a counter-example showing that none exists. We evaluate the performance of our implementation on real-world and synthetic benchmarks, verifying properties such as reachability and slice isolation, typically returning a result in well under a second, which is orders of magnitude faster than previous approaches. Our advancements underscore NetKAT's potential as a practical, declarative language for network specification and verification.

翻译：我们针对NetKAT（一种用于指定网络数据平面行为的领域特定语言）开发了新的数据结构和算法，以检验验证查询。我们的研究成果扩展了先前在符号自动机工作中获得的技术，并为构建高效可扩展的验证工具提供了一个框架。我们提出了KATch——这些思想在Scala中的实现，其特点包括：一套扩展的NetKAT运算符集（有助于表达网络范围的规范），以及一个验证引擎（该引擎可构建双模拟关系，或在不存在双模拟时生成反例）。我们在真实场景和合成基准测试中评估了实现的性能，验证了可达性和切片隔离等属性，通常在远少于一秒的时间内返回结果，这比以往方法快数个数量级。我们的进展凸显了NetKAT作为一种实用声明式语言在网络规范与验证方面的潜力。