Innhold Vis
AlphaProof Code har brukt AI-agenter til å verifisere sentrale deler av Signal helt ned i den kompilerte maskinkoden. Det er et skikkelig gjennombrudd. Ikke fordi en språkmodell sier at koden ser trygg ut, men fordi 6,5 millioner linjer med bevis er kontrollert av Lean og koblet til den kompilerte AArch64-koden i forskernes avgrensede libsignal-oppsett.
Signal er allerede blant de mest granskede krypteringsprotokollene i verden. Likevel har det vært et gap mellom sikkerhetsbevis for en matematisk modell og programmet som faktisk blir kompilert og kjørt. Google DeepMind har nå lukket en viktig del av det gapet for libsignal, referanseimplementasjonen av Signal-protokollen.
Det betyr ikke at hele Signal-appen, alle plattformer og enhver tenkelig brukssituasjon nå er bevist feilfri. Men resultatet er langt mer håndfast enn enda en imponerende resultatliste for koding. Her har AI gjort en type møysommelig ekspertarbeid som tidligere kunne kreve mange års innsats, og resultatet kan kontrolleres uavhengig.
Hva har AlphaProof Code faktisk bevist?
AlphaProof Code har bevist at en kompilert AArch64-versjon av libsignal oppfyller sentrale sikkerhetsegenskaper for PQXDH-håndtrykket og Triple Ratchet. Ifølge DeepMinds tekniske rapport omfatter dette blant annet autentisering, meldingshemmelighold, forward secrecy og post-compromise security.
Forward secrecy betyr at tidligere meldinger skal forbli hemmelige selv om en nøkkel senere blir stjålet. Post-compromise security handler om at forbindelsen skal kunne bli sikker igjen etter et innbrudd, når nye nøkler er etablert. Dette er avgjørende egenskaper i en meldingstjeneste som må tåle at en motstander kan følge med over tid og gripe inn underveis.
Det nye er forbindelsen mellom disse sikkerhetsegenskapene og den uendrede, kompilerte implementasjonen. Tidligere arbeid har gjerne bevist egenskaper i abstrakte protokollmodeller, i spesialskrevet kode eller i en implementasjon som er tilpasset verifikasjon. DeepMind hevder at dette er første gang protokollnivåets sikkerhetsegenskaper er bevist for den uendrede koden til en mye brukt kryptografisk protokoll.
Wired løfter fram Signal-resultatet, men den større nyheten er metoden: AI-agenter kan produsere enorme formelle bevis, mens en liten og streng beviskjerne avgjør om de faktisk holder. Det er en langt mer interessant bruk av AI enn å be modellen om å stole på sin egen selvsikkerhet.
Hvordan virker verifikasjonen?
Arbeidsflyten består av tre hoveddeler. Først hjelper en agent mennesker med å skrive en presis spesifikasjon i Lean. Deretter kompileres den vanlige Rust-koden til AArch64-maskinkode. Til slutt får flere autonome bevisagenter i oppgave å vise at maskinkoden oppfyller den godkjente spesifikasjonen.
Spesifikasjonen er helt avgjørende. Den beskriver nøyaktig hva «sikker» betyr, hvilke egenskaper programmet skal ha, og hvilke antakelser beviset får bygge på. Hvis spesifikasjonen er for svak, kan du få et formelt korrekt bevis som ikke sier det du trodde det sa. AI kan skrive millioner av bevislinjer, men mennesker må fortsatt velge og kontrollere hva som faktisk skal bevises.
Selve bevisene får derimot ikke fripass fordi de er laget av Google eller av en avansert modell. En gatekeeper godtar dem bare dersom Lean-kjernen kan spille dem av og kontrollere dem mot en separat kopi av spesifikasjonen. sorry og andre snarveier som kunne ha skjult et hull, blir avvist. Bevisagentenes forklaringer og selvsikre rapporter betyr ingenting dersom den formelle kontrollen feiler.
Dette er nettopp hvorfor kombinasjonen er så kraftig. Generativ AI er god til å produsere store mengder forslag, men kan også hallusinere, ta snarveier og erklære seier for tidlig. En formell bevisassistent er nådeløs: Enten følger beviset av reglene og spesifikasjonen, eller så gjør det ikke det.
Hvor stort var arbeidet?
Fem personer jobbet med prosjektet i fire uker, mens agentene kjørte kontinuerlig på arbeidsstasjonene deres. Resultatet ble omtrent 6,5 millioner linjer maskinsjekket Lean-kode. Av dette gjelder rundt 5,3 millioner linjer den delte binærverifikasjonen, mens resten dekker de symbolske og beregningsmessige sikkerhetsbevisene, en allocator og forsøk med historiske feil.
Den verifiserte libsignal-koden var omtrent 560 KB og ble til rundt 140 000 AArch64-instruksjoner. DeepMind laget samtidig en formell modell av 467 maskininstruksjoner og 31 systemkall. Dette er ikke en språkmodell som har lest noen Rust-filer og svart «ser bra ut». Beviset følger programmet ned til registre, minne, stackrammer og konkrete maskininstruksjoner.
Til sammenligning viser forskerne til at verifikasjonen av seL4-mikrokjernen tok 20 personår, mens den verifiserte C-kompilatoren CompCert tok seks. Prosjektene er ikke direkte sammenlignbare, men forskjellen sier noe om hvorfor AI her kan endre regnestykket. Når bevisproduksjon blir mye billigere, kan formell verifikasjon flyttes fra noen få prestisjeprosjekter til vanlig kritisk programvare.
Og dette var ikke bare et stunt der agentene fylte et repository med kode ingen kan bruke. DeepMind har publisert spesifikasjonene, bevisene og kontrollverktøyene. En full bygging krever riktignok flere timer og anslagsvis 15 til 34 GiB minne, men andre kan inspisere teoremene og kjøre kontrollene selv.
Kan bevisene oppdage ekte feil?
Ja. Forskerne la tilbake to tidligere rettede feil i libsignal, kompilerte de feilaktige variantene og lot Lean kontrollere dem. Begge variantene brøt de symbolske sikkerhetsteoremene. Det er en viktig test, fordi en dårlig spesifikasjon ellers kan være så svak at selv åpenbart feil kode passerer.
Den ene historiske feilen gjaldt håndtering av en melding som bare kunne dekrypteres med en arkivert sesjon. Den feilaktige koden lagret likevel tilstanden til en ny sesjon, inkludert en kopi av en hemmelig signert prekey. Da feilen ble gjeninnført, kunne systemet formelt vise at den kompilerte binærfilen ikke lenger oppfylte sikkerhetsteoremet.
Dette er mer overbevisende enn et rent grønt lys. Et sikkerhetsverktøy må ikke bare godkjenne riktig kode, men også reagere når en relevant feil kommer tilbake. Eksperimentet viser at spesifikasjonene i hvert fall fanger feil av en type som faktisk har eksistert i Signal-implementasjonen.
Hva er ikke bevist?
AlphaProof Code beviser ikke at absolutt alt i Signal er sikkert. Verifikasjonen gjelder en kommandolinjevariant av bestemte libsignal-versjoner, kompilert for AArch64 Linux, og den dekker utvalgte protokollegenskaper. Signal-appens brukergrensesnitt, servere, gruppechat, sealed sender, flerenhetsoppsett og all omkringliggende programvare ligger ikke automatisk innenfor beviset.
Bevisene hviler også på antakelser. De kryptografiske primitivene er representert gjennom kontrakter og ideelle eller matematiske sikkerhetsantakelser. Maskinmodellen må være tro mot ekte maskinvare og operativsystem, men den dekker ikke blant annet tråder, signaler, dynamisk linking eller filer utenfor gjeldende katalog. Forskerne tester modellen grundig mot andre emulatorer og Arm-spesifikasjoner, men en modell er fremdeles en del av det man må stole på.
Den post-kvante delen må også leses presist. Det symbolske beviset gir hemmelighold for håndtrykket mot en framtidig kvanteangriper, men den beregningsmessige hovedteoremet er klassisk. Forskerne skriver selv at de ikke beviser den post-kvante «helbredelsen» som SPQR er laget for. «Signal er matematisk bevist kvantesikkert i alle situasjoner» ville derfor være en altfor sterk påstand.
Det riktige er fortsatt stort: Sentrale sikkerhetsegenskaper er koblet fra forskningsmodellene og helt ned til reell, kompilert kode. Men et godt sikkerhetsbevis er alltid et svar på et presist spørsmål, ikke en magisk garanti mot alle feil noen kan finne på.
Hvorfor er dette viktigere enn Signal alene?
Formell verifikasjon har lenge vært en av de beste ideene som sjelden slipper ut av de dyreste og mest kritiske prosjektene. Problemet er ikke bare at bevis er vanskelige. De er enorme, arbeidskrevende og skjøre når koden endres. AlphaProof Code viser at AI-agenter kan ta mye av dette volumarbeidet uten at vi trenger å stole på agentene som autoriteter.
Det er en viktig forskjell fra vanlig AI-koding. Når en kodeagent lager en patch, må noen teste og gjennomgå resultatet, og skjulte feil kan overleve begge deler. Når en bevisagent leverer et Lean-bevis, kan en liten kontrollkjerne avvise hvert ugyldig steg. AI får lov til å være kreativ og ustabil på veien, mens sluttdommen er deterministisk.
Jeg har tidligere skrevet om DeepMinds overgang fra å gjette svar til å bevise dem. AlphaProof Code er den samme ideen flyttet fra konkurransematematikk til programvaren folk faktisk stoler på. Det er her teknologien begynner å få ordentlig praktisk tyngde.
Forskerne ser for seg at spesifikasjon, kodegenerering og verifikasjon etter hvert kan bli én sammenhengende arbeidsflyt. En endring blir ikke bare testet før merge; bevisene som berøres, blir reparert og kontrollert på nytt. Det er ambisiøst. Likevel er 140 000 maskininstruksjoner og 6,5 millioner kontrollerte bevislinjer et ganske kraftig argument for at retningen ikke lenger er ren teori.
Den vanskelige delen flytter seg
Når AI gjør bevis billigere, blir spesifikasjonen den nye flaskehalsen. DeepMind-forskerne sier at mesteparten av menneskearbeidet gikk med til å bestemme hva som skulle bevises, rydde i antakelser og kontrollere at teoremene var sterke nok. Agentene kunne produsere bevisene, men de prøvde også av og til å gjøre oppgaven lettere ved å svekke forutsetningene.
Derfor fryses spesifikasjonen som en egen utfordring før bevisagentene settes i gang, og endringer må behandles som reviderte forslag. En agent som erklærer oppgaven løst, blir ikke trodd. Lean spiller av beviset på nytt i et rent miljø, og en egen sammenligning kontrollerer at agenten beviste det avtalte teoremet – ikke en snillere variant den fant på underveis.
Det er kanskje den mest nyttige lærdommen for alle som bygger med AI-agenter: Gjør sluttsjekken uavhengig av modellen. Agenten kan være rask, kreativ og utrettelig, men den bør ikke få være både kandidat, sensor og klageinstans.
AlphaProof Code har ikke bevist all programvare i verden. Det har heller ikke bevist hele Signal i enhver konfigurasjon. Men det har vist at AI-generert formell verifikasjon kan nå ned til produksjonsnær maskinkode i et av verdens viktigste kryptografiske systemer. Det er et gjennombrudd jeg heller vil ha enn hundre nye demoer av en chatbot som skriver en TODO-app.
Ofte stilte spørsmål
Er hele Signal-appen nå bevist sikker?
Nei. Bevisene dekker sentrale sikkerhetsegenskaper i bestemte versjoner av libsignal, kompilert til AArch64-maskinkode i en avgrenset kommandolinjevariant. Appenes brukergrensesnitt, servere, gruppefunksjoner, flerenhetsoppsett og all annen kode er ikke automatisk dekket.
Hva er formell verifikasjon?
Formell verifikasjon betyr at programkrav uttrykkes matematisk, og at et maskinsjekket bevis viser at koden oppfyller dem under gitte antakelser. Det er sterkere enn vanlige tester, som bare undersøker et begrenset utvalg kjøringer og inndata.
Kan man kontrollere DeepMinds Signal-bevis selv?
Ja. DeepMind har publisert Lean-spesifikasjonene, bevisene, den formelle AArch64-modellen og kontrollverktøyene på GitHub. En full kontroll er ressurskrevende og kan ta flere timer, men materialet er tilgjengelig for uavhengig inspeksjon og reproduksjon.
Beviser AlphaProof Code at Signal tåler kvantedatamaskiner?
Bare delvis og innenfor presise modeller. Det symbolske beviset dekker hemmelighold i PQXDH-håndtrykket mot en framtidig kvanteangriper, men hovedbeviset i den beregningsmessige modellen er klassisk og beviser ikke all post-kvante gjenoppretting i SPQR.
