Certora Chief Scientist Mooly Sagiv: Blockchainbeveiliging is meer dan alleen code

Als 2025 ons iets heeft geleerd, dan is het wel dat Solana een hoge vlucht heeft genomen en zich heeft gevestigd als “de retailketen. Elke dag verplaatsen duizenden gebruikers geld en ondertekenen ze transacties, waarbij ze zich bezighouden met ondoorgrondelijk complexe slimme contracten zonder zich te bekommeren om de potentiële risico's.

Natuurlijk zitten de risico's nog steeds onder de service. Maar terwijl crypto hacks en exploits nog steeds veel vaker voorkomen dan we zouden willen, gaan mensen er vaak vanuit dat de grootste risico's diep begraven liggen in obscure logica en technische codebases.

Mooly Sagiv is daar niet zo zeker van.

Volgens de Chief Scientist van Certora, een blockchain beveiligingsbedrijf dat meer dan $190B in DeFi TVL beveiligt, worden de meeste verliezen niet veroorzaakt door fouten in de code logica of programmeerfouten, maar door veel eenvoudigere boosdoeners:  Sleutels, bewaring, en menselijke fouten. 

“Houd je sleutel in de gaten… en houd je telefoon in de gaten.”

Het is een eenvoudige waarschuwing, maar het geeft een belangrijke en vaak over het hoofd geziene benadering van cryptobeveiliging weer. Beveiligingsfouten zijn zelden “just a bug”, en de proliferatie van mobiele crypto apps voegt alleen maar meer variabelen en potentiële kwetsbaarheden toe. 

Sagiv bevindt zich in een unieke positie om die zaak te bepleiten. Bekend onder zijn academische collega's als Shmuel (Mooly) Sagiv, heeft de Certora Chief Scientist ook gediend als Tel Aviv University’s Chair of Software Systems voor bijna 28 jaar. Met tientallen jaren onderzoek in programma-analyse en -verificatie speelt Sagiv een leidende rol in Certora’s streven om formele verificatie uit te breiden van een niche-discipline tot iets dat ontwikkelaars continu kunnen uitvoeren.

Tijdens een gesprek met SolanaFloor op Breakpoint 2025 wierp Mooly Sagiv een verhelderend licht op het donkere bos van blockchainbeveiliging. Verantwoordelijk voor het auditen van enkele van de grootste namen in DeFi, Certora’s Chief Scientist besprak enkele van de grootste misvattingen die crypto-gebruikers hebben over beveiliging, het belang van formele verificatie, en of AI en quantum computing risico's worden overschat.

Cryptobeveiliging’s grootste misvatting: “Alle bugs zitten in de code”

Wanneer het aankomt op misvattingen over blockchainbeveiliging, stelt Sagiv dat de cryptocultuur veel te laks is. Het gevaarlijkste misverstand is het geloof dat kwetsbaarheden uitsluitend in code leven en dat als de code wordt gecontroleerd, gebruikers hun gezond verstand kunnen afschaffen.

“Iedereen denkt dat alle bug[s] in de code zitten. En dat hoeft niet altijd zo te zijn… misschien is je code helemaal in orde, maar is er iets buiten… de manier waarop het wordt ingezet…”

Cryptofielen houden vast aan filosofische grondbeginselen zoals ‘code is wet’. Maar hoewel dat waar is, zijn er nog steeds tientallen variabelen waarmee rekening moet worden gehouden. Een protocol kan “correct” zijn en toch onveilig omdat de sleutels slecht worden gecontroleerd, de integraties poreus zijn of de operationele omgeving gecompromitteerd is. Een app is slechts zo veilig als de systemen en het gedrag van de mensen die hem beheren.

Sagiv’s tweede misvatting is de misvatting die de meeste gebruikers willen geloven: dat “audited” veiligheid impliceert.

“Het’is nooit helemaal veilig. We kunnen het veiliger maken… maar het’is nooit volledig veilig.”

Audits zijn ongetwijfeld een integraal onderdeel van cryptobeveiliging, maar ze bieden geen enkele garantie. Mensen ontwikkelen een vals gevoel van veiligheid zodra ze zien dat een app is gecontroleerd, maar DeFi-gebruikers moeten zeker de basisbeveiligingspraktijken niet vergeten.

Certora’s hybride benadering van beveiliging

