مقالة بحثية

التحقق الرسمي من آليات الإجماع في بلوك تشين باستخدام الحدث-ب

DOI:

10.3791/70193

⸱

مايو 8, 2026

 ,  , 
1Department of Computer Science & Engineering, Pranveer Singh Institute of Technology, AKTU, 2Department of Computer Science & Engineering, Institute of Engineering & Technology

في هذه المقالة

ملخص

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

تقدم هذه الدراسة إطار تحقق رسمي لآليات التوافق على البلوكشين والعقود الذكية، مستخدمة طريقة Event-B. يجمع هذا النهج بين التجريد من التمثيل، والإثبات القائم على الثواب، والتحقق من النماذج الزمنية، مع الفحوصات الرسمية للسلامة والحيوية والمقاومة للإنفاق المزدوج قبل النشر.

الملخص

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

تطور هذه الدراسة إطار عمل تحقق قائم على أساس رسمي لآليات التوافق على البلوك تشين وسلوك العقود الذكية باستخدام Event-B ومنصة Rodin. على عكس الأساليب السابقة التي تعتمد بشكل أساسي على المحاكاة أو التحقق القائم على الحالة للعقود المعزولة، يدمج هذا العمل تجريد آلة الحالة المنتهية (FSM)، والإثبات المدفوع بالثبات، ونمذجة التحسين، والتحقق من المنطق الزمني لتحليل إثبات العمل (PoW)، وإثبات الرهان (PoS)، وآليات منع الإنفاق المزدوج. يتم تجريد العقود الذكية من Solidity إلى نماذج FSM وترميزها كآلات Event-B، مما يتيح تحديد الانتقالات الحالة وقيود السلامة رسميا. يتم التحقق من خصائص الأمان — بما في ذلك تفرد المعاملات، واتساق الحالات، وتطبيق التحكم في الوصول، والحفاظ على الثبات في دفتر الحسابات — من خلال التزامات الإثبات التلقائية في رودين. تم توليد ما مجموعه 312 التزاما بالإثبات، منها 287 (92٪) تم إعفاؤها تلقائيا، و25 منها مثبتة تفاعليا، مما أدى إلى تغطية كاملة للثابت. تم تحديد خصائص الحيوية في منطق شجرة الحوسبة (CTL) وتم التحقق منها عبر فحص النموذج، مما يؤكد حرية الجمود واختيار المدقق النهائي تحت شروط PoS. تم فرض منع الإنفاق المزدوج رسميا باستخدام نمذجة دفتر الأستاذ المتوافقة مع الدولة، حيث تم إثبات قيود التفرد في جميع الولايات القابلة للوصول. تم تحسين منطق الإجماع على مستوى البروتوكول ل PoW وPoS عبر ثلاثة مستويات تجريدية، لضمان سلامة الكتل وصحة المدقق من خلال تحسين تدريجي. تظهر النتائج أن البراهين التي يتم التحقق منها آليا توفر ضمانات صحة قابلة للتحقق تتجاوز التقييم القائم على المحاكاة، مما يؤسس خط تحقق صارم وقابل للتكرار يعزز ضمان الصحة والمتانة على مستوى البروتوكول في أنظمة البلوكشين.

المقدمة

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

تطورت تقنية البلوك تشين لتصبح نموذج دفتر الأستاذ الموزع الذي يتيح حفظ السجلات اللامركزية دون الاعتماد على السلطات المركزية. من خلال تكرار حالات الأستاذ عبر العقد المشاركة وتحقيق الاتفاق عبر آليات التوافق، توفر أنظمة البلوك تشين السلامة والشفافية ومقاومة العبث في البيئات المفتوحة والعدائية. كما وصف ياغا وآخرون، تجمع معمارية البلوك تشين بين البدائيات التشفيرية، وبروتوكولات التوافق الموزعة، والتواصل بين الأقران لضمان أن تصبح المعاملات المثبتة غير عملية حسابيا للتغيير. آليات الإجماع الأساسية مثل إثبات العمل (PoW) وإثبات الحصة (PoS) تنظم اختيار المدققين، والتحقق من الكتل، ومزامنة السجل. بالإضافة إلى ذلك، توسع العقود الذكية قدرات البلوكشين من خلال تضمين منطق قابل للبرمجة ينفذ قواعد محددة مسبقا بشكل مستقل، مما يمكن التطبيقات اللامركزية عبر قطاعات مثل المالية والرعاية الصحية والحوكمة. مع تزايد انتشار تقنيات البلوك تشين في بيئات عالية القيمة وحيوية للسلامة، أصبح ضمان صحة آليات الإجماع وسلوك العقود الذكية أمرا ضروريا للحفاظ على موثوقية التشغيل2.

