A (not) NICE way to verify the openflow switch specification: formal modelling of the openflow switch using alloy
A (not) NICE way to verify the openflow switch specification: formal modelling of the openflow switch using alloy
复制标题
验证开放流交换机规格的（不是）好方法：使用合金对开放流交换机进行形式化建模
DOI：
10.1145/2486001.2491711
复制
发表时间：
2013
期刊：
影响因子：
--
通讯作者：
Davide Proserpio
中科院分区：
文献类型：
--
作者：
Natali Ruchansky;Davide Proserpio
软件定义网络 (SDN) 的引入彻底改变了网络的构建和管理方式。 SDN 将数据与控制平面访问分离，这使得新网络功能的引入变得更加简单。 OpenFlow 的理念是走向集中化，其中单个控制器程序管理交换机的逻辑。虽然集中式系统通常更容易协调，但出现错误的可能性仍然很高。尽管存在 OpenFlow 规范 [3]，但在遵守该规范的同时仍有可能观察到意外行为。这可能是由于多种原因造成的，例如协议某些方面的规范不足或人为的事件序列。验证（证明系统满足其规范）标准和协议的新兴技术之一是形式建模。形式模型是在某些选定的抽象级别上创建的，其目的是实现对系统的精确理解、规范和分析。建模语言 Alloy 被认为是一种适合对复杂网络进行建模的工具。事实上，它已被用于许多应用中 [1]，包括对 Chord [6, 7] 的分析，这导致了一个反例证明该协议的不正确性。本文的主要贡献是将形式化建模的原理应用于 OpenFlow。具体来说，我们使用模型枚举（合金和合金分析器 [5]）来对支持 OpenFlow 的交换机进行建模。该项目的目标有两个：(1) 提供 OpenFlow Switch 规范版本 1.1.0 正确性（或不正确性）的证明；(2) 为研究人员提供完整的 OpenFlow Switch 模块，该模块可用作验证各种应用程序或网络类型的基础（更多详细信息请参见第 4 节和我们的网站 [2]）。本文的其余部分组织如下。在秒-
The introduction of Software Defined Networks (SDNs) is completely changing the way in which networks are built and managed. SDNs decouple data from control plane access, which makes introduction of new network functionalities significantly simpler. The philosophy of OpenFlow is a move towards centralization, where a single controller program manages the logic of switches. While centralized systems are often easier to coordinate, the likelihood of bugs is still high. Despite the existence of an OpenFlow Specification [3], it may still be possible observe unexpected behavior while adhering to this Specification. This can be due to various reasons, such as underspecification of some aspect of the protocol or a contrived sequence of events. One of the emerging techniques to verify (prove that a system satisfies its specification) standards and protocols is formal modeling. Created at some chosen level of abstraction, the purpose of a formal model is to enable precise understanding, specification, and analysis of the system. The modeling language Alloy has been noted as a tool that lends itself to modeling complex networks. In fact, it has been used in many applications [1], including the analysis of Chord [6, 7] which led to a counterexample proving the incorrectness of the protocol. The main contribution of this paper is to apply the principles of formal modeling to OpenFlow. Concretely we use model enumeration (Alloy and Alloy Analyzer [5]) to model an OpenFlow-capable switch. The aim of this project is twofold: (1) to provide a proof of correctness (or not) of the OpenFlow Switch Specification Version 1.1.0 and (2) provide researchers with a complete OpenFlow Switch module that can be used as a foundation to verify various applications or types of networks (more detail in Section 4 and our site [2]). The remainder of the paper is organized as follows. In Sec-