Ethereum's Vitalik Buterin legt uit hoe AI slimme contracten echt veilig kan maken

Het bericht Ethereum's Vitalik Buterin legt uit hoe AI slimme contracten echt veilig kan maken verscheen eerst op Coinpedia Fintech News

Ethereum-medeoprichter Vitalik Buterin heeft een uitgebreid betoog gepubliceerd waarin hij stelt dat door AI ondersteunde formele verificatie fundamenteel kan veranderen hoe veilige software wordt gebouwd, en daarmee ingaat tegen het groeiende pessimisme in de cybersecuritygemeenschap over de vraag of trustless systemen kunnen overleven onder steeds krachtigere door AI aangedreven aanvallen.

"Veel mensen beweren dat met door AI ondersteund bugs zoeken, veilige code onmogelijk wordt," schreef Buterin. "Ik heb een veel optimistischere kijk, en door AI ondersteunde formele verificatie is een belangrijk deel van de reden daarvoor."

Wat formele verificatie eigenlijk is

Formele verificatie is de praktijk van het schrijven van wiskundige bewijzen over code die automatisch door een computer kunnen worden gecontroleerd. In plaats van software te testen en te hopen dat er geen bugs verschijnen, schrijven ontwikkelaars bewijzen die wiskundig garanderen dat een stuk code zich onder alle omstandigheden precies gedraagt zoals bedoeld.

De technologie bestaat al decennia maar bleef een niche omdat het met de hand schrijven van deze bewijzen buitengewoon moeilijk en tijdrovend is. Buterins argument is dat AI deze vergelijking drastisch verandert. AI kan zowel de code als de bewijzen schrijven, terwijl mensen eenvoudig verifiëren dat de te bewijzen stellingen overeenkomen met wat ze eigenlijk willen dat de software doet.

Hij beschreef deze combinatie als wat onderzoeker Yoichi Hirai "de eindvorm van softwareontwikkeling" noemt.

Waarom het belangrijk is voor Ethereum

Buterin wees op verschillende gebieden waar formele verificatie al wordt toegepast binnen het ontwikkelingsecosysteem van Ethereum. Hieronder vallen kwantumbestendige handtekeningen, STARK-bewijssystemen, consensusalgoritmen en ZK-EVM's — allemaal gebieden waarbij de beveiligingseigenschappen eenvoudig te definiëren zijn, ook al is de onderliggende code buitengewoon complex.

Projecten zoals Arklib werken aan een volledig formeel geverifieerde STARK-implementatie. Het evm-asm-project bouwt een volledige EVM die rechtstreeks in RISC-V assembly is geschreven en wiskundig is geverifieerd aan de hand van een door mensen leesbare referentie-implementatie. Byzantijnse fouttolerante consensusprotocollen worden ook formeel gespecificeerd en geverifieerd in Lean.

Het belangrijkste inzicht is dat voor deze systemen de kloof tussen wat de code doet en wat hij zou moeten doen met wiskundige zekerheid kan worden gedicht in plaats van via probabilistisch testen.

De beperkingen die hij erkent

Buterin was voorzichtig om de zaak niet te overdrijven. Formele verificatie heeft echte faalmodi. Bewijzen kunnen worden geschreven over slechts een deel van een systeem terwijl kritieke bugs verborgen blijven in niet-geverifieerde secties. Ontwikkelaars kunnen vergeten relevante eigenschappen te specificeren. De formele specificatie zelf kan onjuist zijn. Hardwarekwetsbaarheden zoals side-channel-aanvallen kunnen zelfs wiskundig correcte software omzeilen.

"Aantoonbare correctheid bewijst niet dat software correct is op de manier zoals de meeste mensen correctheid begrijpen," schreef hij. Wat formele verificatie feitelijk doet, is ontwikkelaars in staat stellen hun intenties op meerdere verschillende redundante manieren uit te drukken en automatisch te controleren of al die uitdrukkingen met elkaar verenigbaar zijn.

De bredere visie

Buterin beschreef een optimistische toekomst waarbij software zich opsplitst in twee lagen. Een onveilige randlaag verwerkt functies met lagere inzetten, draait in sandboxes en werkt met minimale rechten. Een veilige kern verwerkt alles wat kritiek is, waaronder Ethereum zelf, besturingssysteemkernen en gevoelige IoT-infrastructuur.

De veilige kern wordt bewust klein gehouden en onderworpen aan agressieve formele verificatie. AI brengt de rekenkracht om verificatie op schaal praktisch te maken. Het resultaat is niet software zonder bugs, maar software waarbij de meest kritieke componenten met wiskundige zekerheid kunnen worden vertrouwd in plaats van op hoop.

"Verdedigers hebben eindelijk een kans om te winnen, en dat op beslissende wijze," concludeerde hij, daarbij verwijzend naar Mozilla's eigen ervaring met het verharden van zijn codebase tegen door AI ondersteunde aanvalsmiddelen.