מאמר מחקר

אימות פורמלי של מנגנוני קונצנזוס בבלוקצ'יין באמצעות אירוע-B

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 ופלטפורמת רודין. בניגוד לגישות קודמות שהסתמכו בעיקר על סימולציה או אימות מבוסס מקרה של חוזים מבודדים, עבודה זו משלבת הפשטה של מכונת מצבים סופיים (FSM), הוכחה מונעת אינבריאנט, מידול שיפור ואימות לוגי זמני לניתוח הוכחת עבודה (PoW), הוכחת הימור (PoS) ומנגנונים למניעת הוצאה כפולה. חוזים חכמים של Solidity מופשטים ל-FSMs ומקודדים כמכונות Event-B, מה שמאפשר להגדיר באופן פורמלי מעברי מצבים ומגבלות בטיחות. מאפייני בטיחות — כולל ייחודיות העסקאות, עקביות מצב, אכיפת בקרת גישה ושימור אינבריאנטי פנקס חשבונות — מאומתים באמצעות התחייבויות הוכחה שנוצרות אוטומטית ברודין. בסך הכל נוצרו 312 התחייבויות הוכחות, מתוכן 287 (92%) שוחררו אוטומטית, ו-25 הוכחו באופן אינטראקטיבי, מה שהוביל לכיסוי מלא של אינווריאנטיות. תכונות חיות הוגדרו בלוגיקת עץ החישוב (CTL) ואומתו באמצעות בדיקת מודל, מה שמאשר חופש קיפאון ובחירת מאמתים בתנאי PoS. מניעת הוצאה כפולה נאכפה רשמית באמצעות מודל פנקס עקבי מצבים, כאשר הוכחו מגבלות ייחודיות בכל המדינות הנגישות. לוגיקת הקונצנזוס ברמת הפרוטוקול עבור PoW ו-PoS שופרה בשלוש רמות הפשטה, תוך הבטחת שלמות בלוק ונכונות מאמתים באמצעות שיפור מדרגה. התוצאות מראות שהוכחות שנבדקו במכונה מספקות ערבויות נכונות שניתן לאמת מעבר להערכה מבוססת סימולציה, ובכך מקימות צינור אימות קפדני וניתן לשחזור שמגביר את הבטחת הנכונות ואת החוסן ברמת הפרוטוקול במערכות בלוקצ'יין.

מבוא

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

טכנולוגיית הבלוקצ'יין התפתחה לפרדיגמת פנקס חשבונות מבוזר שמאפשרת שמירה מבוזרת של רשומות ללא תלות בסמכויות מרכזיות. על ידי שכפול מצבי פנקס בין הצמתים המשתתפים והשגת הסכמה באמצעות מנגנוני קונצנזוס, מערכות בלוקצ'יין מספקות שלמות, שקיפות ועמידות לשיבוש בסביבות פתוחות ועמותות. כפי שמתואר על ידי יאגה ואחרים, ארכיטקטורת הבלוקצ'יין משלבת פרימיטיבים קריפטוגרפיים, פרוטוקולי קונצנזוס מבוזרים ותקשורת עמית לעמית כדי להבטיח שעסקאות מאומתות יהפכו לבלתי מעשיות חישובית לשינוי. מנגנוני קונצנזוס מרכזיים כגון הוכחת עבודה (PoW) והוכחת הימור (PoS) מסדירים את בחירת הוולידטורים, אימות הבלוקים וסנכרון הלדג'רים. בנוסף, חוזים חכמים מרחיבים את יכולות הבלוקצ'יין על ידי הטמעת לוגיקה מתוכנתת שמבצעת באופן עצמאי כללים מוגדרים מראש, ומאפשרת יישומים מבוזרים במגזרים כמו פיננסים, בריאות וממשל. ככל שטכנולוגיות בלוקצ'יין מיושמות יותר ויותר בסביבות יקרות ערך וקריטיות לבטיחות, הבטחת נכונות מנגנוני הקונצנזוס והתנהגות החוזים החכמים הפכה לחיונית לשמירה על אמינות תפעולית2.

