迈向模型检测真实世界软件定义网络（含附录版）
网络与互联网体系结构
2020-07-21 v5
摘要
在软件定义网络（SDN）中，控制器程序负责在大量交换机上部署多样化的网络功能，但这带来了巨大风险：部署有缺陷的控制器代码可能导致网络与服务中断以及安全漏洞。因此，自动检测缺陷或更好地验证其不存在是极为可取的，然而网络规模与控制器复杂性使此举颇具挑战。本文中我们提出 MOCS，一种高表达力、优化的 SDN 模型，可在合理时间内捕获微妙的真实世界缺陷。这通过以下方式实现：（1）分析模型以寻求可能的偏序归约；（2）静态预计算包等价类；（3）对模型中存在的包与规则建立索引。我们通过提供 MOCS 在 UPPAAL 中的原型实现所捕获的现实缺陷示例，以及在不同规模网络拓扑上运行示例以凸显我们抽象与优化的重要性，展示了其在表达力上相对于现有技术的优越性，以及在性能/可扩展性上的优越性。
引用
@article{arxiv.2004.11988,
title = {Towards Model Checking Real-World Software-Defined Networks (version with appendix)},
author = {Vasileios Klimis and George Parisis and Bernhard Reus},
journal= {arXiv preprint arXiv:2004.11988},
year = {2020}
}