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.


翻译:在现代网络中,包裹的传送往往取决于先前传送的交通的历史。这些网络含有有声势的中继箱,其转发行为取决于可变的内部状态。 防火墙和负载平衡器是典型的有声势的中继箱。 这项工作解决了在与有限状态中继箱的网络中核查安全性质的复杂性, 如隔离等。 不幸的是, 我们显示, 即使没有转发环, 有关这些网络的推理也难以确定, 原因是中继箱之间通过无线定线的频道连接了互动。 因此, 我们抽象地发出频道命令。 这种抽象性能对于安全来说是健全的, 使得问题可以破解。 具体地说, 安全检查在网络中的主机和中继箱数量中成为 EXPSPACE 。 要解决高度复杂的问题, 我们确定两个有用的中继箱子类, 承认比较复杂的。 最简单的类别包括, 例如防火墙和允许多盘时间核查。 第二类包括, 比如, 缓存服务器和学习交换器, 并且使安全问题变得可以完成。 最后, 我们实施一个工具来核查正确性网络。

0
下载
关闭预览

相关内容

Networking:IFIP International Conferences on Networking。 Explanation:国际网络会议。 Publisher:IFIP。 SIT: http://dblp.uni-trier.de/db/conf/networking/index.html
【Cell】神经算法推理,Neural algorithmic reasoning
专知会员服务
28+阅读 · 2021年7月16日
开源书:PyTorch深度学习起步
专知会员服务
50+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
机器学习在材料科学中的应用综述,21页pdf
专知会员服务
48+阅读 · 2019年9月24日
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
已删除
将门创投
9+阅读 · 2018年12月19日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Highway Networks For Sentence Classification
哈工大SCIR
4+阅读 · 2017年9月30日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年7月26日
Arxiv
13+阅读 · 2021年5月25日
Arxiv
5+阅读 · 2020年3月16日
Arxiv
3+阅读 · 2018年8月17日
VIP会员
相关资讯
Transferring Knowledge across Learning Processes
CreateAMind
28+阅读 · 2019年5月18日
计算机 | 中低难度国际会议信息6条
Call4Papers
7+阅读 · 2019年5月16日
动物脑的好奇心和强化学习的好奇心
CreateAMind
10+阅读 · 2019年1月26日
逆强化学习-学习人先验的动机
CreateAMind
15+阅读 · 2019年1月18日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
已删除
将门创投
9+阅读 · 2018年12月19日
可解释的CNN
CreateAMind
17+阅读 · 2017年10月5日
Highway Networks For Sentence Classification
哈工大SCIR
4+阅读 · 2017年9月30日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Top
微信扫码咨询专知VIP会员