💻 computer science

Smart Contract Invariants Protect Against Cybercriminals

Dit artikel toont aan dat smart contract-invarianten, gevalideerd via de INVARIANTEVAL-benchmark en het PONDEREPLAY-framework, effectief bescherming bieden tegen alle 28 real-world Ethereum-exploits door cybercriminele aanvallen te blokkeren over 108.637 historische transacties.

Oorspronkelijke auteurs: Sofia Bobadilla, Humaira Afrin, Angela Novelli, Martin Monperrus

Gepubliceerd 2026-08-14

📖 4 min leestijd☕ Koffiepauze-leesvoer

CC BY 4.0

Oorspronkelijke auteurs: Sofia Bobadilla, Humaira Afrin, Angela Novelli, Martin Monperrus

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je het internet voor als een enorme, bruisende digitale stad waar geld niet in banken wordt bewaard, maar in gigantische, transparante glazen kluizen die "blockchains" worden genoemd. Binnen deze kluizen leven "smart contracts", die in essentie zelfuitvoerende verkoopautomaten zijn. Je stopt de juiste code erin (zoals een muntje) en de machine geeft je het juiste product (zoals een token), allemaal zonder een menselijke kassier. Maar hier zit de adder onder het gras: deze verkoopautomaten zijn gebouwd door mensen, en mensen maken fouten. Als een programmeur vergeet een deur op slot te doen of het wisselgeld verkeerd berekent, kan een slimme dief naar binnen glippen, de hele kluis grijpen en met miljarden dollars verdwijnen. Dit is het wilde westen van de digitale economie, waar cybercriminelen constant op zoek zijn naar een los schroefje om het glas open te breken.

Om deze dieven te stoppen, proberen computerwetenschappers betere sloten te bouwen. Eén veelbelovend idee is de "invariant". Denk aan een invariant als een magische regel die de verkoopautomaat controleert voordat hij iets doet. Het is als een uitsmijter bij een club die een lijst controleert: "Is de persoon ouder dan 21? Is de deur op slot? Komt de prijs overeen?" Als het antwoord op een van deze vragen "nee" is, slaat de machine de deur dicht en weigert hij te bewegen, zelfs als de dief een meestersleutel vasthoudt. De grote vraag die onderzoekers hebben gesteld is: Als we deze magische uitsmijters in plaats hadden gehad tijdens eerdere overvallen, zouden ze de dieven dan daadwerkelijk hebben tegengehouden? En nog belangrijker: kunnen we computers leren om deze uitsmijters zelf uit te vinden, of hebben we nog steeds menselijke experts nodig om de regels te schrijven?

Dit artikel duikt diep in dat vraagstuk door een enorme, real-world experiment op te zetten. De onderzoekers, een team van de KTH Koninklijke Instituut van Technologie, besloten niet langer te gissen maar te testen. Ze verzamelden een collectie van 28 echte, miljarden dollars kostende overvallen die al hadden plaatsgevonden op de Ethereum-blockchain. Voor elk van deze rampen traden ze op als digitale rechercheurs van een plaats delict. Ze keken precies naar hoe de dieven waren ingebroken en schreven vervolgens handmatig een specifieke "invariant" (een beveiligingsregel) die die specifie specifieke aanval zou hebben geblokkeerd. Ze noemden deze collectie INVARIANTEVAL.

Maar ze schreven niet alleen de regels; ze bouwden een tijdmachine om ze te testen. Met behulp van een geavanceerde tool die ze zelf hebben ontwikkeld, genaamd PONDEREPLAY, lieten ze de geschiedenis van de blockchain opnieuw afspelen. Ze namen de oorspronkelijke, kwetsbare code, voegden hun nieuwe beveiligingsregels toe en speelden vervolgens 108.637 historische transacties opnieuw af. Het is alsof je de film van een bankoverval opnieuw bekijkt, maar dit keer heeft de bank een nieuw, supersterk alarmsysteem.

De resultaten waren bijzonder duidelijk. Toen ze de replay draalden, werkten al die 28 door mensen geschreven beveiligingsregels perfect. In elk geval raakte de aanvallende transactie de nieuwe regel, zei de machine "Niet mogelijk" en werd de diefstal geblokkeerd. De onderzoekers ontdekten dat deze regels niet alleen de slechteriken tegenhielden; ze lieten de goeden (legitieme gebruikers) ook 98,3% van de tijd normaal gebruikmaken van het systeem. De weinige keren dat het systeem iets te streng was en een normale gebruiker blokkeerde, konden de onderzoekers precies herleiden waarom, wat bewees dat de regels naar behoren werkten en niet zoma aantastten.