على الرغم من طبيعتها اللامركزية، تظل أنظمة البلوك تشين عرضة للهشاشة المنطقية وعلى مستوى البروتوكول. قد تحدث هجمات الإنفاق المزدوج عندما لا تطبق قيود اتساق السجل بشكل صارم. أدت نقاط الضعف على مستوى الإجماع، مثل منطق اختيار المدقق غير الصحيح أو قواعد التحقق من الكتل المعيبة، بالإضافة إلى ثغرات العقود الذكية، بما في ذلك إعادة الدخول والتحكم غير السليم في الوصول، إلى خسائر مالية كبيرة في المنصات المنتشرة. على الرغم من أن أطر الاختبار والمحاكاة التجريبية تستخدم على نطاق واسع لتقييم سلوك بروتوكولات PoW وPoS، إلا أن هذه الأساليب تقدم فقط ملاحظات توضيحية بدلا من ضمانات دقيقة شاملة. لا يمكن للتحقق القائم على المحاكاة إثبات الحفاظ الثابت عبر جميع الحالات القابلة للوصول أو ضمان خصائص السلامة والحيوية تحت كل مسار تنفيذ. يبرز هذا القيد الحاجة إلى تقنيات تحقق رياضية يمكنها التفكير بدقة حول أنظمة البلوك تشين بما يتجاوز التحليل الرصدي فقط.

توفر الطرق الرسمية هذا الأساس من خلال تمكين تحديد النظام والتحقق من خلال المنطق الرياضي 3,4. يوسع الحدث-ب هذا النموذج من خلال تحسين تدريجي، حيث يمثل الأنظمة كآلات حالة مجردة حيث تكون حالات النظام مقيدة بالثوابت وتنمذج الانتقالات كأحداث محمية5. تقوم منصة رودان تلقائيا بإنشاء التزامات الإثبات وتدعم تصريفهم، مما يتيح التحقق الآلي من حفظ الثابت واتساق الحالة6. تظهر تقنيات المواصفات الكلاسيكية مثل طريقة B7 وZ8 كيف يمكن للاستدلال القائم على الثبات والتحسين الشكلي ضمان صحة النظام عبر مراحل التطوير المختلفة. تم تطبيق هذه الطرق على نطاق واسع في الأنظمة الحرجة للمهمة والسلامة لضمان الصراحة قبل النشر 9,10,11,12,13. تظهر التوسعات الإضافية مثل UML-B وأطر تحسين الرسوم البيانية قابلية التوسع للنمذجة القائمة على التحسين للأنظمة الصناعيةالمعقدة 14، 15، 16، 17، 18، 19. توضح هذه التطورات أن النمذجة الرسمية المدفوعة بالتحسين يمكنها إدارة تعقيد النظام بفعالية مع الحفاظ على ضمانات صحة قوية.

