Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userReachability Specification in (SDN) by TLA+
توصيف الوصولية في شبكة (SDN) باستخدام TLA+
905
0 61
0
(
0
)
Created by
Shamra Editor
Ask ChatGPT about the research
في هذا البحث تم توصيف الشبكة بواسط الجبر المنطقي و ذلك لكي يتم فرز الرزم إلى مجموعتين تتضمن الرزم التي ستصل إلى الهدف و الرزم التي سيتم سحبها وفق حالة الشبكة و جداول التدفق, تم كتاب التوصيف باستخدام لغة TLA+ التي تعتمد على الجبر المنطقي الأولي و تم فحص النموذج بواسطة أداة TLCحيث تساعد هذه الطريقه على عملية التحقق المسبق (Proactive verification) لتعريفات الشبكة و التأكد من أنها تتعارض مع السياسة الأمنيه العامه.
In this paper the network specification by logic algebra is presented then the packets are classified into reachable packets and dropped packets according to the current state of the network and flow tables of switches. The model specification is written by TLA+ language which is built on First Order Logic (FOL), and the specification is checked by TLC. This model will help the programmers to detect the network in proactive verification and prove that this configuration meets the global policy of the network.
References used
AL-SHAER, E, & AL-HAJ, S, 2010 - FlowChecker: Configuration Analysis and Verification of Federated OpenFlow Infrastructures. In Proceedings of the 3rd ACM Workshop on Assurable and Usable Security Configuration,ACM PP: 37–44
BALL, T, & BJØRNER, N, & GEMBER, A, & ITZHAKY, S, 2014 - VeriCon: Towards Verifying Controller Programs in Software-Defined Networks. ACM, PP. 1-12
BAIER, C, & KATOEN, J 2007 - Principles of Model Checking. The MIT Press Cambridge, Massachusetts, England, May. (992)P
rate research
Read More
In this paper we introduce a specification model for the host migration
process in Software Defined Network, and for verifying the reachability
property for packets that do not change after the migration, and achieve
the required modifications to
meet the same properties.
The model is designed by TLA+ language and verified by TLC which is
correlated with it. The model is implemented by few states to meet the
required property.
The mapping of Layer 3 (IP) to Layer 2 (MAC) addresses is a key service in IP networks, and is achieved via the Address Resolution Protocol (ARP) protocol in IPv4. Due to its stateless nature and lake of authentication, ARP is an easy goal to spoofin
g attacks, which can enable Denial of Service (DoS) or Man-in-the-Middle (MIM) attacks. In this search, we discuss the problem of ARP spoofing in the context of Software Defined Networks (SDNs). We studied important parameters such as throughput, delay and the availability of the network. Results showed that ARP spoofing attacks was able to make a negative effects on network performance
Software defined networks SDN is one of the most influential types of networks in information and communication technology compared to all traditional network technologies where there are many challenges, SDN is one of the most promising solutions fo
r the Internet in the future and provides a strong network infrastructure with high specifications and low cost, and represents the future of the next generation of network engineering due to the easy division of networks, programming, monitoring, control and management through a central control, and the separation of control plane from the data-forwarding plane in SDN networks facilitates the process of managing and developing networks, as this technology is currently used in data centers and wireless networks, and is a solution to many of the problems faced by traditional networks. SDN networks are characterized by sufficient dynamism to deal with the different conditions of the network, and the controller is one of its most important components and is considered the smartest component in the network, and given the importance of choosing the appropriate controller according to the different parameters and conditions of the SDN network,in this research we conducted an analysis of the characteristics of Software defined Networks, The analysis relied on comparing SDN networks with the presence of a single OpenDaylight controller (ODL) and the presence of several controllers ODL, OpenDaylight controller was chosen as one of the famous controllers and it is distinguished from others as an open source and contains a distributed datastore and is designed to suit the data center environment, Taking into account the OpenFlow protocol supported on the southern interface by this controller, the research includes simulations of software defined networks topologies using the Mininet emulator, and various scenarios and parameters such as data rate, packet delay, and throughput were analyzed by the D-ITG tool.
Current traditional IP networks start to be complex as the demands of the users are ever-growing. Software Defined Network (SDN) is a new paradigm to ease the management of the network and make the network programmable by decoupling the control plane
and forwarding plane (such as switch and router). A centralized controller is used to manage the control plane, and it interacts with the forwarding plane using a standardized OpenFlow protocol. However, many controllers are used recently such as POX, Ryu, ONOS, and OpenDaylight. The important question is which is the best controller to use in our network and fits our network’s goals? To answer this question, a decision-making method is proposed in this paper. First, four SDN controllers are selected, and five criteria are analyzed to collect these controllers’ properties. Then a Multi-Criteria Decision Making method named TOPSIS is used to rank the controllers and choose the best one. By applying this method, a comparative study is done to evaluate the four controllers in an environment of LAN topology, and “Ryu” controller is selected as the best one based on our criteria.
ASON\GMPLS based optical network technology has shown high reliability recently, but the issue of unified control of optical networks has become an urgent necessity to cover problems caused by separate control between different optical network layers
. The attempt to implement GMPLS-based standardized control of Internet Protocol / Dense Wavelength Division Multiplexing (IP/DWDM) networks has yielded satisfactory results but reflected significant complexity when operating in real time. On the other hand, the OpenFlow control level is offered as a promising solution to be a uniform control level for such networks, but it is not yet effective enough to control optical switch nodes. Therefore, as an intermediate step towards a unified UCP level entirely based on the OpenFlow protocol, the logical thinking for the time being is to introduce an OpenFlow/GMPLS interoperability control level that uses GMPLS to control the optical layer and the dynamic coordination between the IP layer and the optical layers. This research presents a practical application of interoperability solutions (parallel, overlapping, and integrated) for GMPLS and OpenFlow control levels applied to the ASON optical network installed in the southern region of Syria. The results have shown that the integrated solution for uniform control is superior to parallel and overlapping solutions in terms of the overall path provision latency (OPPL), at the expense of the high complexity of the design and processing of the load within the controller.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
