带流表项超时的软件定义网络模型检测（含附录版）
网络与互联网体系结构
2022-01-19 v2
摘要
软件定义网络（SDN）通过（虚拟）集中式可编程控制器实现网络部署的高级运行与管理，控制器通过在网络交换机的流表中安装规则来部署网络功能。尽管这是一个强大的抽象，控制器功能的缺陷可能导致严重的服务中断与安全漏洞，从而催生了寻找甚至验证无缺陷的（半）自动化工具需求。文献中已提出 SDN 的模型检测，但现有方法均无法支持流表项因超时而过期的动态网络部署。这对于自动刷新（并消除陈旧）网络状态（在网络协议设计术语中称为软状态）是必要的，而软状态对扩展应用或从故障中恢复十分重要。在本文中，我们扩展我们的模型（MoCS）以处理流表项的超时，从而支持网络中的软状态。我们提出了针对该扩展的优化。我们在 UPPAAL 中使用负载均衡器与防火墙在不同规模网络拓扑中评估了所提模型的性能。
引用
@article{arxiv.2008.06149,
title = {Model Checking Software-Defined Networks with Flow Entries that Time Out (version with appendix)},
author = {Vasileios Klimis and George Parisis and Bernhard Reus},
journal= {arXiv preprint arXiv:2008.06149},
year = {2022}
}