Google DeepMind zegt dat het AlphaProof Code heeft ingezet om belangrijke beveiligingseigenschappen van libsignal wiskundig te controleren. Libsignal is de referentie-implementatie van het Signal-berichtenprotocol. Het werk duurde vier weken. Volgens DeepMind kostte vergelijkbare verificatie expertteams voorheen jaren.
Het systeem combineerde menselijke onderzoekers met AI-agenten. Onderzoekers en AI hielpen de beveiligingsdoelen van Signal om te zetten in wiskundige specificaties, die vervolgens door mensen werden beoordeeld. Daarna genereerden agenten op basis van Gemini Carbon ongeveer 6,5 miljoen regels Lean-bewijscode. Lean is een programmeertaal waarvan de controlemechanismen kunnen nagaan of een wiskundig bewijs aan de regels voldoet. De agenten markeerden ongeveer één procent van de codebase voor menselijke beoordeling.
Wat bewijst het onderzoek?
De onderzoekers controleerden de gecompileerde machinecode van libsignals postkwantumhandshake PQXDH en Triple Ratchet. Ze bewezen specifieke eigenschappen, waaronder voorwaartse geheimhouding, authenticatie en bescherming nadat een apparaat is gecompromitteerd. In het onderzoeksartikel staat dat de code met een standaardcompiler is gecompileerd vanuit ongewijzigde Rust-code en vervolgens als AArch64-machinecode is gecontroleerd.
Dit gaat verder dan bewijzen dat een abstract ontwerp veilig is: het koppelt gespecificeerde beveiligingsgaranties aan gecompileerde code. DeepMind noemt dit de eerste formele verificatie op dit niveau van de implementatie van een breed gebruikt cryptografisch protocol. Het team zette ook twee eerder verholpen bugs terug in een geïsoleerde versie van de code. Het systeem leverde bewijzen dat de versies met die bugs niet voldeden aan de opgegeven beveiligingseigenschappen.
Het bewijs kent beperkingen
Dit is geen wiskundige garantie dat elk onderdeel van Signal, of elke app die het protocol gebruikt, vrij is van beveiligingsproblemen. Het bewijs geldt voor geselecteerde eigenschappen van libsignal, niet voor de hele app. Ook steunt het op goedgekeurde specificaties, de controlemechanismen van Lean en contracten voor cryptografische routines op laag niveau. The Register merkt op dat het resultaat niet bewijst dat de daadwerkelijke berichtinhoud computationeel geheim blijft. Het artikel van DeepMind beschrijft bewijzen in zowel symbolische als computationele modellen; die steunen op aannames over de onderliggende cryptografische primitieve bouwstenen.
DeepMind zegt de verificatiematerialen beschikbaar te stellen voor anderen. Het hoopt de aanpak toe te passen op onder meer firmware voor medische apparatuur en software voor elektriciteitsnetten, maar zegt dat meer onderzoek nodig is om de methode op grotere schaal toe te passen. Het werk is een stap richting het controleren van meer code uit de praktijk, geen bewijs dat die andere systemen zijn geverifieerd.
Waarom het ertoe doet
Voor Signal-gebruikers levert dit werk een door een machine gecontroleerd bewijs op voor specifieke beveiligingseigenschappen van de kernimplementatie van het protocol. Het toont niet aan dat de hele app bugvrij is, en het bewijs steunt op aannames over cryptografische componenten.
