בדיקה סמלית עם Halmos: מינוף בדיקות קיימות לאימות פורמלית

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

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

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

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

אימות פורמלי מול בדיקה

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

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

מפרט תקורה

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

ולמרות שבדיקה ואימות פורמלי יכולים לשפר את איכות הקוד כאשר משתמשים בהם יחד, שניהם דורשים (לפעמים דומים) תיאורים של ההתנהגות הצפויה של תוכנית בשפות ובפורמטים שונים. כתיבה ותחזוקה של תיאורים אלה היא עתירת עבודה, ושמירה על שתי צורות שונות של אותו תיאור יכולה להרגיש כמו מאמץ כפול. זה מעלה את השאלה הבאה: האם ניתן לתאר את ההתנהגות הצפויה באופן שמפתחים יכולים להשתמש בו הן לבדיקה והן לאימות?

גישור על הפער בין בדיקה לאימות פורמלית עם בדיקה סמלית והלמוס

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

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

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

דוגמה: בדיקת ה isPowerOfTwo() פונקציה

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

תאר לעצמך את המבחן הבא עבור isPowerOfTwo() פונקציה: היא משווה את הפלט בפועל של הפונקציה עם הפלט הצפוי עבור קלט נתון. זוהי בדיקה בעלת פרמטרים (הידועה גם כבדיקה מבוססת מאפיינים), כלומר ניתן להפעיל אותה בקלות עם ערכי קלט שונים, אולי עם כלים מטושטשים כמו Foundry.

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

עם זאת, Halmos מאפשר למפתחים לעשות שימוש חוזר בבדיקות הקיימות הללו לאימות פורמלית רק עם מעט מאמץ נוסף. הכלי בודק שהבדיקות עוברות עבור כל התשומות האפשריות על ידי ביצוע ביצוע סימבולי של הבדיקה ולאחר מכן מוודא שהטענה לעולם לא מופרת, (או, אם הטענה is הופר, על ידי מתן דוגמה נגדית). המשמעות היא שאם הבדיקה עוברת את Halmos, נכונות הפונקציה מאומתת באופן רשמי, כלומר האלגוריתם מיושם נכון ותורגם במדויק על ידי המהדר לקוד בתים.

הגבלה: ביצוע סימבולי מוגבל

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

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

לדוגמה, שקול את הגרסה האיטרטיבית הבאה של isPowerOfTwo() פונקציה, הכוללת לולאת while unbounded, שבה מספר איטרציות הלולאה נקבע על פי המספר המינימלי של סיביות הנדרשות כדי לייצג את מספר הקלט.

Halmos חוזר באופן סמלי על הלולאה הבלתי מוגבלת הזו רק עד לתחום מסוים. לדוגמה, אם הגבול מוגדר ל-3, Halmos יחזור על הלולאה 3 פעמים לכל היותר ולא ישקול ערכי קלט שיגרמו ללולאה לחזור על יותר מ-3 פעמים (כלומר, כל ערכים הגדולים או שווים ל-2^3 ). במקרה הספציפי הזה, הגדרת הגבול ל-256 ומעלה תאפשר ל-Halmos להיות שלם.

הדגמה: אימות רשמי של ERC721A עם Halmos

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

מאפייני בדיקה סימבוליים

מכיוון שהבדיקות הקיימות עבור ERC721A נכתבו ב-JavaScript עם Hardhat (שאיננה נתמכת כרגע על ידי Halmos), כתבנו מבחנים חדשים ב-Solidity עבור פונקציות נקודת הכניסה הראשיות: mint(), burn(), ו transfer(). בדיקות אלו בדקו שכל פונקציה מעדכנת בצורה נכונה את הבעלות והיתרה של טוקנים, ומשפיעה רק על המשתמשים הרלוונטיים מבלי לשנות את היתרה או הבעלות של משתמשים אחרים. זה האחרון אינו טריוויאלי להוכחה עקב השימוש באלגוריתם מבנה הנתונים העצל ב-ERC721A. לדוגמה, הבדיקה הבאה בודקת שה- transfer() הפונקציה מעדכנת בצורה נכונה את הבעלות על האסימון שצוין:

בדיקה נוספת בודקת שה transfer() הפונקציה אינה משנה את האיזון עבור כתובות אחרות, אשר מאתגר להוכיח כפי שהוזכר קודם לכן:

תוצאות אימות

