Static Differential Program Analysis for Software-Defined Networks
Static Differential Program Analysis for Software-Defined Networks
复制标题
软件定义网络的静态差分程序分析
DOI：
10.1007/978-3-319-19249-9_25
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
S. Krishnamurthi
中科院分区：
文献类型：
--
作者：
Tim Nelson;Andrew D. Ferguson;S. Krishnamurthi
网络越来越多地由软件控制，糟糕的更新可能会导致整个网络瘫痪。因此，网络运营商需要工具来确定变化的影响。为了解决这个问题，我们提出了软件定义网络(SDN)控制器程序的静态差分分析。给定控制器程序的两个版本，我们的工具Chimp构建在合金之上，以产生程序行为不同的一组具体场景。因此，CHIMP使网络开发人员能够利用形式化方法工具的力量，而不必接受形式逻辑或属性启发方面的培训。此外，我们还展示了许多有趣的属性，您可以对这些更改本身进行说明。我们的评估表明，Chimp速度很快，在几个实际应用程序上返回场景的时间不到一秒。
Networks are increasingly controlled by software, and bad updates can bring down an entire network. Network operators therefore need tools to determine the impact of changes. To address this, we present static differential analysis of software-defined network (SDN) controller programs. Given two versions of a controller program our tool, Chimp, builds atop Alloy to produce a set of concrete scenarios where the programs differ in their behavior. Chimp thus enables network developers to exploit the power of formal methods tools without having to be trained in formal logic or property elicitation. Furthermore, we show that there are many interesting properties that one can state about the changes themselves. Our evaluation shows that Chimp is fast, returning scenarios in under a second on several real applications.