Modeling and Verifying OpenFlow Scheduled Bundle Mechanism Using CSP

Huiwen Wang, Huibiao Zhu, Lili Xiao, Wanling Xie, Gang Lu

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

3 Scopus citations

Abstract

OpenFlow is considered as one of the first standard of software defined networking (SDN). The OpenFlow scheduled bundle mechanism is a latest mechanism proposed in OpenFlow protocol to guarantee the completeness and consistency of messages transimitted between SDN switches and controllers during the communication process. Due to the requirement of reliability and security, it is of great significance to formally analyze and verify the mechanism. In this paper, we apply Communication Sequential Processes (CSP) and use the model checker Process Analysis ToolKit (PAT) to model and verify the OpenFlow scheduled bundle mechanism. We verify the main property of the mechanism, schedulability. In addition, we analyze and verify the security of the mechanism and find that it suffers from some kinds of possible attacks.

Original languageEnglish
Title of host publicationProceedings - 2018 IEEE 42nd Annual Computer Software and Applications Conference, COMPSAC 2018
EditorsClaudio Demartini, Sorel Reisman, Ling Liu, Edmundo Tovar, Hiroki Takakura, Ji-Jiang Yang, Chung-Horng Lung, Sheikh Iqbal Ahamed, Kamrul Hasan, Thomas Conte, Motonori Nakamura, Zhiyong Zhang, Toyokazu Akiyama, William Claycomb, Stelvio Cimato
PublisherIEEE Computer Society
Pages376-381
Number of pages6
ISBN (Electronic)9781538626665
DOIs
StatePublished - 8 Jun 2018
Event42nd IEEE Computer Software and Applications Conference, COMPSAC 2018 - Tokyo, Japan
Duration: 23 Jul 201827 Jul 2018

Publication series

NameProceedings - International Computer Software and Applications Conference
Volume2
ISSN (Print)0730-3157

Conference

Conference42nd IEEE Computer Software and Applications Conference, COMPSAC 2018
Country/TerritoryJapan
CityTokyo
Period23/07/1827/07/18

Keywords

  • Modeling
  • Scheduled Bundle
  • Security
  • Software Defined Networking
  • Verifying

Fingerprint

Dive into the research topics of 'Modeling and Verifying OpenFlow Scheduled Bundle Mechanism Using CSP'. Together they form a unique fingerprint.

Cite this