למרות אופיין המבוזר, מערכות הבלוקצ'יין נשארות פגיעות לפגיעויות לוגיות וברמת הפרוטוקול. התקפות הוצאה כפולה עלולות להתרחש כאשר מגבלות עקביות הספר אינן נאכפות בקפדנות. חולשות ברמת הקונצנזוס, כמו לוגיקת בחירת מאמתים שגויה, או כללי אימות בלוק פגומים, כמו גם פגיעויות בחוזים חכמים, כולל חזרה לכניסה ובקרת גישה לא נכונה, הובילו להפסדים כספיים משמעותיים בפלטפורמות המופעלות. למרות שמסגרות בדיקה אמפיריות וסימולציה משמשות באופן נרחב להערכת התנהגות פרוטוקולי PoW ו-PoS, גישות אלו מספקות רק תצפיות להמחשה ולא הבטחות נכונות מקיפות. אימות מבוסס סימולציה אינו יכול להוכיח שמירה בלתי משתנה בכל המצבים הנגישים או להבטיח תכונות בטיחות וחיות בכל מסלול ביצוע. מגבלה זו מדגישה את הצורך בטכניקות אימות מבוססות מתמטיקה שיכולות להסיק ביסודיות מערכות בלוקצ'יין מעבר לניתוח תצפיתי.

שיטות פורמליות מספקות בסיס כזה בכך שהן מאפשרות מפרט ואימות מערכת באמצעות לוגיקה מתמטית 3,4. אירוע-B מרחיב פרדיגמה זו באמצעות עידון מדרגה, ומציג מערכות כמכונות מצבים מופשטות שבהן מצבי המערכת מוגבלים על ידי אינבריאנטים והמעברים מדומים כאירועים מוגנים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 ופריקת חובות הוכחה שנבדקה על ידי מכונה בתוך פלטפורמת רודין. במקום להתייחס לאימות חוזים ומידול קונצנזוס כבעיות נפרדות, המסגרת המוצעת מגדירה באופן פורמלי מעברי מצב ברמת הפרוטוקול עבור PoW ו-PoS, מגבלות שלמות הלדג'ר, תנאי ייחודיות של העסקאות והתפתחות מצב חוזה חכם בתוך מודל מובנה אחד. מאפייני בטיחות — כולל שימור אינבריאנטי, ייחודיות עסקאות, מעברי מצבים מבוקרים ועקביות ספר חשבונות — מבוטאים כבלתי משתתפים באירוע-B ונאמתים באמצעות התחייבויות הוכחה שנוצרות אוטומטית. תכונות זמניות ותלויות בסדר ביצוע מוגדרות באמצעות לוגיקת עץ החישוב ונאמתות באמצעות בדיקת מודלים כדי להבטיח נכונות מעבר לאינווריאנטים סטטיים. תרומה מתודולוגית מרכזית טמונה בקביעת מעקב מפורש בין שכבות הפשטה: פונקציות סולידיות מופשטות למעברי FSM, מעברי FSM מקודדים כאירועי אירוע-B, ואינווריאנטים יחד עם מפרטים זמניים מקושרים ישירות להתחייבויות הוכחה משוחררות ולתוצאות בדיקת מודלים. מיפוי מובנה זה מבטיח שכל טענה לנכונות נתמכת בראיות מאומתות על ידי המכונה ומבדילה בבירור בין ערבויות מבוססות הוכחה לתצפיות מבוססות סימולציה.

היקף עבודה זו מוגבל במכוון כדי להבטיח דיוק ובהירות אנליטית. המידול מתמקד במעברי מצב ברמת הפרוטוקול עבור מנגנוני קונצנזוס, מגבלות שלמות החשבונות, תכונות ייחודיות של עסקאות והתנהגות מצב חוזה חכם. היבטים ברמת הרשת כמו עיכובים בהפצת הודעות, אסטרטגיות יריבה ביזנטיות, מנגנוני פתרון פיצול וסמנטיקה מפורטת של גז מכונה וירטואלית של את'ריום, נמצאים מחוץ לגבול ההפשטה המוגדר. על ידי הגדרה מפורשת של הנחות מודל אלו, המסגרת מבטיחה שטענות אימות יישארו מותאמות לראיות הוכחות מאומתות פורמלית. שאר המאמר מציג את מתודולוגיית ההפשטה, תהליך המידול והשיפור של Event-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.

כל ביצועי האימות בוצעו בסביבה חישובית מבוקרת באמצעות Ubuntu 22.04 LTS, OpenJDK 11 ו-Python 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) לנתח את עץ התחביר המופשט של חוזה Solidity.
2) ליצור את מצב ההתחלה S₀ מתוך הגדרת הקונסטרקטור.
3) עבור כל פונקציית Solidity f, ליצור מצב בקרה מובחן S_f ולרשום נראות V(f) ∈ {ציבורי, חיצוני, פנימי, פרטי}.
4) עבור כל משפט בתוך פונקציה f, נגזר מעבר t על ידי חילוץ פרדיקטים של שומרים מתנאי דרישה/אסרט ופעולות מעדכוני משתני מצב.
5) מוסיפים מעבר t ל-T.
6) יצירת סוגי מעבר מפורשים לפעולות העברת אתר (קריאה, שליחה, העברה), קריאות פנימיות וחיצוניות, קריאת delegatecall, השמדה עצמית, שימוש tx.origin, הסתעפות מותנות ומבני לולאות.
7) החזרת FSM-SC = (S, S₀, T, V, G, A).

