基于模型检测的OpenFlow多交换机数据包转发协议的分析与验证.pdf

第43卷 第 10期 计 算 机 科 学 Vo1．43No．10 2016年 1O月 Computer Science Oct2016 基于模型检测的OpenFlow多交换机数据包转发 协议的分析与验证 朱 革 曾国荪 丁春玲。 王 伟 (同济大学计算机科学及技术系 上海201804) (高效能服务器和存储技术国家重点实验室 济南25O1O1) (同济大学化学系 上海 201804)。 摘 要 OpenFlow协议是 SDN 网络中控制平面与数据转发平面之间进行交互的规范与标准，其正确性将直接影响 到整个 网络功能的实现 。通过模型检测技术实现一种验证 OpenFlow协议 正确性的形式化方法 。首先提取 Open— Flow协议 的核心子协议 ，即OpenFlow 多交换机数据包转发协议作为验证的实例 ；然后运用协议行为 自动机对该子 协议进行形式化建模 ，并且通过时态逻辑描述协议需要进行验证的性质；最后给出算法验证协议模型是否满足给定的 性质要求，以此检测OpenFlow协议是否存在正确性漏洞，以便对其进行修正。 关键词 OpenFlow协议，模型检测，协议行为 自动机，时态逻辑 中图法分类号 TP391 文献标识码 A DOI 10．11896／j．issn．1002—137)(．2016．10．014 AnalysisandVerificationforOpenFlow Multi—switchProtocolBasedonModelChecking ZHU Ge， ZENG Guo-sun DING Chun-ling。 WANG Wei (DepartmentofComputerScienceandTechnology，TonNiUniversity，Shanghai201804，China) (StateKeyLaboratoryofHigh—endServer＆ StorageTechnology．Jinan250101，China)。 (DepartmentofChemistry，Ton~iUniversity，Shanghai201804，China)。 Abstraet Insoftwaredefinednetworking(SDN)，OpenFlow protocoliSthecommunicationstandardbetweenthecon— trolplaneandforwardingplane．Itsvalidityandrationalitywillinfluencetheperformanceofthewholenetwork．This paperfocusedonaformalmethodtOverifythecorrectnessoftheOpenFlow protocolbymodelchecking．Firstly，akey protocolcalledOpenFlow multi-switchprotocolwasproposed，whichisregardedasanimportantexample．Then，abasic modelforthisprotocolisbuiltbyprotocolactionautomatamachine．Thetemporarylogicisusedc0describesomemajor propertiesthatthisprotocolhas．A modelcheckingalgorithm isgiventoverifytheseproperties．Finally，thespeciala— nalysisandverificationforOpenFlowmulti-switchprotocolarecondu