كما تم استكشاف طرق التحقق الرسمية لأنظمة البلوكشين. تقنيات التحقق من العقود المبنية على SMT تتحقق تلقائيا من الادعاءات داخل برامج Solidity ويمكنها إنتاج أمثلة مضادة عند حدوث انتهاكات منطقية20. تستخدم أدوات مثل VERISOL تجريدات الحالة المنتهية للتحقق من العقود الذكية2، بينما تترجم طرق إثبات النظريات العقود إلى أطر استدلالية رسمية مثل F*21. بالإضافة إلى ذلك، تمكن الصياغة الدلالية لآلة إيثيريوم الافتراضية من التفكير الدقيق حول دلالات التنفيذ واكتشاف الثغرات22. وبالمثل، تم تطبيق بيئات إثبات النظريات مثل Coq لتحليل خصائص الأمان المرتبطة بالتوافق وصحة المعاملات23. بينما توفر هذه الأساليب رؤى قيمة، غالبا ما تركز إما على صحة العقد أو خصائص على مستوى الإجماع بشكل مستقل. نادرا ما يتم دمج ثوابت السجل على مستوى النظام، وانتقالات حالات الإجماع، وسلوك العقود الذكية ضمن إطار موحد قائم على التحسين يحافظ على قابلية التتبع عبر طبقات المواصفات وثواهر التحقق. علاوة على ذلك، تركز العديد من الأساليب الحالية على اكتشاف الثغرات أو التحقق من التأكيدات المنطقية بدلا من الحفاظ المنهجي على ثبات عبر مستويات تحسينية متعددة.

تعالج الدراسة الحالية هذه الفجوة المنهجية من خلال اقتراح إطار تحقق رسمي موحد يدمج تجريد آلة الحالة المنتهية (FSM) لعقود Solidity الذكية مع نمذجة تحسين Event-B وتفريغ الالتزام الإثبات الذي يتم التحقق منه آليا داخل منصة Rodin. بدلا من التعامل مع التحقق من العقود ونمذجة التوافق كمشاكل منفصلة، يحدد الإطار المقترح رسميا انتقالات الحالة على مستوى البروتوكول ل PoW وPoS، وقيود سلامة الحسابات، وشروط تفرد المعاملات، وتطور حالة العقد الذكي ضمن نموذج منظم واحد. تعبر عن خصائص الأمان — بما في ذلك الحفاظ على الثبات، وتفرد المعاملات، وانتقالات الحالات المسيطر عليها، واتساق دفتر الحسابات — كثوابت للحدث B ويتم التحقق منها من خلال التزامات الإثبات المولدة تلقائيا. يتم تحديد الخصائص الزمنية والمعتمدة على ترتيب التنفيذ باستخدام منطق شجرة الحوسبة ويتم التحقق منها من خلال فحص النموذج لضمان صحة ما وراء الثوابت الثابتة. تكمن مساهمة منهجية رئيسية في إثبات قابلية التتبع الصريحة عبر طبقات التجريد: يتم تجريد دوال الصلابة إلى انتقالات FSM، ويتم ترميز انتقالات FSM كأحداث حدث-B، وترتبط الثوابت مع المواصفات الزمنية مباشرة بالتزامات الإثبات اللغوي ونتائج فحص النماذج. يضمن هذا الرسم المنظم أن كل ادعاء صحة مدعوم بأدلة مؤكدة آليا، ويميز بوضوح الضمانات القائمة على الإثبات عن الملاحظات القائمة على المحاكاة.

نطاق هذا العمل مقيد عمدا لضمان الدقة والوضوح التحليلي. يركز النمذجة على انتقالات الحالة على مستوى البروتوكول لآليات التوافق، وقيود سلامة السجل العلمي، وخصائص تفرد المعاملات، وسلوك حالة العقد الذكي. الجوانب على مستوى الشبكة مثل تأخيرات انتشار الرسائل، والاستراتيجيات العدائية البيزنطية، وآليات حل التفرعات، ودلالات غاز الآلة الافتراضية الدقيقة لإيثيريوم تقع خارج حدود التجريد المحددة. من خلال تعريف هذه الافتراضات النمذجة بشكل صريح، يضمن الإطار أن تظل مطالبات التحقق متوافقة مع أدلة الإثبات المثبتة رسميا. يعرض بقية هذه الورقة منهجية التجريد، وعملية نمذجة وتحسين الحدث B، وإجراءات التحقق الثابت والزمني، ونتائج التحقق الناتجة. من خلال ترسيخ بروتوكول البلوكشين والتحقق من العقود الذكية على النمذجة الرسمية القائمة على التحسين والبراهين التي يتم التحقق منها آليا، تعزز هذه الدراسة الصرامة المنهجية وتعزز ضمان صحة ما قبل النشر لأنظمة السجل اللامركزية.

الوصول مقيد. يرجى تسجيل الدخول أو بدء فترة تجريبية لعرض هذا المحتوى.

