KATch: A Fast Symbolic Verifier for NetKAT
arxiv(2024)
摘要
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 , 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.
更多查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要