专栏首页arxiv.org翻译专栏面向模型检验的真实软件定义网络(CS NI)
原创

面向模型检验的真实软件定义网络(CS NI)

在软件定义的网络(sdn)中,控制器程序负责跨大量交换机部署不同的网络功能,但这样做的风险很大: 部署有缺陷的控制器代码可能导致网络和服务中断和安全漏洞。 因此,自动检测 bug,或者更好的是,验证缺陷是最理想的,然而,网络的规模和控制器的复杂性,使这成为一项具有挑战性的任务。 在这篇论文中,我们提出了 mocs,一个高度表达能力的优化 sdn 模型,它允许在合理的时间内捕获微妙的现实世界中的 bug。 这是通过(1)分析模型可能的部分顺序削减,(2)静态预计算包等价类和(3)索引数据包和规则存在的模型。 我们通过在不同规模的网络拓扑结构上运行例子,提供了 mocs 在 uppaal 中的原型实现所捕获的实际错误,以及性能 / 可伸缩性的例子,并强调了抽象和优化的重要性,从而证明了它在表达能力方面相对于现有技术的优势。

原文题目:Towards Model Checking Real-World Software-Defined Networks

原文:In software-defined networks (SDN) a controller program is in charge of deploying diverse network functionality across a large number of switches, but this comes at a great risk: deploying buggy controller code could result in network and service disruption and security loopholes. The automatic detection of bugs or, even better, verification of their absence is thus most desirable, yet the size of the network and the complexity of the controller makes this a challenging undertaking. In this paper we propose MOCS, a highly expressive, optimised SDN model that allows capturing subtle real-world bugs, in a reasonable amount of time. This is achieved by (1) analysing the model for possible partial order reductions, (2) statically pre-computing packet equivalence classes and (3) indexing packets and rules that exist in the model. We demonstrate its superiority compared to the state of the art in terms of expressivity, by providing examples of realistic bugs that a prototype implementation of MOCS in UPPAAL caught, and performance/scalability, by running examples on various sizes of network topologies, highlighting the importance of our abstractions and optimisations.

原文作者: Vasileios Klimis

原文地址:https://arxiv.org/abs/2004.11988

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 识别在公共交通系统中传播疾病的有传染性的旅行者(CS SI)

    最近一种新型冠状病毒的爆发及其迅速传播突出了了解人类流动性的重要性。 密闭空间,例如公共交通工具(例如巴士及火车) ,提供适当的环境让感染迅速广泛传播。因此,调...

    用户7095611
  • 行为变化及其对人气提升的影响: 从精英到微博上的大众(CS SI)

    社交媒体在生产和消费信息方面的繁荣意味着在线用户影响力在决定内容流行度方面的关键作用。 特别是,了解有影响力的精英与大众基层之间的行为差异是沟通中的一个重要问题...

    用户7095611
  • 标度指数与标准差比关系的推导(CS LG)

    异速生长规律是理解城市演化的基本规律之一。这个定律的一般形式是异速缩放定律。然而,标度指数的深层含义和基本原理仍有待揭示。本文运用线性代数和回归分析理论,揭示了...

    用户7095611
  • 面向模型检验的真实软件定义网络(CS NI)

    在软件定义网络(SDN)中,控制器程序负责在大量交换机上部署不同的网络功能,但这会带来很大的风险:如果部署了错误的控制器代码可能会导致网络和服务中断以及安全漏洞...

    Elva
  • 敏捷软件开发的文献计量分析(CS SE)

    敏捷方法目前被认为是软件开发的主要范例之一。从科学的角度来看,它的研究近年来受到软件工程相关科学界的重视。本研究旨在对与该领域最相关研究的数量、特点和范围进行文...

    Elva
  • 【论文推荐】最新八篇网络节点表示相关论文—可扩展嵌入、对抗自编码器、图划分、异构信息、显式矩阵分解、深度高斯、图、随机游走

    【导读】专知内容组整理了最近八篇网络节点表示(Network Embedding)相关文章,为大家进行介绍,欢迎查看! 1.SIGNet: Scalable E...

    WZEARW
  • 【世界读书日】2018版十大引用数最高的深度学习论文集合

    量化投资与机器学习微信公众号
  • 高级知识评估:基于结果分析,重新设计基于药学专业的网络考试(CS CAS)

    各地信息技术的使用导致对新的教育方式有需求。现代化的电子学习环境将学生的学习知识和技能的教学,学习和评估带入了一个新时代,且考虑到学生的电子学习动机。高等数学课...

    时代在召唤
  • 在存在累计前景博弈者的博弈论下的黑盒策略与平衡(cs.GT)

    偏好关系的中间属性规定了两个彩票的可能性混合应该在这两个彩票的偏好之间。它是独立属性的一种弱化形式,并且因此满足于期望效应理论(EUT)。实验中对于中间属性的违...

    Donuts_choco
  • 基于可见性约束的推理障碍与路径有效性(CS RO)

    许多从演示中学习的方法都假设演示者了解整个环境。然而,在许多场景中,演示者只看到环境的一部分,他们在收集信息时不断地重新规划。为了规划新的路径或重建环境,我们必...

    时代在召唤

扫码关注云+社区

领取腾讯云代金券