البروتوكول

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

مدخلات الدراسة
في هذه الدراسة، تم استخدام عقدين ذكيين من Solidity كمدخلات تحقق. الأول كان عقدا على غرار Simple DAO استخدم كدراسة حالة للعودة. أما الثاني فكان عقد تحويل الحسابات/التحويل للحالة مصغر لاختبار القيود على مستوى العقد مقابل الإنفاق المزدوج. كان الشيفرة المصدرية الأصلية ل Solidity بمثابة مدخل لعمليات التجريد والتحقق المحددة في هذا البروتوكول. يتم توضيح عملية التحويل العامة المستخدمة في مثل هذه العقود في الشكل 1، الذي يوضح التحول التدريجي لشفرة مصدر Solidity إلى نماذج FSM وEvent-B وSMV أثناء التحقق.

حدود النمذجة
تركز النمذجة الرسمية على منطق التحكم وتدفق العقود الذكية، بما في ذلك سلوك دخول وخروج الدوال، التنفيذ الداخلي، وانتقالات الحالة على مستوى العقد. تم تمثيل رؤية الدوال (العامة، الخارجية، الداخلية، والخاصة) مع سلوك مكدس المكالمات المقابل المرتبط بتحليل إعادة الدخول. تم التعامل مع أنواع الانتقالات المجردة (الاتصال، الإرسال، النقل) كعمليات لنقل الأثيرات.

تم تعريف الثوابت على مستوى العقد لضمان تفرد المعاملات ومنع الإنفاق المزدوج ضمن حدود التجريد. لتمثيل متطلبات اختيار التحقق وسلامة الكتلة، تم تعريف طبقة تجريد البروتوكول والمنطق من حيث انتقالات الحالة على مستوى البروتوكول لكل من إثبات العمل وإثبات الرهان.

لم يشمل الحد التجريدي عناصر طبقة الشبكة، بما في ذلك جدولة الرسائل التي سيتم تسليمها والتأخيرات الناتجة عن عدد من القفزات، وحل التفرعات، واستخدام خصوم الشبكة لاستراتيجيات بيزنطية، ودلالات الآلة الافتراضية الإيثيريومية، ودلالات الغاز التي تتحكم بها عقد الشبكة، وانتشار الاستثناءات، والتنفيذ غير المتزامن، والسلوك الاحتياطي المعقد، والنهائية على مستوى الشبكة. لذا، فإن نتائج تحديد الإنفاق المزدوج تنطبق فقط على الثوابت على مستوى العقود ولا تشكل اتفاقا على مستوى الشبكة حول النهائية.

الأدوات والتكوين
استخدمت منصة رودان لنمذجة وتحسين وتوليد التزامات الإثبات، وتنفيذ نموذج Event-B (الإصدار 3.7.0)، مما مكن مبروكات PP وML وSMT وAtelier-B من إصدار البراهين تلقائيا وتفاعليا. تم تشغيل نسخة nuXmv 2.0.0 على نماذج SMV المولدة في وضع استكشاف CTL الكامل لإجراء فحص نماذج CTL.

تم تنفيذ جميع عمليات التحقق في بيئة حسابية مضبوطة باستخدام أوبونتو 22.04 LTS وOpenJDK 11 وبايثون 3.10.12. تم استخدام Web3 (7.6.0)، NetworkX (3.4.2)، Matplotlib (3.8.0)، Graphviz (0.20.3)، NumPy (1.26.4)، وPandas (2.2.2) لتنفيذ عناصر المحاكاة والتصور. ضمن هذا التصميم إمكانية إعادة إنتاج نتائج التحقق والمحاكاة الرسمية عند تنفيذها تحت نفس ظروف التنفيذ.

سير عمل التحول
تكونت عملية التحقق هذه من أربع مراحل. تمت ترجمة عقود الصلابة أولا إلى تمثيل آلة الحالة المنتهية (FSM-SC). تم ترميز نموذج FSM-SC لاحقا في Event-B، مع ثوابت محددة ودرجات تحسين واضحة. تمت ترجمة تجريد FSM-SC إلى نموذج SMV في nuXmv. تم الإبلاغ عن نتائج التحقق كإحصائيات حول إثبات الإعفاء من الالتزام وفحص نموذج CTL، وتم تقديم أمثلة مضادة كحالات.

