Signal: wat d’KI wierklech iwwer säi Code bewisen huet

Google DeepMind behaapt, AlphaProof Code agesat ze hunn, fir verschidde Properties vum kompiléierte Code vu libsignal ze beweisen. D’Resultat weist d’Potenzial vun der KI, awer och déi genee Grenze vun engem formelle Beweis.

Fir ze bewäerten, ob eng Software Messagen korrekt verschlësselt, geet et net duer, Tester ze lafen an hiert Verhalen an e puer Situatiounen ze beobachten. Et muss een och mat enger iwwerpréifbarer Begrënnung noweise kënnen, datt verschidde Properties an allen Ausféierungen, déi vum Modell erfaasst ginn, gëllen. Google DeepMind behaapt, säi System AlphaProof Code agesat ze hunn, fir dës Aarbecht um kompiléierte Code vum Signal-Protokoll ze maachen – mat KI-Agenten an dem Beweisverifizéierer Lean.

D’Experiment betrëfft spezifesch kryptographesch Garantien, net déi absolut Sécherheet vun der Signal-App. Et weist virun allem, wéi d’KI un enger usprochsvoller formeller Verifikatioun matwierke kann, wärend wichteg Entscheedungen de Fuerscher iwwerlooss ginn an déi definitiv mathematesch Kontroll enger spezialiséierter Software uvertraut gëtt.

Vum kryptographesche Modell zum ausgeféierte Code

E Verschlësselungsprotokoll beschreift d’Reegelen, déi zum Beispill en Austausch schützen an d’Gespréichspartner authentifizéieren. Mee eng korrekt Konzeptioun geet net duer: De Programm, deen se ëmsetzt, kann e Feeler enthalen. Bei der formeller Verifikatioun gëtt mathematesch nogewisen, datt de Code definéiert Properties erfëllt – ënner Viraussetzungen, déi och ausdrécklech festgehale sinn.

DeepMind seet, datt si um kompiléierte Code vu libsignal geschafft hunn, der Bibliothéik, déi de Signal-Protokoll ëmsetzt. Dëse Schrëtt ass wichteg: D’Team huet sech net mat enger theoretescher Beschreiwung vum Protokoll zefridde ginn, mee probéiert, Sécherheetsgarantien mam Code ze verbannen, deen no der Kompiléierung entsteet.

De System mam Numm AlphaProof Code deelt d’Aarbecht tëscht verschiddene Modeller an Agenten op. Der vu Google DeepMind verëffentlechter Beschreiwung no hunn d’Fuerscher fir d’éischt d’Sécherheetsziler a mathematesch Spezifikatiounen iwwersat. Duerno hunn Agenten, déi vu Gemini ugedriwwe goufen, formell Beweiser opgebaut. Am Blogartikel vun DeepMind ass vu méi wéi sechs Millioune produzéierte Linnen an der Sprooch Lean rieds. Dëse Volume heescht net, datt d’KI sechs Millioune Linne Software geschriwwen huet: Et handelt sech ëm Artefakter, déi dozou déngen, d’Beweiser ze formaliséieren an ze verifizéieren.

Wat Lean verifizéiert – a wat d’Fuerscher decidéieren

Lean ass e Beweisassistent. E kontrolléiert, ob e Beweis de logesche Reegelen vum System entsprécht an d’formuléiert Resultat tatsächlech beweist. E decidéiert awer net eleng, ob déi gewielte Properties all Erwaardunge vun engem Benotzer entspriechen oder ob d’Ufanksviraussetzungen d’reell Welt korrekt beschreiwen.

Dësen Ënnerscheed ass zentral. D’Experten hu bei der Festleeung vun deem matgeschafft, wat bewisen sollt ginn, a laut DeepMind och d’Spezifikatioune gelies. D’Agenten hunn duerno méiglech Beweisweeër exploréiert, wärend Lean hir formell Gültegkeet kontrolléiert huet. De System kann esou en Deel vun der Aarbecht, fir e Beweis ze fannen, reduzéieren. De Kader vum Beweis bleift awer eng mënschlech Entscheedung.