Echter, het verhaal neemt een scherpe wending wanneer de onderzoekers de tweede vraag stellen: Kunnen computers dit doen? Ze namen de beste, meest geavanceerde geautomatiseerde tools die momenteel beschikbaar zijn in het vakgebied — tools die ontworpen zijn om deze beveiligingsregels automatisch voor ons te schrijven — en testten deze tegen hun 28 echte overvallen. Het resultaat was een nederige mislukking. Van de 28 aanvallen die gestopt moesten worden, slaagden deze chique geautomatiseerde tools er slechts in om de juiste beveiligingsregel te achterhalen voor slechts 2 van hen. De andere 26? De tools zagen het gevaar ofwel helemaal niet, of schreven regels die te zwak waren om de dieven te stoppen.

Dus, wat is de kern van het verhaal? Het artikel bewijst dat het concept van "invariants" een krachtig schild is; als we de juiste regels op de plek hadden gehad, hadden we meer dan een miljard dollar aan diefstallen kunnen voorkomen. Maar het slechte nieuws is dat we nog geen robot hebben die die regels betrouwbaar voor ons kan schrijven. We hebben nog steeds menselijke experts nodig om de specifieke trucs van de dieven te begrijpen en de bewakers te schrijven. De technologie om deze verdedigingen automatisch te genereren staat nog in de kinderschoenen, waardoor er een enorme kloof gaapt tussen wat we weten werkt en wat onze computers momenteel zelfstandig kunnen doen.

Technische Samenvatting: Smart Contract Invarianten Beschermen Tegen Cybercriminelen

Probleemstelling

Smart contracts opereren in hoogst vijandige omgevingen waarin kwetsbaarheden leiden tot onomkeerbare financiële verliezen, die de miljard dollar aan gestolen on-chain activa overschrijden. Hoewel security audits en geautomatiseerde tools bestaan, hebben deze er niet in geslaagd om real-world exploits effectief te voorkomen. Er bestaat een kritieke kloof in het begrip of het klassieke software engineering-concept van programma-invarianten (logische condities die op specifieke programmapunten moeten standhouden) effectief deze aanvallen kan stoppen. Bovereen is het een open vraag of state-of-the-art geautomatiseerde tools voor invariantgeneratie in staat zijn om de specifieke invarianten te ontdekken die nodig zijn om real-world, miljoenen dollars kostende diefstallen te blokkeren. Voorgaand onderzoek heeft tools grotendeels geëvalueerd tegen synthetische eigenschappen of gemined patronen, in plaats van hen te confronteren met gedocumenteerde, hoogwaardige incidenten.

Methodologie

De auteurs stellen een nieuw experimenteel protocol voor dat volledig gebaseerd is op on-chain data om twee primaire vragen te beantwoorden: (1) Kan een enkele programma-invariant een real-world exploit stoppen? en (2) Kunnen geautomatiseerde tools dergelijke invarianten ontdekken?

1. INVARIANTEVAL Benchmark

De studie construeert INVARIANTEVAL, een benchmark bestaande uit 28 real-world Ethereum exploits afkomstig uit de DeFiHackLabs corpus. Voor elke exploit schrijven twee auteurs onafhankelijk van elkaar een door mensen geschreven programma-invariant die ontworpen is om de specifieke aanval te blokkeren terwijl de legitieme functionaliteit behouden blijft. Deze invarianten worden in de kwetsbare functies van de originele contracten geplaatst om "verharde" versies te creëren. De dataset beslaat incidenten variërend van 2018 tot 2026, met totale verliezen die de $1,07 miljard overschrijden.

2. PONDEREPLAY Verificatie Framework

Om de effectiviteit en veiligheid van deze invarianten te valideren, hebben de auteurs PONDEREPLAY ontwikkeld, een geavanceerd framework voor historische replay. In tegenstelling tot bestaande tools die een gebrek hebben aan granulariteit op sub-block niveau of handmatige scenario-reconstructie vereisen, voert PONDEREPLAY het volgende uit:

Forkt de Ethereum mainnet op het blok voorafgaand aan de aanval.
Injecteert de verharde bytecode (originele code + invariant) op het doelcontractadres.
Speelt transacties af in drie verschillende modi:
- Reproductie Check: Voert de originele, ongewijzigde contract opnieuw uit om te garanderen dat de replay-infrastructuur de on-chain staat getrouw reproduceert (Originele trace $O$ vs. Recompiled trace $R$ ).
- Security Check: Voert de specifieke aanvalstransactie opnieuw uit (zowel de Proof-of-Concept als de werkelijke kwaadaardige on-chain transactie) tegen het verharde contract om te verifiëren dat de aanval wordt afgewezen (reverted).
- Preservation Check: Voert de volledige historische transactiegeschiedenis van het contract vóór de aanval opnieuw uit (108.637 transacties) tegen het verharde contract om te waarborgen dat legitiem gedrag behouden blijft (Hardened trace $H$ vs. Recompiled trace $R$ ).

Het framework vergelijkt traces op basis van transactiestatus, subcall-uitkomsten en opslagverschillen (met behulp van een numerieke drempelwaarde $\epsilon$ ) om causale attributie te bieden voor eventuele gedragsveranderingen.

3. Onderzoeksvragen

De studie evalueert vier specifieke onderzoeksvragen (RQs):

