Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userReachability Specification in (SDN) by TLA+
توصيف الوصولية في شبكة (SDN) باستخدام TLA+
1073
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.
Artificial intelligence review:
Research summary
تستقطب الشبكات المعرفة بالبرمجة (SDN) اهتمام الباحثين نظرًا لقدرتها على فصل طرق تسليم البيانات عن طرق التحكم بالشبكة، مما يتيح إمكانية البرمجة بواسطة جبر المنطق. في هذا البحث، تم توصيف الشبكة باستخدام الجبر المنطقي لتصنيف الرزم إلى مجموعتين: الرزم التي ستصل إلى الهدف والرزم التي سيتم سحبها وفق حالة الشبكة وجداول التدفق. تم كتابة التوصيف باستخدام لغة +TLA وفحص النموذج بواسطة أداة TLC، مما يساعد على التحقق المسبق من تعريفات الشبكة والتأكد من عدم تعارضها مع السياسة الأمنية العامة. يهدف البحث إلى الاستفادة من التوصيف الصوري لتحليل شبكة SDN واكتشاف التغرات في تعريفات الشبكة، مع التركيز على تحديد سياسات تعريف المبدلات، حالة الشبكة، صحة السياسة الأمنية، وتصنيف الرزم. تم اختبار النموذج على سيناريوهات مختلفة للتأكد من صحة الوصولية وتوافقها مع السياسة الأمنية الموضوعة، وأثبتت النتائج فعالية النموذج في تحقيق الأهداف المرجوة.
Critical review
دراسة نقدية: يعتبر هذا البحث خطوة مهمة في مجال التحقق الصوري للشبكات المعرفة بالبرمجة، حيث يقدم نموذجًا دقيقًا لتحليل الشبكة باستخدام لغة +TLA. ومع ذلك، يمكن توجيه بعض النقد البناء لتحسين البحث. أولاً، قد يكون من المفيد توسيع نطاق الاختبارات لتشمل شبكات أكبر وأكثر تعقيدًا لضمان فعالية النموذج في بيئات متنوعة. ثانيًا، يمكن تحسين توثيق البحث لتوضيح بعض النقاط التقنية بشكل أكبر، مما يسهل على الباحثين الآخرين فهم وتطبيق النموذج. أخيرًا، يمكن النظر في دمج تقنيات أخرى للتحقق الصوري لتعزيز دقة وفعالية النموذج.
Questions related to the research
-
ما هي الفائدة الرئيسية من استخدام لغة +TLA في توصيف الشبكات المعرفة بالبرمجة؟
الفائدة الرئيسية هي أنها تتيح توصيفًا دقيقًا للنماذج باستخدام الجبر المنطقي، مما يسهل عملية التحقق الصوري واكتشاف الأخطاء في تعريفات الشبكة.
-
كيف تم تصنيف الرزم في هذا البحث؟
تم تصنيف الرزم إلى مجموعتين: الرزم التي ستصل إلى الهدف والرزم التي سيتم سحبها، وذلك وفق حالة الشبكة وجداول التدفق.
-
ما هي الأداة المستخدمة لفحص النموذج في هذا البحث؟
تم استخدام أداة TLC لفحص النموذج المكتوب بلغة +TLA.
-
ما هي التوصيات المستقبلية التي قدمها الباحثون لتطوير النموذج؟
أوصى الباحثون بتطوير النموذج ليشمل الأخطاء في الشبكة وتغير طوبولوجيتها، واختبار مدى صحة بعض الحلول مثل التوسعية وتضارب القواعد بين عدة متحكمات.
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
