Onderzoekers van Google DeepMind hebben laten zien dat een AI-systeem belangrijke beveiligingseigenschappen van het Signal-berichtenprotocol wiskundig kan bewijzen. Het team gebruikte een nieuw raamwerk, AlphaProof Code, om verschillende cryptografische garanties formeel te verifiëren. Het onderzoek duurde ongeveer vier weken en was een onderzoeksproject, geen commercieel product. In de onderzochte onderdelen werden geen nieuwe bugs gevonden. Toen de AI op eerdere versies van het protocol werd losgelaten, herkende die wel oudere, al verholpen kwetsbaarheden.
Formele verificatie houdt in dat je met wiskunde controleert of software precies doet wat de bedoeling is, zonder ruimte voor verborgen kwetsbaarheden. Tot nu toe moesten experts daarvoor gedetailleerde specificaties schrijven, die omzetten in formules en vervolgens het bewijs opstellen — een arbeidsintensieve klus die maanden kon duren. Door een agentische AI — een AI die zelf subdoelen kan bepalen en nastreven — een groot deel van het werk te laten doen, bracht DeepMind de doorlooptijd terug tot weken. Volgens de onderzoekers was op belangrijke momenten nog altijd menselijk toezicht nodig, maar kon de AI zelf bewijzen voorstellen en corrigeren.
Ehren Kret, technisch directeur van Signal, merkte op dat eerder verificatiewerk alleen kleine stukjes code omvatte. De aanpak van DeepMind maakt volgens hem een „aanzienlijke uitbreiding” mogelijk van wat gecontroleerd kan worden. Het team stelt de specificatie en het bewijs die het heeft opgesteld beschikbaar, zodat andere groepen daarop kunnen voortbouwen. Hoewel het resultaat veelbelovend is, waarschuwt DeepMind dat toepassing op volledige apps of complete softwareketens nog een uitdaging vormt. Ook zijn de kosten van deze AI-gestuurde verificatie niet bekendgemaakt.
Waarom dit belangrijk is
Als AI de beveiliging van cryptografische protocollen betrouwbaar kan bewijzen, kunnen gebruikers van Signal, Google Messages, WhatsApp en vergelijkbare apps er meer vertrouwen in krijgen dat hun berichten privé blijven. Voor bedrijven die afhankelijk zijn van versleutelde communicatie — zoals banken, zorgverleners en journalisten — kan de technologie op termijn juridisch verifieerbare garanties bieden dat hun software geen kritieke fouten bevat.
Waarom het ertoe doet
Voor gewone gebruikers betekent dit dat de versleuteling van hun chats nu ook met een aanvullende wiskundige controle is getoetst, waardoor de kans op verborgen bugs kleiner wordt. Voor bedrijven die moeten aantonen dat ze aan privacyregels voldoen, kan verificatie met behulp van AI een nieuwe manier bieden om de beveiliging te onderbouwen, zonder langdurige handmatige audits.