E formelle Beweis ass also keen universellen Audit. Wann eng Property net an de Spezifikatioune steet, gëtt se vum Beweis net ofgedeckt. Wann eng kryptographesch Funktioun als sécher ugesi gëtt, ouni datt hir Implementéierung verifizéiert gëtt, bleift dës Viraussetzung ausserhalb vum Resultat. Déi korrekt Conclusioun ass bedéngt: De Code erfëllt déi formaliséiert Properties, am festgeluechte Kader an ënner de gewielte Viraussetzungen.

Véier Wochen, zwee nei agebaute Bugs

DeepMind deelt mat, datt d’Experiment véier Wochen gedauert huet. Fir ze testen, ob d’Method konforme Code vun enger feelerhafter Versioun ënnerscheede kann, huet d’Team och zwee bekannte Bugs, déi virdru gefléckt gi waren, an eng isoléiert Versioun vum Code nees agebaut. Der Entreprise no huet de System dunn maschinnverifizéiert Beweiser geliwwert, déi gewisen hunn, datt dës Varianten déi iwwerpréifte Garantien net méi erfëllt hunn.

Dësen Test ass nëtzlech, well en d’Method mat konkrete Feeler konfrontéiert, amplaz nëmmen ze moossen, ob si e Beweis fir eng korrekt Versioun produzéiere kann. Mee en ass keng Detektiounsquot, déi sech allgemeng iwwertrage léisst: Zwee nei agebaute Feeler representéieren weder all Kategorien vu Schwachstellen nach all Software oder all d’Méiglechkeeten, op déi e System fale kéint.

D’Grenze vum Beweis si genee definéiert

Déi iwwerpréifte Garantien betreffen de kryptographesche Kär an eenzel Austausch. De beschriwwene Kader léisst d’Applikatioun als Ganzt, Gruppegespréicher an d’Benotzung op méi Apparater baussen. Et ass och keng Verifikatioun vu WhatsApp oder Google Messages, och wann dës Servicer Elementer vum Signal-Protokoll benotzen. Eng gemeinsam Bibliothéik oder e gemeinsame Protokoll mécht d’Applikatiounen, déi se integréieren, hir Versiounen an hir Konfiguratiounen net identesch.

D’Verifikatioun bedeit och net, datt keng onbekannt Schwachstelle méi besteet. Si reduzéiert d’Onsécherheet bei definéierte Properties a beim Code, deen an d’Analyse abegraff ass. Aner Komponenten, d’Interfaces, d’Betribssystemer, d’Gestioun vun de Schlësselen oder Funktiounen, déi net zum Kader gehéieren, kënnen aner Froen opwerfen.

Fir d’Benotzer läit den direkten Notzen also manner an enger neier Astellung wéi an enger Kontrollmethod, déi et méi schwéier maache kéint, verschidde Garantien a Fro ze stellen oder se ongewollt ze verletzen. Fir d’Teams, déi kritesch Software entwéckelen, geet et ëm d’Fro, ob Agenten d’mënschlech Aarbecht bei Beweiser reduzéiere kënnen, déi bis elo vill spezialiséiert Aarbecht verlaangt hunn. DeepMind ernimmt méiglech Uwendungen op aner Software, mee et muss sech nach weisen, ob sech dës Approche op méi grouss Systemer ausdeene léisst.

D’Spezifikatiounen an d’Beweiser, déi DeepMind verëffentlecht huet, erméiglechen et anere Spezialisten, d’Aarbecht ze iwwerpréiwen an ze reproduzéieren. Dës Méiglechkeet zur Kontroll, zesumme mat engem kloer definéierte Kader, mécht et méiglech, de Bäitrag vun der KI ze bewäerten: net als allgemeng Zertifizéierung vu „Sécherheet“, mee als Hëllef, fir verschidde Properties vum Code ze beweisen – mat Mënschen, déi decidéieren, wat wichteg ass, an engem formelle Verifizéierer, deen de Beweis kontrolléiert.