Sagiv verwerpt audits niet. In feite pleit hij expliciet tegen het idee dat formele verificatie menselijke beoordeling vervangt. In plaats daarvan zouden formele verificatie en menselijke audits idealiter samen moeten worden gebruikt om zoveel mogelijk dekking te bieden.

Tijdens een gesprek met SolanaFloor schetste Sagiv hoe audits typisch bescherming bieden tegen bekende aanvalspatronen, terwijl formele verificatie de blootstelling aan “unknown unknowns.”

“Wanneer je een audit uitvoert, ben je je code aan het beoordelen [met] je beste persoon tegen de bekende aanval. Wanneer je in staat bent om formele verificatie uit te voeren, heb je een soort van preventie van onbekende aanvallen.”

Dat verschil is belangrijk omdat crypto een wapenwedloop is. Aanvaltechnieken evolueren en hackers en cybercriminelen vinden altijd nieuwe methoden en technieken om de miljarden-apps te kraken die we allemaal elke dag gebruiken.

Er worden hele nieuwe klassen van bugs ontdekt omdat iemand, ergens, een slimme manier heeft gevonden om aannames te doorbreken waarvan de industrie zich niet eens realiseerde dat ze die maakte. Formele verificatie heeft als doel een andere verdedigingslinie te bieden tegen deze “unknown unknowns”.

Sagiv beschrijft een patroon dat Certora herhaaldelijk heeft gezien. Teams kunnen alles “right” doen, enorme interne middelen inzetten voor beveiliging, elite-auditors inhuren, en dan komen er door formele verificatie nog steeds extra problemen van hoge ernst aan het licht.

“Je laat de beste [beveiligingsonderzoeker]… 10 kritieke vinden. Je bent erg blij. En dan voer je formele verificatie uit. Die vindt er nog twee.”

Deze stelling werd verder versterkt door Certora’s Formal Verification Team Lead Pamina Georgiev, die het podium betrad tijdens Solana Breakpoint om het belang en de impact van FV te illustreren.

Desondanks alle belofte en bescherming die formele verificatie biedt, is het’s nog steeds verre van een perfect systeem. Formele verificatie is nauwelijks een ondoordringbaar krachtveld dat hackers tegenhoudt, ondanks wat bepaalde cryptotwitteraars je willen doen geloven.

Sagiv is bot over waarom die framing gevaarlijk is.

“Het grootste probleem [bij] formele verificatie is begrijpen welke eigenschap je moet [specificeren]”.

Formele verificatie bewijst niet dat de code veilig is in absolute zin. Het bewijst dat de code voldoet aan een set eigenschappen; eigenschappen die je vroeg om te bewijzen. Als je de verkeerde eigenschappen kiest, eindig je met iets dat er zeer geloofwaardig uitziet, maar verre van waterdicht is.

CI, Automatisering en “No Human in the Loop”

Eén van Sagiv’s duidelijkste punten op Breakpoint is dat beveiliging geen eenmalige gebeurtenis is. Het is niet omdat een applicatie een audit kreeg enkele jaren geleden dat het vandaag nog steeds veilig zal zijn. Dit is vooral waar in crypto, waar protocollen en aanvalsmethoden voortdurend veranderen en veranderingen in een enkele regel code gevolgen kunnen hebben elders in de stack.

“Het verandert compleet, één verandering van één regel kan de hele code breken.”

Dat is waarom Certora verificatie in de workflow van ontwikkelaars duwt. Sagiv zegt dat Certora integreert in CI-pijplijnen, zodat elke nieuwe commit automatisch verificatiecontroles triggert, waardoor een continue vangrail ontstaat in plaats van een eenmalige mijlpaal.

“Elke keer als ze iets veranderen, ze een commit doen in de code, draaien we formele verificatie. Dat is eigenlijk het mooie van onze tool. Onze tool is automatisch; de mens zit niet in de lus.”

Certora onderhoudt speciale documentatie voor formele verificatie van Solana-programma's, met de “Certora Solana Prover” ontworpen om Solana smart contracts geschreven in Rust te verifiëren.

Cypherpunks & Academia

In tegenstelling tot veel crypto-oorsprongsverhalen, die vaak geworteld zijn in een cypherpunk, anti-establishment ethos, brengt Sagiv wat broodnodige academische klasse naar de industrie. Hij beschrijft zijn overgang van de academische wereld als een botsing tussen intellectuele uitdaging en echte inzet.

“Crypto is het enige domein waar je kleine code hebt die veel waarde met zich meedraagt”