بناء FSM
تم تجريد كل عقد كآلة حالة محدودة تعرف كما يلي:

figure-protocol-1

حيث:
S = مجموعة الحالات
S₀ = الحالة الابتدائية
T = علاقة انتقالية
V = رسم الرؤية
G = مسندات الحماية
A = تحديثات الإجراءات/الحالة.

الخوارزمية 1: بناء FSM من Solidity
الإدخال: كود المصدر Solidity
المخرج: FSM-SC

1) تحليل شجرة النحو المجردة لعقد الصلابة.
2) إنشاء الحالة الابتدائية S₀ من تعريف المنشئ.
3) لكل دالة صلابة f، أنشئ حالة تحكم مميزة S_f وسجل رؤية V(f) ∈ {عامة، خارجية، داخلية، خاصة}.
4) لكل بيان ضمن الدالة f، اشتق انتقال t عن طريق استخراج مسندات الحراسة من شروط الطلب/التأكيد والإجراءات من تحديثات متغيرات الحالة.
5) أضف الانتقال t إلى T.
6) إنشاء أنواع انتقال صريحة لعمليات نقل الإيثر (استدعاء، إرسال، نقل)، والاستدعاءات الداخلية والخارجية، واستدعاء التفويض، والتدمير الذاتي، واستخدام tx.origin، والفروع الشروطية، وتركيبات الحلقات.
7) إعادة FSM-SC = (S, S₀, T, V, G, A).

وكل دالة صلبة مرتبطة بحالة تحكم مختلفة في FSM. لفهم الثغرات، تم تجريد تدفقات التنفيذ ذات الصلة بالثغرات، مثل تلك التدفقات التي تتضمن استدعاءات خارجية تليها تحديثات توازن، بشكل صريح إلى انتقالات مرتبة. يصف الشكل 2 نموذجا لمخطط FSM-SC لعقد على نمط SimpleDAO، موضحا كيف تم تجريد حالات الدخول، وانتقالات الاستدعاء الخارجي، وتسلسلات تحديث الحالة خلال هذه المرحلة من البناء.

ترميز FSM إلى الحدث-B
تم تمثيل انتقال FSM كهياكل حدث ب. جميع الانتقالات تتوافق مع أحداث الحدث ب، بما في ذلك الحراس والإجراءات الخاصة.

خوارزمية 2: ترميز FSM إلى الحدث B
الإدخال: FSM-SC
المخرج: آلة الحدث-ب والسياق

1) تعريف STATE_SET والوظيفة في سياق العقد.
2) إعلان المتغيرات التي تمثل حالة التحكم في FSM وحالة على مستوى العقد.
3) تمثيل كل حالة تحكم FSM s ∈ S باستخدام current_state ∈ STATE_SET.
4) لكل انتقال (s →s′, g, a)، أنشئ حدث-ب حدث E_t مع:
5) حيث current_state = s ∧ g
6) ثم current_state := s′ ∥ ينطبق (a)
7) ترميز قيود الرؤية باستخدام حراس مشتقة من V(f).
8) تعريف الثوابت inv1–inv9 لالتقاط خصائص السلامة والاتساق.
9) تعريف التهيئة عن طريق تعيين قيم S₀ والقيم الافتراضية.

مجموعة الحالات، الحالة الحالية، رؤية الدالة، مكدس الاستدعاءات، ختم المعاملات، حالة نقل الأثير، علم الاستدعاء، علم التدمير الذاتي، وحالة التحقق هي بعض المتغيرات التي تم التقاطها في نموذج الحدث B. الثوابت (inv1-inv9) وإجراءات التهيئة (act1-act6) تتطابق مع تلك الموجودة في المواصفة الرسمية. يوفر الشكل 3 أيضا تمثيلا بيانيا لكيفية الحفاظ على الأحداث الرئيسية ذات الصلة بالثغرات، خاصة الانتقالات المتعلقة بإعادة الدخول، في ترميز الحدث B. يشرح هذا الشكل كيف يتم رسم الأنماط الهيكلية لنموذج FSM-SC الموضحة في الشكل 2 إلى أحداث حدث-ب قابلة للتحقق.

