Google DeepMind обяви на 10 ноември, че с AI агенти е доказала математически сигурността на кода, който стои зад криптирането в Signal – протокола, който пази и чатовете в Google Messages. Досега подобна проверка на толкова широко използван криптографски протокол е отнемала на експертни екипи години, а новата система AlphaProof Code се справя за около четири седмици.
Накратко
- Проверен е реалният код на Signal, който работи на устройствата, а не само описанието на протокола.
- Агентите са написали над 6 милиона реда доказателства, а хора са прегледали около 1% от кода.
- При тест системата хваща два стари, вече поправени пробива, върнати нарочно в кода.
Какво точно е доказано
Обикновено сигурността на един протокол се проверява на хартия: математиците доказват, че идеята е правилна. Пробивите в реалния живот обаче често се крият другаде – в разликата между това, което пише в научната статия, и това, което програмистите реално са написали. Затова DeepMind е насочила проверката към самия код.
Според блога на Google DeepMind доказателствата покриват компилирания машинен код, който се изпълнява на устройствата, и ключови свойства на сигурността. Едно от тях е, че съобщенията остават защитени преди и след като устройството е било временно компрометирано – например ако някой е получил достъп до телефона за кратко.
DeepMind определя резултата като първия случай, в който AI проверява формално толкова широко внедрен криптографски протокол на това ниво. Според компанията това е и първата формална проверка на реалната реализация на такъв протокол с какъвто и да е метод.
Как работи AlphaProof Code
Системата разделя работата между хора и машини. Експертите решават какво трябва да се докаже, а агентите, задвижвани от модела Gemini 4 Carbon, пишат доказателствата на Lean – език, в който всяко доказателство се проверява механично. Ако агентът сгреши, Lean просто отхвърля резултата, така че на самия AI не се налага да се вярва на думата.
Процесът има три части. Първо агент превръща научните статии за протокола в точна спецификация, която човек одобрява. После кодът на Signal, написан на Rust, се превежда в модел, който Lean може да изпълни. Накрая екип от агенти доказва, че кодът отговаря на спецификацията, а Lean играе ролята на пазач на входа.
Резултатът е над 6 милиона реда доказателства. Агентите сами са отбелязали около 1% от кода, който човек трябва да провери ръчно, а останалото е потвърдено автоматично. Артефактите от проверката DeepMind публикува отворено за общността.
Тестът със старите пробиви
Доказателство, че нещо е сигурно, има стойност само ако методът може да различи и несигурния код. Затова екипът е върнал два стари, отдавна поправени пробива в отделно копие на кода на Signal. И в двата случая системата е стигнала до машинно проверено доказателство, че версията е уязвима.
Самият Signal е участвал в процеса – трима души от компанията са давали обратна връзка по методиката. „Да използваш AI агенти, за да превърнеш работещ код във валидни теореми на Lean, е голям пробив“, казва техническият директор на Signal Ерен Крет, цитиран от DeepMind.
Какво означава това за чатовете ви във Viber, WhatsApp и Messages
Новината е добра за всеки, който пише в Signal или Google Messages – математически е потвърдено, че криптирането им е изградено правилно. Протоколът на Signal е в основата и на криптирането в WhatsApp, както припомня 9to5Mac. Проверен обаче е кодът на Signal, а WhatsApp използва собствена реализация, така че за нея същото доказателство не важи директно. Viber има собствена реализация на криптирането и също не е част от изследването.
Има и по-важна уговорка. Сигурният протокол пази съобщенията по пътя, но не и телефона. Ако някой ви измами да инсталирате фалшиво приложение, види кода ви за вход или получи достъп до отключения ви телефон, никакво криптиране не помага. Затова основните навици остават същите:
- обновявайте приложенията за чат и системата на телефона веднага щом излезе ъпдейт;
- сваляйте приложенията само от официалния магазин – видяхме как фалшив WhatsApp събра 500 000 сваляния;
- включете двуфакторната проверка (PIN за регистрация) в WhatsApp и Signal;
- не пращайте кодове за вход на никого, дори да ви пише „приятел“.
Защо това е повече от рекламен успех за Google: същите AI модели, които днес помагат и на хакерите – като в случая с армията от AI агенти, пробила над 100 сайта, тук правят обратното – доказват, че пробив няма. Самите изследователи признават, че методът е изключително скъп откъм изчисления и мащабирането му към целия софтуер в света изисква още работа. Ако обаче цената падне, формалната проверка може да стане стандарт за банкови приложения, системи за вход и всичко, което пази лични данни.
Signal не е чужд на спорове за поверителността – по-рано този есен приложението заплаши да напусне Канада заради законопроект за достъп до съобщенията. Още за сигурността и рисковете при изкуствения интелект четете в рубриката AI рискове.