In traditionele veiligheidskritische software is de code misschien wel enorm, maar vaak oud, stabiel en de complete antithese van crypto’s snelle iteratie. Dit kan hebben gediend als de basis voor een van Certora’s favoriete slogans: “Move fast and break nothing”

Sagiv ziet crypto als perfect geschikt voor formele methoden omdat zoveel inherent wiskundig is: evenwichten, invarianten, behoudsbeperkingen, toegangscontroleregels en toestandsovergangen die nauwkeurig kunnen worden uitgedrukt.

“Ik geef nog steeds academische lezingen. Sommige mensen houden niet van cryptografie. Ik probeer ze te motiveren voor de technische kant. Ik ga terug naar de technische kant en vertel ze wat een uitdaging is.”

Zelfs als zijn academische collega's sceptisch zijn over crypto, benadrukt Sagiv dat crypto een van de meer stimulerende en motiverende gebieden van de computerwetenschap is voor opkomende ontwikkelaars.

Solana’s “Can-Do Attitude”

Certora is zeker geen exclusief beveiligingsbedrijf voor Solana, maar dat betekent niet dat het bedrijf niet diep verweven is in de DeFi-scene van de keten. Sagiv heeft gewerkt met enkele van Solana’s grootste en invloedrijkste applicaties en biedt het ecosysteem een niveau van operationeel respect dat alleen ontstaat als je schouder aan schouder staat met topteams.

p dir">p dir">p dir">squo"

Certora’s eerste Solana-engagement was met Squads, die Sagiv “amazing.&rdquo noemt; Van daaruit werkte Certora met de Solana Foundation en controleerde eigenschappen van SPL-programma's, waarbij hij de samenwerking als ongewoon ontvankelijk beschreef.

Wat het meest opvalt is zijn vergelijking met andere omgevingen. Over zijn ervaring met Solidity Developers merkte Sagic op dat teams resistent kunnen zijn tegen veranderingen.

“Als we met mensen praten, soms in Solidity, en hen vragen om code te veranderen zijn ze erg terughoudend. Ze zeggen dat we een beperkte hoeveelheid tijd hebben… Hier [Solana] hebben mensen meer een ‘can do’ houding. Als je ze vraagt om de code te veranderen, zijn ze heel recht door zee.”

Veiligheidsbedreigingen in 2026

Op de vraag naar de grootste bedreigingen waar mensen zich in 2026 bewust van moeten zijn, benadrukte Sagiv opnieuw dat mensen zich niet moeten blindstaren op kwetsbaarheden in code. Goede operationele beveiliging is een veelzijdig beest, en de gemiddelde cryptobezitter heeft veel meer kans om het slachtoffer te worden van social engineering of een bewaringsfout dan om geld te verliezen door een DeFi exploit.

“We zien van alles gebeuren, het’is niet alleen de code.”

Hij heeft geen ongelijk. Volgens Chainalysis’ 2025 Crypto Crime Report, hebben fraudeurs meer dan $14B gestolen in de loop van 2025 in alweer een recordhoogte.

Sagiv is ook van mening dat de AI-dreiging buiten proportie wordt opgeblazen. Zoals je zou verwachten van een beveiligingsprofessional, beschouwt Certora’s Chief Scientist AI niet als een kwaadaardige bedreiging, maar als een hulpmiddel. Toegegeven, AI kan dienen als een multiplicator voor aanvallers, maar het kan ook worden gebruikt door verdedigers en beveiligingsbedrijven. 

“De slechteriken kunnen AI gebruiken. De goeden kunnen AI gebruiken,”

Als AI helpt kwetsbaarheden te vinden, kan het ook helpen eigenschappen te bewijzen, sterkere specificaties te genereren en verificatieproblemen op te lossen.

Crypto zal nooit “volledig veilig zijn,” en Solana zal’niet immuun zijn voor wat de volgende aanvalsgolf ook bedenkt. Maar de weg voorwaarts blijft trouw aan Crypto Security 101: Versterk sleutelbeheer, gebruik gezond verstand en behandel veiligheid als iets dat je continu bewijst, niet als iets dat je één keer verklaart en dan vergeet.

Lees meer over SolanaFloor

De enige zekerheid is onzekerheid.

Chinees-Canadese handelsbesprekingen, yen-inflatie en alweer een regeringsstop jagen cryptomarkten de stuipen op het lijf

SolanaFloor zit aan tafel met Certora’s Mooly Sagiv