גוגל דיפמיינד הציגה את AlphaProof Code, מערכת סוכנים שהפיקה הוכחה מכונתית לליבת ההצפנה של Signal. זה חשוב כי אימות פורמלי של תוכנה אמיתית נחשב עד היום עבודה של שנים, והפעם לפי החברה הוא הושלם בארבעה שבועות.
היעד היה libsignal, ספריית ההצפנה של Signal. לפי דיפמיינד, הסוכנים בדקו את הפרוטוקולים PQXDH ו-Triple Ratchet ברמת קובץ ההרצה המהודר ל-Arm, ולא רק בקוד המקור. ההוכחות נכתבו ב-Lean ומנו יותר משישה מיליון שורות, ורכיב ה-Lean בודק אותן מכנית.
- הסוכנים סימנו כאחוז אחד מהקוד כאזורים הדורשים עין אנושית נוספת.
- כשהחוקרים החזירו שני באגים שתוקנו בעבר, המערכת הפיקה הוכחה שהגרסה הפגיעה אינה בטוחה.
- ההוכחה מכסה שיחות אחד-על-אחד בלבד; הודעות קבוצתיות מוגדרות כעבודה עתידית.
זו מהדורת מחקר ולא API מסחרי. הנתונים הם הצהרת דיפמיינד, ודיווחים שונים נבדלים מעט בספירת השורות המדויקת.
מקורות: Google DeepMind, Axios
₿ אהבת את הפוסט?
אפשר לשלוח לי ביטקוין ישירות לכתובת שלי. סרקו את הקוד, או העתיקו את הכתובת:
bc1qsn043qmlv4ejxydeknkfm9u6e93e6tegmq9x85
שימו לב: העברה on-chain כרוכה בעמלת רשת שאינה תלויה בסכום, ולכן סכומים קטנים מאוד אינם כדאיים.
