有状态网络验证的一些复杂性结果
Some Complexity Results for Stateful Network Verification
摘要：
在现代网络中，数据包的转发通常取决于先前传输的流量的历史。这样的网络包含有状态的中间盒，其转发行为取决于可变的内部状态。防火墙和负载均衡器是有状态中间盒的典型例子。这项工作解决了在具有有限状态中间盒的网络中验证安全属性（如隔离）的复杂性。不幸的是，我们表明，即使在没有转发循环，推理这样的网络是不可判定的，由于连接的无界有序通道的中间盒之间的相互作用。因此，我们抽象出通道排序。这种抽象对于安全性来说是合理的，并且使得问题是可判定的。具体而言，安全检查在网络中的主机和中间盒的数量中变得EXPSPACE完全。为了解决高复杂性，我们确定了两个有用的子类有限状态中间盒承认更好的复杂性。最简单的类包括，例如，防火墙，并允许多项式时间验证。第二类包括，例如，缓存服务器和学习交换机，并使安全问题的coNP完全。最后，我们实现了一个工具，用于验证有状态网络的正确性。
英文摘要：
In modern networks, forwarding of packets often depends on the history of previously transmitted traffic. Such networks contain stateful middleboxes, whose forwarding behaviour depends on a mutable internal state. Firewalls and load balancers are typical examples of stateful middleboxes. This work addresses the complexity of verifying safety properties, such as isolation, in networks with finite-state middleboxes. Unfortunately, we show that even in the absence of forwarding loops, reasoning about such networks is undecidable due to interactions between middleboxes connected by unbounded ordered channels. We therefore abstract away channel ordering. This abstraction is sound for safety, and makes the problem decidable. Specifically, safety checking becomes EXPSPACE-complete in the number of hosts and middleboxes in the network. To tackle the high complexity, we identify two useful subclasses of finite-state middleboxes which admit better complexities. The simplest class includes, e.g., firewalls and permits polynomial-time verification. The second class includes, e.g., cache servers and learning switches, and makes the safety problem coNP-complete. Finally, we implement a tool for verifying the correctness of stateful networks.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