استراتيجية التنقية
تم تنفيذ مستويين من التحسين. تم تمثيل تدفق التحكم التعاقدي عالي المستوى والثوابت الأساسية على المستوى المجرد. أضاف المستوى المحسن قيودا خاصة بالعقود، بما في ذلك قيود مكدس النداءات، وقيود الرؤية، وشروط منع العودة إلى المكان.

الخوارزمية 3: التحسين والتفريغ بالإثبات
الإدخال: آلة مجردة وآلة مكررة
النتائج: التزامات وإحصائيات إثبات الإسفاء

1) توليد التزامات إثبات للآلة المجردة في رودان.
2) تنفيذ الإثباتات التلقائية الممكنة وتسجيل نتائج التفريغ.
3) توليد التزامات مقاومة للتحسين للآلة المكررة.
4) تطبيق الإثباتات التلقائية على التزامات التحسن.
5) الوفاء بالالتزامات المتبقية بشكل تفاعلي عند الضرورة.
6) إحصائيات إثبات التصدير وتقارير الحالة.

شملت تقارير الإثبات عدد الثواب، مستويات التنقية، التزامات الإثبات المولدة، معدل التفريغ التلقائي، معدل التفريغ التفاعلي، ومعدل التفريغ النهائي.

مواصفات خصائص CTL وفحص النماذج
تمت ترجمة تجريد FSM-SC إلى نموذج SMV للتحقق الزمني المتفرع في nuXmv.

الخوارزمية 4: التحقق من FSM إلى SMV وCTL
المخرج: نتيجة التحقق من PASS/FAIL وتتبع الأمثلة المضادة (إن وجدت)

1. تسجيل حالات التحكم في FSM كحالة متغيرة SMV معدودة.
2. تحويل انتقالات FSM إلى تعيينات محمية للولايات التالية.
3. الحفاظ على العلامات المتعلقة بالحالات المتعلقة بالثغرات، مثل المكالمات الخارجية وتحديثات التوازن.
4. ترميز خصائص CTL في nuXmv وإجراء فحص النماذج.
5. إذا فشلت خاصية، قم بتوليد مسارات الأمثلة المضادة التي تمثل تسلسلات انتقال FSM.

شمل فحص CTL متطلبات أوامر إعادة الدخول، وإنهاء تحديثات الحالة بعد عمليات النقل، والحد من الدخول المتكرر غير المقيد إلى الأقسام الحرجة، وتجنب الجمود.

خصائص الأمان تم التحقق منها
تم تأكيد عقد Simple DAO الذي يمنع العودة إلى الداخل من خلال ضمان ترتيب آمن بين المكالمات الخارجية وتحديثات الحالة عبر الثوابت وقيود CTL. وعندما يسمح ذلك، كان هؤلاء الحراس يفحصون قيود التحكم في الوصول، لضمان تقييد الانتقالات غير المصرح بها بواسطة الثابتات. وقد تحقق نموذج السجل المختصر من ثوابت تفرد المعاملات واتساقها على مستوى الوقاية داخل العقد.

المخرجات المبلغ عنها
يوفر قسم النتائج تقارير حول مقاييس هيكلية FSM، ومقاييس نموذج الحدث B، والإحصائيات لإثبات الالتزام والتحقق من CTL. تقدم نتائج الإثبات الرسمي، ونتائج التحقق من نموذج CTL، بشكل منفصل للتمييز بين ضمانات صحة الأدلة بواسطة الثوابت وأدلة التحقق الزمني باستخدام التحقق الزمني.

الوصول مقيد. يرجى تسجيل الدخول أو بدء فترة تجريبية لعرض هذا المحتوى.

النتائج

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

تجمع نتائج هذا العمل بين منتجات التحقق الرسمية لفحص نموذج Event-B وCTL مع معلومات قابلة للتنفيذ من محاكاة البلوكشين. يدعم دمج هذه المخرجات متعددة الطبقات التحقق من صحة السلوكيات الرئيسية في العقود الذكية، وأنظمة التوافق الخاصة بها، وحدود صلاحية الدفتر ضمن التمثيل المحدود للتصميم.

