اشترك بالحزمة الذهبية واحصل على وصول غير محدود شمرا أكاديميا
تسجيل مستخدم جديدتوصيف الوصولية في شبكة (SDN) باستخدام TLA+
Reachability Specification in (SDN) by TLA+
884
0 61
0
(
0
)
تمت اﻹضافة من قبل
Shamra Editor
اسأل ChatGPT حول البحث
في هذا البحث تم توصيف الشبكة بواسط الجبر المنطقي و ذلك لكي يتم فرز الرزم إلى مجموعتين تتضمن الرزم التي ستصل إلى الهدف و الرزم التي سيتم سحبها وفق حالة الشبكة و جداول التدفق, تم كتاب التوصيف باستخدام لغة 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.
المراجع المستخدمة
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
قيم البحث
اقرأ أيضاً
نقدم في هذا البحث نموذجاً صورياً لتوصيف عملية هجرة المضيفات في SDN بحيث
يتم التأكد من خاصية الوصولية (Reachability ) لمرزم و عدم تغييرها بعد الانتقال
و تحقيق التعديلات المطلوبة لكي يتم الحفاظ على نفس الخصائص. تم تصميم النموذج
بواسطة لغة التوصيف
الصوري TLA+ و التحقق منه من خلال أداة فحص النماذج TLC
المترافقة معه, حيث تميز النموذج بعدد قليل للحالات لتحقيق المطلوب.
تعد عملية التخطيط بين عناوين الطبقة الثالثة (IP) والطبقة الثانية (MAC) المفتاح الرئيسي في شبكات IP، وذلك من خلال بروتوكول دقة العناوين ARP في شبكات IPv4. بما أن هذا البروتوكول غير مستقر ولا يستخدم أي آلية للمصادقة فإنه يعد هدفاً سهلاً لهجمات الخداع.
قد تؤدي هذه الهجمات بدورها إلى هجمات أعقد مثل هجوم الرجل في المنتصف MIM وهجوم حجب الخدمة DoS. ناقشنا في هذا البحث مشكلة هجوم خداع البروتوكول ARP من خلال الدراسة في سياق الشبكات المعرفة بالبرمجيات SDN. دُرست مجموعة من البارامترات الهامة مثل الإنتاجية والتأخير وتوافرية الشبكة. بينت النتائج أن هجمات خداع البروتوكول ARP قادرة على التأثير سلباً على أداء الشبكة.
تعد الشبكات المعرفة برمجيا" SDNواحدة من أكثر أنواع الشبكات تأثيرا" في تكنولوجيا المعلومات والاتصالات مقارنة بجميع تكنولوجيات الشبكات التقليدية التي يوجد فيها الكثير من التحديات، كما تعدّ شبكات SDN من أكثر الحلول الواعدة للإنترنت في المستقبل وتوفر بن
ية تحتية قوية للشبكات بمواصفات عالية وتكلفة منخفضة، وتمثل مستقبل الجيل القادم لهندسة الشبكات بسبب سهولة تقسيم الشبكات وبرمجتها ومراقبتها، والتحكم فيها وإدارتها من خلال وحدة تحكم مركزية، كما إنّ فصل مسارات التحكم عن مسارات تمرير البيانات في شبكات SDN، يسهّل عملية إدارة وتطوير الشبكات، حيث تستخدم هذه التقنية حاليا" في مراكز البيانات والشبكات اللاسلكية، كما تعد حلا" للكثير من المشاكل التي تواجهها الشبكات التقليدية. تتميز شبكات SDN بالديناميكية الكافية للتعامل مع الظروف المختلفة للشبكة، ويعدّ المتحكم أحد أهم مكوناتها ويعتبر المكون الأذكى في الشبكة، ونظرا" لأهمية اختيار المتحكم المناسب حسب البارامترات والظروف المختلفة لشبكة SDN، قمنا في هذا البحث بإجراء تحليل لخصائص الشبكات المعرفة برمجيا"، و اعتمد التحليل على مقارنة شبكات SDN بوجود متحكم وحيدOpenDaylight (ODL) مع عدة متحكمات ODL، تم اختيار المتحكم ODL كونه يعدّ من المتحكمات الشهيرة ويتميز عن غيره بأنه مفتوح المصدر ويحتوي على datastore موزعة ومصمم ليناسب بيئة مراكز البيانات، مع الأخذ بعين الاعتبار بروتوكول OpenFlow المدعوم على الواجهة الجنوبية من قبل هذا المتحكم، ويتضمن البحث محاكاة لطبولوجيا الشبكات المعرفة برمجيا" باستخدام المحاكي Mininet، كما تم تحليل السيناريوهات والمعاملات المختلفة مثل معدل البيانات وتأخير الرزم والإنتاجية من خلال الأداة D-ITG.
إن الشبكات الحاسوبية التقليدية الحالية تأخذ منحى أن تكون معقدة أكثر نظراً لمتطلبات المستخدمين المتزايدة باستمرار. الشبكات المعرفة بالبرمجيات SDN هي نموذج جديد لتسهيل إدارة الشبكة وجعلها قابلة للبرمجة من خلال فصل مستوى التحكم عن مستوى التوجيه (المتضمن
الموجهات والمبدلات). في هذا النموذج يتم استخدام متحكم مركزي لإدارة مستوى التحكم ويتم التفاعل بين المتحكم وبين مستوى التوجيه من خلال بروتوكول معياري OpenFlow. هناك العديد من المتحكمات المستخدمة حالياً, منها على سبيل المثال لا الحصر POX, Ryu, ONOS, و OpenDaylight. السؤال المهم والمطروح بشدة هو أي من المتحكمات العديدة هو الأفضل لنستخدمه في شبكتنا خلال تصميمها ويكون مناسباً لأهداف شبكتنا؟؟ للإجابة على هذا السؤال قمنا باقتراح طريقة اتخاذ قرار في هذه الورقة. بدايةً, تم اختيار أربعة متحكمات بالإضافة لتحليل خمسة معايير من أجل جمع خصائص هذه المتحكمات. من ثم, قمنا بتطبيق طريقة اتخاذ القرار المتعدد الخصائص (TOPSIS) من أجل ترتيب هذه المتحكمات واختيار الأفضل بينها. عند تطبيق هذه الطريقة قمنا بإجراء دراسة مقارنة من أجل تقييم أداء تلك المتحكمات ضمن بيئة شبكية محلية LAN وتم اختيار المتحكم Ryu كأفضل متحكم مناسب بالاستناد للمعايير المتبعة في هذه الوقة.
أظهرت تقنية الشبكات الضوئية المعتمدة على Automatically Switched Optical Network (ASON)\Generalized Multi-Protocol Label Switching (GMPLS) وثوقية عالية في الآونة الأخيرة، إلاَّ أنّ مسألة التحكم الموحد في الشبكات الضوئية أمست ضرورةً مُلحّة لتغطية المش
اكل الناتجة عن التحكم المنفصل بين طبقات الشبكة الضوئية المختلفة. وقد حققت محاولة تطبيق التحكم الموحد المستند إلى GMPLS في شبكات بروتوكول الانترنت/التنضيد بتقسيم طول الموجة المكثفInternet Protocol /Dense Wavelength Division Multiplexing (IP/DWDM) نتائجاً مرضية لكنها عكست تعقيداً كبيراً عند التشغيل في الزمن الحقيقي. من ناحية أخرى، يتم طرح مستوى تحكم OpenFlow كحل واعد ليكون مستوى تحكم موحد في مثل هذه الشبكات، لكنه ليس فعّالاً بدرجة كافية للتحكم في عقد التبديل الضوئية حتى الآن. لذلك، كخطوة وسيطة نحو مستوى تحكم موحد UCP يستند كليّاً إلى البروتوكولOpenFlow ، فإنّ الخيار المنطقي في الوقت الحالي هو تقديم مستوى تحكم التشغيل البيني OpenFlow/GMPLS القادر على استخدام GMPLS للتحكم في الطبقة الضوئية والتنسيق الديناميكي بين طبقة IP والطبقات الضوئية. يُقدم هذا البحث تطبيقاً عمليّاً لحلول التشغيل البيني (المتوازي والمتراكب والمتكامل) لمستويات التحكم GMPLS وOpenFlow المطبّقة على الشبكة الضوئيّة ASON المركّبة في المنطقة الجنوبية من سوريا. وقد أظهرت النتائج بأن الحل المتكامل للتحكم الموحد يتفوق على الحلول المتوازية والمتراكبة من حيث زمن التأخير الكلي لتوفير المسار في الشبكة الضوئيّة Overall path provisioning latency (OPPL)، على حساب التعقيد العالي للتصميم ومعالجة الحمل داخل المتحكم.
سجل دخول لتتمكن من نشر تعليقات
التعليقات
جاري جلب التعليقات
سجل دخول لتتمكن من متابعة معايير البحث التي قمت باختيارها
