אנתרופיק הציגה את תוצאות הניסויים שהשתמשו במודלים של בינה מלאכותית כדי לאמת באופן רשמי את האמינות והאבטחה של פרויקטים קיימים. במהלך הניסוי, נעשה שימוש במודלים של בינה מלאכותית כדי ליצור הוכחות מתמטיות להיעדר שגיאות זיכרון עבור 123 ספריות קוד פתוח שנבדקו בתשתית OSS Fuzz.
האימות בוצע ברמת קוד האסמבלי שעבר קומפילציה עבור ארכיטקטורת RISC-V. נפח ההוכחות הכולל שנוצר הסתכם בכ-180 מיליון שורות קוד עבור מערכת האימות Rocq Prover (כ-600 שורות לכל קובץ בינארי עם 18 הוראות RISC-V). ההוכחות נוצרו על ידי המרה אוטומטית של מבחני fuzzing קיימים למפרטים פורמליים, ולאחר מכן מודל הבינה המלאכותית של קלוד הוכיח שהתוכנית נטולת תקלות עבור כל נתוני קלט עד 64 מגה-בייט.
במהלך תהליך בניית ההוכחה, מודל הבינה המלאכותית היה מסוגל לזהות ולהכין תיקונים למאות באגים שלא זוהו בעבר על ידי בדיקות fuzz. בין היתר, אלה כללו פגיעויות של overflow (גליפת מאגר) בעת עיבוד נתוני קלט מסוימים (למשל, CVE-2026-56132 ב-libexpat), כמו גם שגיאות לוגיות. יתר על כן, מודל הבינה המלאכותית שימש להוכחת תאימות של יישום האלגוריתם zlib על ידי הליבה. Linux מפרט RFC 1950.
מפרש עבור תת-קבוצה של Python נוצר גם ב-Rust, עבורו הוכנה הוכחה רשמית של תאימות לסמנטיקה של CPython באמצעות ערכת הכלים Verus. כדי להשוות את ההתנהגות עם CPython, בוצעו מעל 1.7 מיליון תוכניות Python שנוצרו באופן אקראי. ב-99.95% מהמקרים, תוצאות ביצוע התוכניות הללו במימוש החדש וב-CPython תאמו, וכל פער שנמצא היה מקרי קצה ידועים.
אימות פורמלי מבטיח עמידה במפרט, אך אינו מבטל לחלוטין בעיות אבטחה, שכן סיכונים הנגרמים מבעיות ריבוי הליכים, קישור דינמי והתנהגות חריגה בחומרה אמיתית נותרים בלתי פורמליים. יתרון מרכזי של הגישה המוצעת הוא שהיא עובדת ישירות עם קבצים בינאריים, ובכך מבטלת את הצורך לכתוב מחדש קוד קיים בשפות הניתנות לאימות פורמלית.
מקור: OpenNet.ru