ערכנו ניסוי אימות באמצעות Halmos על החוזה החכם ERC721A על ידי כתיבת סך של 19 בדיקות. המבחנים בוצעו דרך Halmos עם סף לולאה של 3, שלקח 16 דקות להשלים. ניתן לראות את פירוט זמן האימות בטבלה למטה. הניסוי נערך על מקבוק פרו עם שבב M1 Pro וזיכרון של 16 ג'יגה-בייט.

מִבְחָן	זמן (ים)
testBurnBalanceUpdate	6.67
testBurnNextTokenIdUnchanged	1.40
testBurnOtherBalancePreservation	5.69
testBurnOwnershipPreservation	189.70
testBurnOwnershipUpdate	3.81
testBurn Requirements	71.95
testMintBalanceUpdate	0.20
testMintNextTokenIdUpdate	0.18
testMintOtherBalancePreservation	0.26
testMintOtherOwnershipPreservation	5.74
testMintOwnershipUpdate	1.38
testMintRequirements	0.09
testTransferBalanceUnchanged	9.03
testTransferBalanceUpdate	53.53
testTransferNextTokenIdUnchanged	4.47
testTransferOtherBalancePreservation	19.57
testTransferOwnershipPreservation	430.61
testTransferOwnershipUpdate	18.71
testTransfer Requirements	149.18

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

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

ניסוי עם באגים שהוזרקו

כדי להדגים את היעילות של ההיגיון התחום של Halmos, השתמשנו בו כדי לזהות באגים בגרסה קודמת של חוזה ERC721A. לגרסה זו הייתה בעיה שלא טיפלה בהצפה אריתמטית ואפשרה פוטנציאל להטביע מספר רב של אסימונים, מה שעלול לשבור את שלמות מבנה הנתונים העצל ולגרום לחלק מהמשתמשים לאבד את בעלות האסימון שלהם (בעיה נפתרה בגרסה הנוכחית). הרצנו את אותה קבוצה של 19 בדיקות עבור ERC721A בגרסת הבאגי, והלמוס הצליח למצוא דוגמה נגדית למאפיינים של mint() פוּנקצִיָה. באופן ספציפי, Halmos סיפק ערכי קלט שהובילו לתרחיש הניצול שתואר לעיל. תוצאות הניסוי הזה מצביעות על כך שלמרות חוסר השלמות שלו, ההיגיון התחום של Halmos יכול להיות דרך יעילה לאיתור ומניעת באגים שניתנים לניצול בחוזים חכמים.

עבודה קשורה

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

בעוד Halmos הוא תוספת חשובה למערכת הכלים הזמינה לאימות חוזים חכם, היא נועדה להשלים (לא להחליף) כלים קיימים. מפתחים יכולים לשלב את Halmos עם כלים אחרים כדי להשיג רמת ביטחון גבוהה יותר בחוזים שלהם. להלן, אנו משווים את Halmos עם כמה כלים רשמיים נבחרים התומכים ב-EVM bytecode.

• K היא מסגרת אימות פורמלית רבת עוצמה המאפשרת אימות דדוקטיבי והוכחת משפט אינטראקטיבי. התיאוריה והיישום הבסיסיים שלו מספקים רמה גבוהה של כושר ביטוי, מה שהופך אותו למתאים לאימות תוכניות ואלגוריתמים מורכבים. עם זאת, יש לציין כי K אינו מתוכנן עם דגש רב על אימות אוטומטי וחסר תכונות אוטומציה מסוימות אשר עשויות לדרוש מאמץ ידני יותר במהלך תהליך האימות. כדי להשתמש במסגרת K, מפרטים פורמליים נכתבים בשפת K, אותם יש ללמוד לפני השימוש. כוחו שימושי במיוחד באימות מערכות מורכבות, אשר עשוי להיות מאתגר לניתוח באמצעות חשיבה אוטומטית.
• צרטורה הוא כלי אימות רשמי לחוזים חכמים המתמקד באימות אוטומטי ותומך בבדיקת מודלים מוגבלים, בדומה ל-Halmos. כדי להשתמש ב-Certora, מפתחים חייבים ללמוד את השפה החדשה שלהם, CVL, על מנת לכתוב מפרטים. שפה זו מאפשרת תיאור תמציתי של מאפיינים קריטיים רבים באמצעות אינוריאנטים של חוזים, תכונה שבה Halmos אינה תומכת כיום. למרות היותו כלי קנייני במקור סגור, Certora מספקת כלי אימות פורמליים חזקים, עם פיתוח מתמשך ותמיכה טובה במשתמשים.
  
  Halmos, לעומת זאת, הוא כלי קוד פתוח שהוא קטן יותר בקנה מידה וחסר כרגע כמה תכונות מסופקות על ידי Certora, אבל הוא נועד לשמש כטובת הציבור ונועד כפתרון נישה לאימות מהיר של חוזים חכמים ללא הצורך בהתקנה ותחזוקה נרחבים.