וכל פונקציית Solidity משויכת למצב שליטה FSM שונה. להבנת פגיעויות, זרימות ביצוע רלוונטיות לפגיעות, למשל זרימות עם קריאות חיצוניות ואחריהן עדכוני איזון, הופשטו במפורש למעברים מסודרים. איור 2 מתאר דוגמה לדיאגרמת FSM-SC לחוזה בסגנון SimpleDAO, המראה כיצד מצבי כניסה, מעברי קריאה חיצונית ורצפי עדכון מצב הופשטו במהלך שלב הבנייה הזה.

קידוד FSM לאירוע-B
מעבר FSM יוצג כמבנים של אירוע-B. כל המעברים תואמים לאירועי אירוע-B, כולל שומרים ופעולות מסוימים.

אלגוריתם 2: קידוד FSM לאירוע-B
קלט: FSM-SC
פלט: מכונת אירוע-B והקשר

1) להגדיר STATE_SET ופונקציה בהקשר החוזה.
2) הכרזה על משתנים המייצגים מצב שליטה ב-FSM ומצב ברמת החוזה.
3) ייצג כל מצבי בקרה של FSM s ∈ S באמצעות current_state ∈ STATE_SET.
4) עבור כל מעבר (s →s′, g, a), צור אירוע אירוע-B E_t עם:
5) כאשר current_state = s ∧ g
6) אז current_state := s′ ∥ חל (a)
7) קידוד מגבלות נראות באמצעות מגנים שמקורם ב-V(f).
8) להגדיר אינבריאנטים inv1–inv9 כדי ללכוד תכונות בטיחות ועקביות.
9) להגדיר אתחול על ידי הקצאת ערכי S₀ וערכי ברירת מחדל.

קבוצת המצבים, המצב הנוכחי, נראות הפונקציה, מחסנית הקריאה, חותמת זמן העסקה, מצב העברת אתר, דגל קריאה בהאצלה, דגל ההשמדה העצמית ותנאי האימות הם חלק מהמשתנים שנלכדים במודל Event-B. האינבריאנטים (inv1-inv9) ופעולות האתחולים (act1-act6) תואמים לאלו של המפרט הפורמלי. איור 3 מספק גם ייצוג גרפי של האופן שבו האירועים המרכזיים הרלוונטיים לפגיעות, במיוחד מעברים הקשורים לכניסה חוזרת, נשמרים בקידוד Event-B. איור זה מסביר כיצד דפוסי המבנה של מודל FSM-SC המוצגים באיור 2 ממופים לאירועי אירוע-B הניתנים לאימות.

אסטרטגיית שיפור
יושמו שתי רמות של שיפור. זרימת בקרת חוזה ברמה גבוהה ואינווריאנטים ליבה יוצגו ברמה המופשטת. הרמה המשופרת הוסיפה הגבלות ספציפיות לחוזה, כולל הגבלות על מערך השיחות, הגבלות נראות ותנאי מניעת חזרה לכניסה.

אלגוריתם 3: עידון ושחרור הוכחה-התחייבות
קלט: מכונה מופשטת ומכונה מעודנת
פלט: התחייבויות וסטטיסטיקות של הוכחת שחרור

1) ליצור התחייבויות הוכחה עבור המכונה המופשטת ברודין.
2) לבצע הוכחות אוטומטיות מופעלות ולתעד תוצאות שחרור.
3) יצירת התחייבויות עמידה לשיפור עבור המכונה המעודנת.
4) להחיל אישורים אוטומטיים על התחייבויות שיפור.
5) לבצע התחייבויות שנותרו באופן אינטראקטיבי כאשר נדרש.
6) סטטיסטיקות ודוחות סטטוס של הוכחות לייצוא.

דיווח ההוכחות כלל את מספר האינווריאנטים, רמות הזיקוק, התחייבויות הוכחה שנוצרו, קצב פריקה אוטומטית, קצב פריקה אינטראקטיבי וקצב פריקה סופי.

