AlphaProof Code: הוכחות לתכונות אבטחה בקוד של libsignal
לפי Google DeepMind, סוכני AlphaProof Code הוכיחו תכונות אבטחה מוגדרות במימוש libsignal עד לרמת קוד המכונה, עם כ־6.5 מיליון שורות הוכחה שנבדקו ב־Lean.
Google DeepMind הציגה ב־10 בנובמבר את AlphaProof Code, מערכת סוכני AI שהוכיחה תכונות אבטחה מרכזיות במימוש libsignal, עד לרמת קוד המכונה. לפי הפרסום, התוצאה כוללת כ־6.5 מיליון שורות הוכחה שנבדקו ב־Lean. זו התפתחות מחקרית בשאלה האם AI יכול לעזור לא רק לייצר תוכנה, אלא גם לספק ראיות לכך שהקוד מקיים דרישות אבטחה מוגדרות.
מה הוכח: מהתכנון התאורטי אל המימוש
ההבחנה החשובה בסיפור היא בין תכנון בטוח לבין קוד שמממש אותו כראוי. אפשר לנתח מנגנון אבטחה ולהראות שהוא עומד בדרישות מסוימות, אך התוכנה שמפעילה אותו כוללת פרטי מימוש שעלולים לסטות מהתכנון. המחקר של DeepMind מתמקד בפער הזה: לא להסתפק בנכונות של רעיון מופשט, אלא לבדוק תכונות של המימוש בפועל.
לפי התחקיר, האימות מגיע עד לרמת קוד המכונה. המשמעות היא שהטענה המחקרית אינה נעצרת בתיאור עילי של האלגוריתם. עם זאת, כדי להבין בדיוק מה מכוסה צריך לקרוא את המפרט הטכני: אילו תכונות נוסחו, איזה קוד נכלל ואילו הנחות נדרשות כדי שההוכחות יחולו. עצם האזכור של קוד מכונה אינו תשובה לכל השאלות האלה.
גם היקף ההוכחה דורש פרשנות זהירה. כ־6.5 מיליון שורות הן נתון על היקף תוצר ההוכחה, לא מספר החולשות שנחסמו ולא מדד ישיר לרמת האבטחה של האפליקציה. הערך תלוי בראש ובראשונה בחשיבות הטענות שהוכחו ובקשר שלהן להתנהגות שהתוכנה אמורה לקיים.
למה Lean משנה את אופן בדיקת התוצאה
Lean הוא כלי לאימות פורמלי, שבו אפשר לנסח טענות ולבדוק הוכחות במסגרת לוגית מוגדרת. בשונה מתשובה מילולית של מודל, שנשמעת לעיתים משכנעת גם כשהיא שגויה, הוכחה פורמלית חייבת לעמוד בכללי הבדיקה. כאן נמצאת נקודה מרכזית בשימוש בסוכני AI: אפשר להפריד בין המערכת שמציעה את ההוכחה לבין המנגנון שבודק אותה.
ההפרדה הזאת אינה מעלימה את הצורך באמון, אלא משנה את המקום שבו הוא נדרש. עדיין צריך לבחון את הגדרות הבעיה, את ההנחות ואת סביבת האימות. אבל אין צורך להסתפק בהצהרה של הסוכן שהוא הצליח. תוצר העבודה שלו ניתן לבדיקה לפי כללים מפורשים, וזה הבדל מהותי לעומת סקירת קוד שמסתיימת בהסבר חופשי.
הוכחה שהקוד מקיים מפרט אינה הוכחה שהמפרט מכסה כל איום.
לכן השאלה המחקרית אינה רק כמה הוכחות AI מסוגל לכתוב. חשוב לבדוק גם כמה עבודה אנושית נדרשת כדי להגדיר את הטענות, להכין את סביבת הבדיקה ולתחזק את התוצאה. התחקיר המצורף אינו מספק נתונים שמאפשרים לכמת את החיסכון הזה, ולכן מוקדם להסיק שהשיטה כבר זולה או פשוטה להטמעה בכל צוות פיתוח.
מה המחקר לא אומר על Signal
הניסוח המדויק הוא שהוכחו תכונות אבטחה מרכזיות במימוש libsignal בתחום שנבדק. אין כאן בסיס לטענה שכל אפליקציית Signal נטולת חולשות. אפליקציה פועלת בתוך מערכת רחבה של רכיבים, ממשקים ומכשירים, והוכחה שנוגעת לרכיב או לתכונה מסוימת אינה מתרחבת אוטומטית לכל סביבת השימוש.
אין לפרש את ההכרזה כאישור גורף לבטיחות Signal. לפני שמסיקים מסקנה מעשית, צריך לזהות את התכונות שהוכחו, את גבולות הקוד שנבדק ואת ההנחות שעליהן נשענת ההוכחה.
למשל, הוכחה על התנהגות קוד אינה כשלעצמה הגנה מפני מכשיר שנפרץ או משתמש שמוסר מידע לגורם מתחזה. אלה דוגמאות לגבולות אפשריים של אימות תוכנה, ולא דיווח על חולשות שהתגלו במחקר. באותה מידה, אין להניח שתוצאה המתייחסת למימוש שנבדק תחול ללא בדיקה נוספת לאחר שינוי בקוד או בסביבת ההרצה.
גם היחס לבדיקות מסורתיות צריך להישאר ענייני. בדיקות יחידה, fuzzing וסקירות אבטחה בוחנים היבטים שונים של התנהגות התוכנה. אימות פורמלי יכול להוסיף להם שכבת ראיות חזקה ביחס לטענות מסוימות, אך אינו סיבה להפסיק לחפש בעיות מחוץ למסגרת שהוגדרה.
המשמעות לישראל: להתחיל מדרישה שאפשר להגדיר
למשתמש בישראל, המחקר אינו מצביע כשלעצמו על צורך לשנות את אופן השימוש ב־Signal. עבור צוותי פיתוח בחברות סייבר, פינטק ובריאות, הוא מציע כיוון מעשי יותר: לבחון אם יש במוצר רכיב רגיש שבו הדרישה ברורה מספיק כדי לנסח אותה פורמלית. נקודת פתיחה סבירה אינה הבטחה להוכיח מוצר שלם, אלא טענה ממוקדת שאפשר לבדוק.
- בחרו תכונה בעלת משמעות עסקית ואבטחתית, כגון כלל הרשאה מוגדר, במקום יעד עמום כמו ״מערכת בטוחה״.
- תעדו את ההנחות: על אילו קלטים, רכיבים ותנאי הפעלה מסתמכת הטענה.
- דרשו תוצר שניתן לבדיקה, ולא רק הסבר של סוכן AI שלפיו הקוד תקין.
- תכננו מה קורה אחרי שינוי בקוד: מי מעדכן את המפרט ומי מוודא שההוכחה עדיין רלוונטית.
אלה עקרונות לבחינת הכיוון המחקרי, לא תיאור של שירות מסחרי שהוכרז כזמין. התחקיר אינו קובע ש־AlphaProof Code מוצע כעת לשימוש חיצוני, וגם אינו מספק מחיר או מסלול הטמעה. עסק ישראלי שבוחן אימות פורמלי צריך לכן להפריד בין ההישג המחקרי לבין זמינות הכלים והכישורים הנדרשים ליישום אצלו.
מה כדאי לבדוק בהמשך
השלב הבא בהערכת המחקר הוא בחינת גבולותיו, לא הרחבת הכותרת. כדאי לחפש פירוט של המפרט, ההנחות, היכולת לשחזר את התוצאות והעבודה הנדרשת בעקבות עדכון תוכנה. שאלות נוספות הן עד כמה השיטה עוברת לרכיבים אחרים, ואיך נראית חלוקת העבודה בין החוקרים לסוכנים כאשר ההוכחה אינה מתקבלת.
AlphaProof Code מציג כיוון שונה מהמרוץ לכתיבת עוד קוד: שימוש ב־AI ליצירת ראיות על קוד קיים. ההישג המדווח ממוקד ומשמעותי דווקא כששומרים על גבולותיו. הוא אינו מבטיח תוכנה חסינה, אלא מראה כיצד סוכנים יכולים להשתלב בתהליך שבו טענות אבטחה מוגדרות עוברות בדיקה פורמלית.
שאלות נפוצות
מה זה AlphaProof Code?
AlphaProof Code היא מערכת סוכני AI שהציגה Google DeepMind ב־10 בנובמבר 2026. לפי התחקיר, המערכת הוכיחה תכונות אבטחה מרכזיות במימוש libsignal עד לרמת קוד המכונה, באמצעות כ־6.5 מיליון שורות הוכחה שנבדקו ב־Lean.
האם המחקר מוכיח שאפליקציית Signal בטוחה לחלוטין?
לא. ההוכחה חלה על התכונות שהוגדרו, על התחום שנבדק ותחת ההנחות של האימות. אין להסיק ממנה שכל אפליקציית Signal, המכשיר שעליו היא פועלת או כל גרסה עתידית נטולי חולשות.
מה ההבדל בין אימות פורמלי לבדיקות אבטחה רגילות?
בדיקות תוכנה בוחנות התנהגות במקרים מסוימים, ואימות פורמלי מבקש להוכיח טענה מוגדרת במסגרת מתמטית. השיטות משלימות זו את זו: גם הוכחה תקפה אינה מגינה מפני סיכון שלא נכלל במפרט או נמצא מחוץ לתחום שנבדק.
דרגו את הכתבה
הדירוג עוזר לנו לדעת מה שווה לכם.
תגובות