Ethereum-medeoprichter Vitalik Buterin zegt dat de opkomst van AI-gedreven hacking cybersecurity niet tot een onwinbare wedstrijd maakt, en wijst in plaats daarvan op formele verificatie als een manier om te bewijzen dat software veilig is. In plaats van afhankelijk te zijn van het ontdekken van kwetsbaarheden, kunnen ontwikkelaars volgens hem wiskundig aantonen dat programma's aan gedefinieerde beveiligingseisen voldoen.

In een blogpost van 18 mei, die hij deelde op X, stelde Buterin dat AI dergelijke verificatie op schaal praktisch haalbaar kan maken — een aanpak die volgens hem het meest relevant is voor kritieke systemen, waaronder cryptografie, berichtenprotocollen en blockchainsoftware.

Beveiliging moet gedefinieerd worden voordat deze bewezen kan worden

Buterin zei dat het bewijzen dat een programma veilig is, eerst vereist dat wordt gedefinieerd wat beveiliging werkelijk betekent. Hij noemde de versleutelde berichtenapp Signal als voorbeeld, met de kanttekening dat versleuteling alleen niet elke beveiligingskwestie afdekt. Een volledige definitie moet mogelijk rekening houden met vervalste berichten, mislukte bezorging, opnieuw afgespeelde berichten, gehackte apparaten en gelekte sleutels.

Hardware voegt verdere complicaties toe. Fysieke signalen kunnen informatie lekken, terwijl details zoals berichtgrootte, identiteit van de afzender en timing op zichzelf al onthullend kunnen zijn. Samen kunnen deze overwegingen beveiligingsdefinities tot meer dan 1.000 regels code doen uitgroeien. Desondanks stelde Buterin dat definities een kleiner verificatiedoel blijven dan de onderliggende implementatie.

Formele verificatie richt zich op het hele programma

Formele verificatie is geen nieuw idee: het wordt al lang toegepast in veiligheidskritieke gebieden zoals luchtvaart- en medische software, waar kosten van falen hoog zijn, maar de benodigde inspanning heeft het zeldzaam gemaakt in reguliere softwareontwikkeling. Historisch gezien hebben ontwikkelaars alleen secties geverifieerd die zij zelf als beveiligingskritiek aanmerkten, vooral omdat verificatie aanzienlijke inspanning vergde. Buterin betoogde dat AI die vergelijking kan veranderen, waardoor verificatie van het volledige programma praktischer wordt en de dekking kan worden uitgebreid tot databases, netwerken, caching-lagen en andere componenten.

Hij schetste het doel als onderscheidend van het traditionele model waarbij verdedigers racen om kwetsbaarheden te ontdekken vóór aanvallers. Onder zijn aanpak wordt software veerkrachtiger doordat wordt bewezen dat deze aan de beveiligingseisen voldoet. Definities kunnen ook worden gecombineerd wanneer verschillende groepen aparte eisen vaststellen, zei hij, en waar twee definities niet naast elkaar kunnen bestaan, kunnen ontwikkelaars het onderliggende ontwerpconflict isoleren. Hij erkende echter dat sommige gebruikersinterfaces moeilijker te behandelen blijven.

Complexe verificatiebehoeften voor Ethereum-software

Buterin wees berichtenprotocollen, sandboxes, SNARKs — compacte cryptografische bewijzen dat een berekening correct is uitgevoerd — en volledig homomorfe versleuteling, die berekeningen direct op versleutelde data mogelijk maakt, aan als gebieden waar het onderscheid tussen definities en implementaties ertoe kan doen. Hij koppelde de aanpak direct aan de ontwikkelrichting van Ethereum en zei dat blockchains sterkere softwarebeveiliging nodig hebben, vooral in systemen die gericht zijn op schaalbaarheid en privacy.

De context onderstreept wat er op het spel staat: blockchainsoftware is open-source en de netwerken die het ondersteunt beheren direct activa, waardoor dezelfde code openlijk zichtbaar is voor aanvallers en verdedigers — omstandigheden waaronder garanties die niet afhankelijk zijn van wie een fout het eerst vindt, bijzonder zwaar wegen.

Zijn betoog draait om wiskundige verificatie in plaats van alleen het ontdekken van kwetsbaarheden. Verificatie moet zich volgens hem uitstrekken tot meer dan geselecteerde codesecties: de definitie vraagt om zorgvuldig werk, terwijl de implementatie aan formele controle blijft onderworpen. AI zou in zijn visie de omvang van dat proces kunnen dragen, met dekking van databases, netwerken, caching en andere componenten. De vraag om in de gaten te houden is of AI-ondersteunde tooling verificatie van volledige programma's tot routinepraktijk op productschaal kan brengen, inclusief de gebruikersinterfaces die hij als de moeilijkste gevallen aanmerkte.