מפרט תכונות CTL ובדיקת מודלים
ההפשטה של FSM-SC תורגמה למודל SMV לאימות זמני בזמן הסתעפות ב-nuXmv.

אלגוריתם 4: FSM ל-SMV ובדיקת CTL
פלט: תוצאת אימות PASS/FAIL ועקבות נגד-דוגמה (אם יש)

1. תיעד מצבי בקרת FSM כמצב משתנה SMV מנוי.
2. להמיר מעברים של FSM להקצאות שמורה ל-next(state).
3. שמירה על דגלים למצבים רלוונטיים לפגיעות, כגון שיחות חיצוניות ועדכוני יתרה.
4. קידוד תכונות CTL ב-nuXmv וביצוע בדיקת מודלים.
5. אם תכונה נכשלת, יצר עקבות נגד-דוגמה המייצגים רצפי מעבר FSM.

בדיקת CTL כללה דרישות לפקודת כניסה מחדש, סיום עדכוני מצב לאחר פעולות העברה, הגבלת כניסה רקורסיבית בלתי מוגבלת לאזורים קריטיים, והימנעות של קיפאון.

מאפייני אבטחה מאומתים
החוזה בסגנון DAO הפשוט שמונע כניסה חוזרת אושר על ידי הבטחת סדר בטוח בין שיחות חיצוניות ועדכוני מצב באמצעות אינבריאנטים ומגבלות CTL. כאשר התאפשר, שומרים אלו בדקו מגבלות בקרת גישה, והבטיחו שמעברים לא מורשים יוגבלו על ידי אינבריאנטים. מודל הספר המוקטן אישר את האינווריאנטים של ייחודיות העסקה ועקביות הספר ברמת המניעה בתוך החוזה.

תוצאות שדווחו
מדור התוצאות מספק דוחות על מדדים מבניים של FSM, מדדי מודל Event-B וסטטיסטיקות להוכחת התחייבות ואימות CTL. תוצאות ההוכחה הפורמלית, ותוצאות בדיקת מודל CTL, ניתנות בנפרד כדי להבחין בין הוכחות לנכונות על ידי אינבריאנטים, לבין ראיות לאימות זמן באמצעות אימות זמני.

הגישה מוגבלת. התחברו או התחילו תקופת ניסיון כדי לצפות בתוכן זה.

תוצאות

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

ממצאי עבודה זו משלבים את מוצרי האימות הפורמליים של בדיקת מודלים של Event-B ו-CTL עם מידע הרצה מסימולציית בלוקצ'יין. השילוב של פלטים רב-שכבתיים אלו תומך באימות התנהגויות מפתח בחוזים חכמים, מערכות הקונצנזוס שלהם, ומגבלות תקינות הספר החשבונות שלהם במסגרת הדוגמה המוגבלת של העיצוב.

הגדרת סביבה ואימות תלות
סביבת ההרצה ששימשה לטרנספורמציית מודל, אימות וסימולציה הושקה ללא קונפליקטים של תלות. באמצעות Web3, NetworkX, Matplotlib, Graphviz, NumPy ו-Pan...

הגישה מוגבלת. התחברו או התחילו תקופת ניסיון כדי לצפות בתוכן זה.

דיון

$$\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 (v2.0.0)FBK (Fondazione Bruno Kessler)https://nuxmv.fbk.eu/בדיקת מודלים סימבוליים של תכונות CTL
Graphviz (v0.20.3)צוות גראפוויזhttps://graphviz.org/ויזואליזציה של FSM ורינדור גרפים
פייתון (v3.10.12)קרן התוכנה של פייתוןhttps://www.python.org/downloadsסביבת סימולציה וביצוע
Web3.py (v7.6.0)קרן את'ריום / תורמיםhttps://web3py.readthedocs.io/אינטראקציה עם בלוקצ'יין וסימולציה של עסקאות
NetworkX (v3.4.2)מפתחי NetworkXhttps://networkx.org/מידול גרפי של בלוקצ'יין ומבני FSM
Matplotlib (v3.8.0)צוות הפיתוח של Matplotlibhttps://matplotlib.org/תכנון זמן כרייה והתפלגויות מאמתים
NumPy (גרסה 1.26.4)מפתחי NumPyhttps://numpy.org/חישובים נומריים
פנדות (v2.2.2)צוות הפיתוח של הפנדותhttps://pandas.pydata.org/ניתוח ועיבוד נתונים
OpenJDK 11קהילת Oracle / 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 Bstake

מאמרים קשורים