גוגל דיפמיינד השתמשה ב-AI כדי להוכיח מתמטית כמה מהבטחות האבטחה המרכזיות של פרוטוקול Signal

חוקרים ב-Google DeepMind השתמשו ב-agentic AI, כלומר מערכות AI שפועלות באופן עצמאי לאורך תהליך רב-שלבי, כדי להוכיח מתמטית כמה מהבטחות ההצפנה המרכזיות של פרוטוקול Signal. התהליך הזה נקרא "אימות פורמלי" (formal verification). העבודה נעשתה כפרויקט הדגמה (proof-of-concept) ונמשכה ארבעה שבועות בלבד, כך מדווח WIRED. היא מתבססת על כלי חדש של החברה בשם AlphaProof Code.

למה זה חשוב

פרוטוקול Signal הוא לא רק הבסיס של אפליקציית Signal. הוא מגן גם על כמויות עצומות של תקשורת בפלטפורמות כמו WhatsApp ו-Google Messages. לכן המחקר משמש עוד אימות בלתי תלוי לקריפטוגרפיה שמיליוני אנשים סומכים עליה כל יום, ובמקביל מציג את יכולות האימות הפורמלי החדשות של דיפמיינד.

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

מה נמצא, ומה לא נבדק

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

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

"בעוד שאימות פורמלי קודם התמקד בחלקים קטנים יותר של הקוד, הגישה של Google DeepMind מאפשרת הרחבה משמעותית", אמר ארן קרט (Ehren Kret), סמנכ"ל הטכנולוגיות של Signal, בהצהרה. "ככל שאיומי האבטחה מבוססי ה-AI גדלים, אימות קפדני של מימוש פרוטוקול Signal נותן לנו ביטחון רב עוד יותר בהבטחות הפרטיות של הקוד שלנו".

השאיפה: כל התוכנה בעולם

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

פושמיט קוהלי (Pushmeet Kohli), המדען הראשי של Google Cloud וסגן נשיא למחקר בדיפמיינד, מתאר חזון רחב עוד יותר: "אם אפשר עכשיו לאמת את הנכונות של המימושים האלה, אפשר לישון בשקט. תחשבו על בנקים, על כל החברות האחרות שתלויות באישורים ודואגות מבאגים, שיוכלו עכשיו לומר: 'אני יכול להוכיח את התכונות האלה'".

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

השאלה הפתוחה: עלות והיקף

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

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