إعداد البيئة والتحقق من التبعية
تم إطلاق بيئة التنفيذ المستخدمة لتحويل النموذج والتحقق والمحاكاة دون تعارضات التبعية. باستخدام Web3 وNetworkX وMatplotlib وGraphviz...

الوصول مقيد. يرجى تسجيل الدخول أو بدء فترة تجريبية لعرض هذا المحتوى.

المناقشة

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

تظهر التحقق الرسمي والمعتمد على المحاكاة أن نظام التحقق متعدد الطبقات المستخدم في البحث المعطى كان قادرا على التحقق من سلوك العقود الذكية، وصحة آلية الإجماع، وخاصية السلامة في دفتر الأستاذ تحت حدود التجريد المحددة جيدا. يوفر الحدث B تمثيلا رياضيا لخصائص السلامة، ومنطق تدفق الحالة، ومنع العودة من حيث الثوابت والمنطق القائم على التحسين 5,6. حقيقة أن معدل الإثبات والتفريغ مرتفع تعني أن الأنظمة التي يتم نمذجتها منطقية داخليا وتتماشى ...

الوصول مقيد. يرجى تسجيل الدخول أو بدء فترة تجريبية لعرض هذا المحتوى.

الإفصاحات

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,

المؤلفون لا يفرضون أي تضارب مصالح.

المواد

قائمة المواد المستخدمة في هذه المقالة
الاسمالشركةرقم فهرسيالتعليقات
منصة رودان (v3.7.0)فريق رودان / مؤسسة إكليبسhttps://www.event-b.org/install.htmlنمذجة الحدث B، والتنقيح، وتوليد وإثبات الالتزام والتنفيذ
طريقة الحدث-بجامعة ساوثهامبتون / مجتمع رودانhttps://www.event-b.org/إطار النمذجة الرسمي لتحديد وتحسين الثبات
nuXmv Model Checker (v2.0.0)FBK (مؤسسة برونو كيسلر)https://nuxmv.fbk.eu/التحقق الرمزي من النماذج لخصائص CTL
Graphviz (v0.20.3)فريق جرافيزhttps://graphviz.org/تصور FSM وعرض الرسوم البيانية
بايثون (الإصدار 3.10.12)مؤسسة بايثون للبرمجياتhttps://www.python.org/downloadsبيئة المحاكاة والتنفيذ
Web3.py (الإصدار 7.6.0)مؤسسة إيثيريوم / المساهمونhttps://web3py.readthedocs.io/تفاعل البلوكشين ومحاكاة المعاملات
NetworkX (الإصدار 3.4.2)مطوري NetworkXhttps://networkx.org/نمذجة الرسوم البيانية لهياكل البلوكشين وإدارة الأنظمة المالية
ماتبلوتليب (الإصدار 3.8.0)فريق تطوير ماتبلوتليبhttps://matplotlib.org/رسم وقت التعدين وتوزيعات المدقق
NumPy (الإصدار 1.26.4)مطورو نومبيhttps://numpy.org/الحسابات العددية
الباندا (الإصدار 2.2.2)فريق تطوير البانداhttps://pandas.pydata.org/تحليل البيانات ومعالجتها
OpenJDK 11مجتمع أوراكل / OpenJDKhttps://openjdk.org/projects/jdk/11/مدة التشغيل المطلوبة لمنصة رودان
أوبونتو 22.04 LTSكانونيكال المحدودة.https://ubuntu.com/downloadنظام التشغيل لجميع التجارب
الصلابةمؤسسة إيثيريومhttps://soliditylang.org/لغة المصدر للعقد الذكي المستخدمة كإدخال
لغة الإدخال nuXmv (SMV)FBKhttps://nuxmv.fbk.eu/documentation.htmlتمثيل النموذج الوسيط للتحقق من CTL

المراجع

