Google DeepMind השתמשה בבינה מלאכותית סוכנית כדי לאמת פורמלית את פרוטוקול Signal

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

מה מצא הניתוח

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

למה אימות פורמלי חשוב

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

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

עדיין לא ברור עד כמה יהיה מעשי אימות פורמלי בסיוע בינה מלאכותית לשימוש נרחב, ועד כמה הוא יהיה יעיל באבטחת כמויות גדולות של קוד. DeepMind ערכה את הניתוח של Signal ללא תשלום, כפרויקט מחקר, ו-Google סירבה לחשוף את עלות הניתוח או להתייחס לשאלה אם יש לה תוכניות להשיק מוצר או שירות מסחרי לאימות פורמלי. Ehren Kret, מנהל הטכנולוגיות הראשי של Signal, אומר בהצהרה כי אימות פורמלי קודם התמקד בחלקים קטנים יותר של הקוד, ואילו הגישה של Google DeepMind מאפשרת הרחבה משמעותית. "ככל שאיומי האבטחה שמונעים על ידי בינה מלאכותית גדלים, אימות קפדני של יישום פרוטוקול Signal מעניק לנו ביטחון רב עוד יותר בהבטחות הפרטיות של הקוד שלנו", אומר Kret. Pushmeet Kohli, המדען הראשי של Google Cloud וסגן נשיא המחקר ב-DeepMind, אומר שאם אפשר כעת לאמת את נכונות היישומים, חברות שנשענות על הבטחות וחוששות מבאגים יוכלו לומר שהן מסוגלות להוכיח את התכונות האלה. Chaudhuri אומר ש-DeepMind נרגשת מהתוצאה, אך עוד דרך ארוכה לפני שאפשר להרחיב זאת לכל התוכנה בעולם.

מקורות: Wired