• HEVM הוא כלי אימות פורמלי נוסף הדומה ל-Halmos. זה היה בעבר חלק מ-DappTools, שהוא מבשר של Foundry. גם ל-HEVM וגם ל-Halmos יש את התכונה שהם לא דורשים מפרט נפרד ויכולות לבצע באופן סמלי בדיקות קיימות כדי לזהות הפרות טענה. זה מאפשר למשתמשים להשתמש בשני הכלים לסירוגין או להפעיל אותם במקביל לאותן מבחנים, ומספק להם אפשרויות מרובות לבדיקה סמלית.
  
  ראוי לציין שלמרות הדמיון ביניהן, HEVM והלמוס פותחו באופן עצמאי ונבדלים בפרטי היישום שלהם; במיוחד במונחים של אופטימיזציות ואסטרטגיות חשיבה סימבולית. בנוסף, HEVM כתוב ב-Haskell, בעוד Halmos כתוב ב-Python, מה שמספק חשיפה לאקוסיסטם האקולוגי העשיר של Python. היכולת להשתמש בשני הכלים מעניקה למשתמשים יותר גמישות ואפשרויות להבטיח את האבטחה והנכונות של חוזים חכמים.

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

**

הדעות המובעות כאן הן אלה של אנשי AH Capital Management, LLC ("a16z") המצוטטות ואינן הדעות של a16z או החברות הקשורות לה. מידע מסוים הכלול כאן התקבל ממקורות צד שלישי, כולל מחברות פורטפוליו של קרנות המנוהלות על ידי a16z. למרות שנלקחה ממקורות האמינים כאמינים, a16z לא אימתה מידע כזה באופן עצמאי ואינה מציגה מצגים לגבי הדיוק הנוכחי או המתמשך של המידע או התאמתו למצב נתון. בנוסף, תוכן זה עשוי לכלול פרסומות של צד שלישי; a16z לא סקרה פרסומות כאלה ואינה תומכת בתוכן פרסומי כלשהו הכלול בהן.

תוכן זה מסופק למטרות מידע בלבד, ואין להסתמך עליו כייעוץ משפטי, עסקי, השקעות או מס. עליך להתייעץ עם היועצים שלך באשר לעניינים אלה. הפניות לניירות ערך או לנכסים דיגיטליים כלשהם נועדו למטרות המחשה בלבד, ואינן מהוות המלצת השקעה או הצעה לספק שירותי ייעוץ השקעות. יתר על כן, תוכן זה אינו מכוון ואינו מיועד לשימוש על ידי משקיעים או משקיעים פוטנציאליים כלשהם, ואין להסתמך עליו בשום פנים ואופן בעת ​​קבלת החלטה להשקיע בקרן כלשהי המנוהלת על ידי a16z. (הצעה להשקעה בקרן a16z תתבצע רק על ידי מזכר ההנפקה הפרטית, הסכם המנוי ותיעוד רלוונטי אחר של כל קרן כזו ויש לקרוא אותה במלואה). המתוארים אינם מייצגים את כל ההשקעות בכלי רכב המנוהלים על ידי a16z, ואין כל ודאות שההשקעות יהיו רווחיות או שלהשקעות אחרות שיבוצעו בעתיד יהיו מאפיינים או תוצאות דומות. רשימה של השקעות שבוצעו על ידי קרנות המנוהלות על ידי אנדריסן הורוביץ (למעט השקעות שעבורן המנפיק לא נתן אישור ל-a16z לחשוף בפומבי וכן השקעות בלתי מוקדמות בנכסים דיגיטליים הנסחרים בבורסה) זמינה בכתובת https://a16z.com/investments /.

תרשימים וגרפים המסופקים בתוכן הם למטרות מידע בלבד ואין להסתמך עליהם בעת קבלת החלטת השקעה כלשהי. ביצועי העבר אינם מעידים על תוצאות עתידיות. התוכן מדבר רק לתאריך המצוין. כל תחזיות, אומדנים, תחזיות, יעדים, סיכויים ו/או דעות המובעות בחומרים אלו כפופים לשינויים ללא הודעה מוקדמת ועשויים להיות שונים או מנוגדים לדעות שהובעו על ידי אחרים. אנא ראה https://a16z.com/disclosures למידע חשוב נוסף.