$$\rightleftharpoonup{xx}$$ $$\longleftharp{xx}$$, $$\longrightharp{xx}$$,
  1. Yaga, D., Mell, P., Roby, N., Scarfone, K. Blockchain Technology Overview. , National Institute of Standards and Technology. Gaithersburg, MD, USA. (2018).
  2. Wang, Y., et al. Formal specification and verification of smart contracts for Azure Blockchain. arXiv preprint. , (2019).
  3. Huth, M., Ryan, M. Logic in Computer Science: Modelling and Reasoning About Systems. , Cambridge University Press. Cambridge, U.K. (2004).
  4. Baier, C., Katoen, J. P. Principles of Model Checking. , MIT Press. Cambridge, MA, USA. (2008).
  5. Abrial, J. R. Modeling in Event-B: System and Software Engineering. , Cambridge University Press. Cambridge, U.K. (2010).
  6. Abrial, J. R., et al. Rodin: An open toolset for modelling and reasoning in Event-B. Int. J. Softw. Tools Technol. Transf. 12 (6), 447-466 (2010).
  7. Abrial, J. R. The B-Book: Assigning Programs to Meanings. , Cambridge University Press. Cambridge, U.K. (1996).
  8. Jacky, J. The Way of Z: Practical Programming with Formal Methods. , Cambridge University Press. Cambridge, U.K. (1996).
  9. Verma, S., Yadav, D., Chandra, G. Introduction of formal methods in blockchain consensus mechanism and its associated protocols. IEEE Access. 10, 66611-66621 (2022).
  10. Guha, S., Nag, A., Karmakar, R. Formal verification of safety-critical systems: A case study in airbag system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 107-116 (2021).
  11. Karmakar, R. Formal verification techniques: A comparative analysis for critical system design. Proc. Int. Conf. Intelligent Systems Design and Applications, , Springer. Cham, Switzerland. 93-102 (2022).
  12. Karmakar, R. Symbolic model checking: A comprehensive review for critical system design. Adv. Data Inf. Sci. , Springer. Singapore. 693-703 (2022).
  13. Said, M. Y., Butler, M., Snook, C. A method of refinement in UML-B. Softw. Syst. Model. 14 (4), 1557-1580 (2015).
  14. Snook, C. F., Butler, M. J. UML-B: A plug-in for the Event-B tool set. Proc. ABZ 2008: Abstract State Machines, B and Z, , Springer. 344-358 (2008).
  15. Ben Younes, A., Ben Ayed, L. From UML activity diagrams to Event-B for the specification and the verification of workflow applications. Proc. IEEE 32nd Int. Conf. Computer Software and Applications, , 643-648 (2008).
  16. Morris, K. V., Snook, C. Reconciling SCXML Statechart Representations and Event-B Lower Level Semantics. , Sandia National Laboratories. Livermore, CA, USA. (2016).
  17. Butler, M. Decomposition structures for Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. 20-38 (2009).
  18. Butler, M. Incremental design of distributed systems with Event-B. Proc. Integrated Formal Methods (IFM 2009), , Springer. Berlin, Heidelberg. (2009).
  19. Le, T. C., Garriga, M., Pautasso, C., Stankovic, M. Proving conditional termination for smart contracts. Proc. ACM Workshop Blockchains, Cryptocurrencies, and Contracts, , (2018).
  20. Alt, L., et al. SMT-based verification of Solidity smart contracts. Proc. ISoLA 2018: Leveraging Applications of Formal Methods, , Springer. Cham, Switzerland. 376-388 (2018).
  21. Bhargavan, K., et al. Formal verification of smart contracts. Proc. ACM Workshop Programming Languages and Analysis for Security, , 91-96 (2016).
  22. Grishchenko, I., Maffei, M., Schneidewind, C. A semantic framework for the security analysis of Ethereum smart contracts. Formal Methods Secure Software Systems (PoST 2018), , Springer. Cham. 243-269 (2018).
  23. Nielsen, J. B., et al. Smart contract interactions in Coq. arXiv preprint. , (2019).

الوصول مقيد. يرجى تسجيل الدخول أو بدء فترة تجريبية لعرض هذا المحتوى.

إعادة الطباعة والأذونات

طلب إذن لإعادة استخدام النص أو الأشكال في مقالة JoVE هذه

طلب إذن

الوسوم

Event B

مقالات ذات صلة