Google DeepMind informuje o formalnej weryfikacji kodu maszynowego protokołu Signal za pomocą AlphaProof Code

Pushmeet Kohli z Google DeepMind ogłosił, że jego zespół udowodnił kluczowe właściwości bezpieczeństwa kodu maszynowego stanowiącego podstawę komunikatora Signal. DeepMind twierdzi, że to pierwszy przypadek, w którym kod produkcyjny powszechnie używanego protokołu został formalnie zweryfikowany dowolną metodą na tak szczegółowym poziomie. Są to własne twierdzenia DeepMind.

Do pracy wykorzystano AlphaProof Code — opisywany przez DeepMind jako nowy agentowy framework do formalnej weryfikacji, działający w oparciu o LLM-y, w tym Gemini Carbon. DeepMind twierdzi, że weryfikacja obejmuje kod uruchamiany na urządzeniach i zajęła około miesiąca, podczas gdy podobne przedsięwzięcia mogłyby wymagać łącznie dekad pracy zespołów. DeepMind wymienia zespół Signal jako partnera.

DeepMind udostępnia na otwartej licencji formalne specyfikacje i artefakty weryfikacji, aby inni mogli na nich bazować. Do rana 10 listopada post miał 1 297 polubień na X.