RQ1: In welke mate stoppen programma-invarianten real-world aanvallen?
RQ2: In welke mate breken aanval-stoppende invarianten bestaand legitiem gedrag?
RQ3: Wat zijn de beperkingen van historische replay-verificatie?
RQ4: In welke mate kunnen state-of-the-art invariantgeneratie-tools deze aanval-stoppende invarianten ontdekken?

Belangrijkste Resultaten

RQ1: Effectiviteit van Invarianten

De door mensen geschreven invarianten waren 100% effectief. Alle 28 verharde contracten blokkeerden succesvol zowel de Proof-of-Concept exploits als de werkelijke kwaadaardige on-chain transacties. In elk geval werd de transactie afgebroken bij de kwetsbare stap met de specifieke foutmelding die in de invariant is gedefinieerd. De studie identificeerde acht terugkerende families van invarianten, waarbij Price/Oracle checks (8 gevallen), Ledger/Supply conservation (6 gevallen) en Access Control/Interaction Safety (elk 4 gevallen) de meest prominente waren.

RQ2: Behoud van Gedrag

De invarianten behielden het legitieme gedrag in 98,3% van de gereplayde historische transacties (106.815 van de 108.637).

Divergenties: 1.526 transacties week af (divergeren). Deze werden causaal toegeschreven aan de invariant, en niet aan replay-ruis.
Aard van de Divergenties:
- Eerdere Exploits/Whitehats: Veel divergenties wezen terecht eerdere kwaadaardige pogingen of whitehat reddingsoperaties af die hetzelfde kwetsbaarheidspad gebruikten.
- Misbruik: Sommige transacties werden afgewezen omdat ze de protocolregels overtraden (bijv. slippage-limieten) die de kwetsbare code eerder wel toeliet.
- Overdreven restrictieve Invarianten: In sommige gevallen (bijv. Yearn yDAI) was de invariant te strikt voor legitieme gebruikers (bijv. keeper bots), waardoor geldige calls werden afgewezen die geen exploit gebruikten.
- Strakke Numerieke Enveloppen: Sommige invarianten wezen legitieme transacties af vanwege nauwe numerieke grenzen (bijv. prijsafwijking-drempels) die te strikt waren voor normale marktvolatiliteit.

RQ3: Beperkingen van Replay-verificatie

Van de 108.637 transacties waren er 296 onconcluderend (het opnieuw gecompileerde ongewijzigde contract kwam niet overeen met de originele on-chain trace).

Oorzaken: De primaire oorzaak was Out-of-Gas (OOG) mismatches (173 gevallen), waarbij de replay meer gas toewezag dan de originele transactie, waardoor deze slaagde waar de originele faalde. Andere oorzaken waren subcall OOGs (12 gevallen) en geaccumuleerde state drift door co-gelokaliseerde transacties in dezelfde block (111 gevallen).
Validatie: Voor 291 van deze 296 inconcludente gevallen kwam de verharde trace nog steeds overeen met de recompiled trace, wat bevestigde dat de inconclusiviteit voortkwam uit de gas-handling van de replay-infrastructuur, en niet uit de invariant zelf.

RQ4: Prestaties van Geautomatiseerde Tools

De auteurs evalueerden drie state-of-the-art tools: FLAMES, InvCon en InvCon+.

Resultaten: De tools herstelden gezamenlijk slechts 2 van de 28 ground-truth invarianten (beide door FLAMES).
Analyse: Hoewel de tools kandidaat-invarianten genereerden voor veel contracten, slaagden ze er niet in om de specifieke beveiligingskritische eigenschappen te synthetiseren die nodig zijn om de real-world aanvallen te blokkeren. Dit onderstreept een fundamentele kloof tussen de huidige automatische synthese-capaciteiten en de eisen van real-world beveiliging.

Betekenis en Claims

Het artikel claimt dat smart contract invarianten een krachtig en effectief defensiemechanisme zijn tegen cybercriminelen. De studie demonstreert dat:

Haalbaarheid: Een enkele, correct gespecificeerde invariant voldoende is om een real-world exploit te stoppen, ongeacht de aanvalsvector (overflow, reentrancy, oracle manipulatie, etc.).
Veiligheid: Wanneer zorgvuldig vervaardigd, behouden deze invarianten het overgrote deel (98,3%) van het legitieme gebruik van het contract.
Tooling Gap: Ondanks de bewezen effectiviteit van handmatige invarianten, zijn huidige geautomatiseerde invariantgeneratie-tools nog niet in staat om te beschermen tegen real-world aanvallen, aangezien zij minder dan 10% van de noodzakelijke guards herstellen.

De auteurs concluderen dat hoewel het concept van invarianten een robuuste oplossing biedt voor het probleem van smart contract security, de automatisering van hun ontdekking een open onderzoeksuitdaging blijft. Het werk vestigt een nieuwe benchmark (INVARIANTEVAL) en verificatie-infrastructuur (PONDEREPLAY) om toekomstig onderzoek in invariant-synthese en contract-hardening te begeleiden.