Formalization and Verification of the OpenFlow Bundle Mechanism Using CSP

2018 ◽  
Vol 28 (11n12) ◽  
pp. 1657-1677
Author(s):  
Huiwen Wang ◽  
Huibiao Zhu ◽  
Lili Xiao ◽  
Yuan Fei

Software-Defined Networking (SDN) is an emerging architecture of computer networking. OpenFlow is considered as the first and currently most popular standard southbound interface of SDN. It is a communication protocol which enables the SDN controller to directly interact with the forwarding plane, which makes the network more flexible and programmable. The promising and widespread use makes the reliability of OpenFlow important. The OpenFlow bundle mechanism is a new mechanism proposed by OpenFlow protocol to guarantee the completeness and consistency of the messages transmitted between SDN devices like switches and controllers. In this paper, we use Communication Sequential Processes (CSP) to formally model the OpenFlow bundle mechanism. By adopting the models into the model checker Process Analysis Toolkit (PAT), we verify the relevant properties of the mechanism, including deadlock freeness, parallelism, atomicity, order property and schedulability. Our formalization and verification show that the mechanism can satisfy these properties, from which we can conclude that the mechanism offers a better way to guarantee the completeness and consistency.

Author(s):  
Sujitha S. ◽  
Manikandan M. S. K. ◽  
Ashwini G.

Designing and organizing networks has become extra innovative over the past few years with the assistance of SDN (software-defined networking). The software implements network protocols that undergo years of equivalence and interoperability testing. Software-defined networking (SDN) is a move toward computer networking that allows network administrators to programmatically initialize, manage, alter, and direct network behavior dynamically through open interfaces and abstraction of lower-level functionality. SDN controller is an application in software-defined networking (SDN) that manages run control to permit clever networking. SDN controllers are based on protocols, such as OpenFlow, that permit servers to inform switches where to send packets. This chapter explores SDN controllers.


IEEE Access ◽  
2019 ◽  
Vol 7 ◽  
pp. 46646-46658 ◽  
Author(s):  
Sikandar Ejaz ◽  
Zeshan Iqbal ◽  
Peer Azmat Shah ◽  
Bilal Haider Bukhari ◽  
Armughan Ali ◽  
...  

2021 ◽  
Vol 5 (1) ◽  
pp. 20-27
Author(s):  
Israa T. Aziz ◽  
Ihsan H. Abdulqadder

Cloud networks are being used in most industries and applications in the current era. Software-defined networking has come up as an alternative tool and mechanism to follow and implement in a cloud networking environment in place of the traditional networking approaches. This paper includes the security aspects of computer networking concerning the cloud networking environment and software-defined networks. The security risks and vulnerabilities have been listed and described in this work, and the measures that may be adapted to detect, prevent, and control the same. The use of figures, diagrams, and codes has been done as applicable.


2021 ◽  
Author(s):  
◽  
Benjamin Philip Palmer

<p>An increasing number of products are exclusively digital items, such as media files, licenses, services, or subscriptions. In many cases customers do not purchase these items directly from the originator of the product but through a reseller instead. Examples of some well known resellers include GoDaddy, the iTunes music store, and Amazon. This thesis considers the concept of provenance of digital items in reseller chains. Provenance is defined as the origin and ownership history of an item. In the context of digital items, the origin of the item refers to the supplier that created it and the ownership history establishes a chain of ownership from the supplier to the customer. While customers and suppliers are concerned with the provenance of the digital items, resellers will not want the details of the transactions they have taken part in made public. Resellers will require the provenance information to be anonymous and unlinkable to prevent third parties building up large amounts of information on the transactions of resellers. This thesis develops security mechanisms that provide customers and suppliers with assurances about the provenance of a digital item, even when the reseller is untrusted, while providing anonymity and unlinkability for resellers . The main contribution of this thesis is the design, development, and analysis of the tagged transaction protocol. A formal description of the problem and the security properties for anonymously providing provenance for digital items in reseller chains are defined. A thorough security analysis using proofs by contradiction shows the protocol fulfils the security requirements. This security analysis is supported by modelling the protocol and security requirements using Communicating Sequential Processes (CSP) and the Failures Divergences Refinement (FDR) model checker. An extended version of the tagged transaction protocol is also presented that provides revocable anonymity for resellers that try to conduct a cloning attack on the protocol. As well as an analysis of the security of the tagged transaction protocol, a performance analysis is conducted providing complexity results as well as empirical results from an implementation of the protocol.</p>


