验证存在中间件时的隔离属性
网络与互联网体系结构
2014-09-30 v1 计算机科学中的逻辑
摘要
最近在验证路由器转发表的正确性方面取得了巨大进展。然而，这些方法不适用于包含中间件（如缓存和防火墙）的网络，因为这些设备的转发行为取决于先前观察到的流量。我们探讨了如何使用模型检查来验证包含此类“动态数据路径”元件的网络中的隔离属性。我们的工作利用了 SMT 求解器的最新进展，主要挑战在于扩展该方法以处理大型且复杂的网络。虽然将模型检查直接应用于此问题只能处理非常小的网络（如果有的话），但我们的方法可以在几分钟内验证包含 30,000 个中间件的网络上的简单现实不变量。
引用
@article{arxiv.1409.7687,
title = {Verifying Isolation Properties in the Presence of Middleboxes},
author = {Aurojit Panda and Ori Lahav and Katerina Argyraki and Mooly Sagiv and Scott Shenker},
journal= {arXiv preprint arXiv:1409.7687},
year = {2014}
}
备注
Under submission to NSDI