一句话：为 NetKAT 网络规约语言设计新的符号自动机数据结构与算法，实现快速可扩展的等价性验证工具 KATch。
NetKAT 是描述网络数据平面行为的领域特定语言，但其验证查询在规模上难以高效求解。本文扩展符号自动机技术，提出新的数据结构与算法以高效检查 NetKAT 验证查询。作者用 Scala 实现了工具 KATch，支持一组扩展的 NetKAT 算子以表达全网规约，其验证引擎通过构造 bisimulation 证明等价，或生成反例。在真实与合成基准上，KATch 通常能在远小于一秒内完成可达性、切片隔离等验证，比此前方法快若干数量级，展示了 NetKAT 作为实用声明式网络规约与验证语言的潜力。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{MoellerJBDSSFS24,
title = {KATch: A Fast Symbolic Verifier for NetKAT},
author = {Mark Moeller and Jules Jacobs and Olivier Savary Belanger and David Darais and Cole Schlesinger and Steffen Smolka and Nate Foster and Alexandra Silva},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {PLDI},
year = {2024},
doi = {10.1145/3656454}
}