2017 ◽  
Vol 13 (8) ◽  
pp. 155014771772868 ◽  
Author(s):  
Tri-Hai Nguyen ◽  
Myungsik Yoo

The Internet of Things is a network of physical devices consisting of embedded systems and sensors that interact with each other and connect to the Internet, and the quick growth of the Internet of Things industry has resulted in complex inter-networking on the Internet. Software-defined networking is a recent advance in computer networking that redefines the network paradigm for future communication, and the advantages of software-defined networking can also be applied to Internet of Things, namely as software-defined Internet of Things. In this article, we investigate the vulnerability of the software-defined Internet of Things platform device manager, which monitors the connected Internet of Things devices in the network. Although being the one that performs one of the most crucial services, the device managers in current primary controllers have a big security issue as they do not include any device verification, authentication, or authorization routines. Consequently, the device manager accepts all the changes of device information made by other devices, which leads to potential attacks as demonstrated in this article. To address this problem, a comprehensive and lightweight countermeasure is proposed and its effectiveness is verified through experiments.


Author(s):  
Anurag Tiwari ◽  
Suneet Gupta

The idea of software-defined networking (SDN) is a paradigm shift in computer networking. There are various advantages of SDN (e.g., network automation, fostering innovation in network using software, minimizing the CAPEX and OPEX cost with minimizing the power consumption in the network). SDN is one of the recently developed network-driven methodologies where the core of all lower-level services is operated by one centralized device. Developers tried to develop such approaches to make it easy for an administrator to control information flow from one node to another node. To obtain these services, lower-level static architecture is decoupled for the higher level. This chapter introduces a new approach that is based on complex network processing and forecasting for an event.


2020 ◽  
Vol 35 ◽  
Author(s):  
Naipeng Dong ◽  
Guangdong Bai ◽  
Lung-Chen Huang ◽  
Edmund Kok Heng Lim ◽  
Jin Song Dong

Abstract Blockchain technology has rapidly emerged as a decentralized trusted network to replace the traditional centralized intermediator. Especially, the smart contracts that are based on blockchain allow users to define the agreed behaviour among them, the execution of which will be enforced by the smart contracts. Based on this, we propose a decentralized booking system that uses the blockchain as the intermediator between hoteliers and travellers. The system enjoys the trustworthiness of blockchain, improves efficiency and reduces the cost of the traditional booking agencies. The design of the system has been formally modelled using the CSP# language and verified using the model checker Process Analysis Toolkit. We have implemented a prototype decentralized booking system based on the Ethereum ecosystem.


A novel anomaly detection-based NIDS is main demand in the computer networking security for discriminating malicious software attack at the early stage. It monitors and analyzes network traffics, checking abnormal behaviors or attack signatures. The detection rate or accuracy is the prerequisite in the network intrusion detection models, also, developing adaptive and flexible model is a critical challenge regarding to unseen attack. This search paper included the deep neural network (DNN) as anomaly detection model can be used within software defined networking (SDN). Dropout technique is used to prevent DNN model from overfitting. Six features have information about the flow were chosen from NSL-KDD dataset to fit and evaluate this model, these data features could be matched to packet-in message header values, also, these features enable the model to be a good generative, and well perform on intrusion recognition issue with a subset of the data. Cross entropy loss function with SoftMax output layer were used for getting the differences between the two different distribution and mapping to multiple class classification covered five class labels, one is normal and the others are attacks (Dos, R2L, U2L and Probe). Accuracy is a comparative metric utilized for assessing the model performance. The results are promising, where accuracy achieved 92.65%.


2020 ◽  
Vol 12 (3) ◽  
pp. 49
Author(s):  
Abdelrahman Abuarqoub

Recent advances in information and communications cloud-based services hold the potential to overcome the scalability and complex maintenance limitations of traditional networks. Software Defined Networking (SDN) surfaced as a promising paradigm to mitigate such limitations while offering flexible networks management. Particularly, SDN separates the control plane from the data plane to achieve abstraction of lower-level functionality, hence, allowing more efficient network management and utilization. However, SDN suffers from various performance and scalability problems leading to significant research efforts on maximizing the scalability of the control plane. This paper aims at reviewing different SDN controller scalability, topology-based and mechanism-based approaches, as well as discussing and analyzing how they attempt to solve the scalability challenge. Furthermore, this paper elaborates on the promising research trends and challenges. Our insights are also discussed to stimulate further research efforts addressing the control plane scalability in SDN.


Sign in / Sign up

Export Citation Format

Share Document