Securing Smart Contracts Against Business Logic Flaws

QC 20250507

Abstract

Blockchainbaserade smarta kontrakt ger stöd för decentraliserade applikationer (DApps) genom att möjliggöra tillitslösa, transparenta och oföränderliga transaktioner. Emellertid innebär denna oföränderlighet att brister i design eller implementering leder till oåterkalleliga och kostsamma säkerhetsincidenter. Därför är rigorös verifiering och analys av smarta kontrakt innan driftsättning avgörande. Vidare kan inte alla sårbarheter upptäckas på förhand, varför övervakning efter driftsättning också är kritiskt. 

En särskilt utmanande men tämligen outforskad klass av sårbarheter i smarta kontrakt är affärslogikbrister (BLF), som uppstår när den implementerade logiken avviker subtilt men kritiskt från det avsedda beteendet. BLF:er är svåra att upptäcka eftersom de ofta kräver en djup förståelse av de avsedda affärsreglerna snarare än enbart kodnivåanalys. Denna klass av sårbarheter har överlag förbisetts i befintlig litteratur. Den här avhandlingen introducerar ett omfattande ramverk för att hantera sårbarheter under hela säkerhetslivscykeln för DApps – från specifikation och analys före - till övervakning efter - driftsättning – med fokus på att upptäcka, förebygga och hindra BLF:er.

I grunden formaliserar vårt arbete affärslogik på hög nivå för kontrakt med hjälp av Dynamic Condition Response (DCR)-grafer. Vi kategoriserar designmönster som antingen lågnivå (plattforms- och implementeringsspecifika) eller högnivå (affärslogiska) designmönster. Vi formaliserar högnivåmönster, såsom tidsbaserade begränsningar och handlingsberoenden, med grafiska formella modeller. Dessa modeller ger utvecklare en tydlig visuell översikt över de avsedda kontraktsarbetsflödena.Formaliserade kontrakt underlättar inte bara automatiserad verifiering och analys utan lägger också grunden för vår "modellera för att hindra"-metod. I denna metod kopplas smarta kontraktsfunktioner till DCR-aktiviteter, och logiken modelleras med hjälp av DCR-relationer för att avslöja designfel genom att göra tidigare implicita antaganden om koden explicita. 

Som komplement till våra bidrag i designfasen föreslår vi ett off-chain-övervakningsverktyg som observerar on-chain-transaktioner. Genom att koppla varje transaktion mot den DCR-specificerade logiken upptäcker detta verktyg avvikelser från det avsedda beteendet utan att instrumentera det driftsatta kontraktet. Dessutom kan vår metod effektivt upptäcka komplexa cross-chain-attacker och överträdelser av specificerade beteenden, vilket bidrar till att öka säkerheten för de allt mer populära cross-chain DApps. Vi tar itu med bristen på konkreta exploateringsscenarier för BLF:er genom att använda stora språkmodeller (LLM) för att injicera realistiska BLF:er i kontrakt och syntetisera motsvarande exploateringar. Vårt angreppssätt använder DCR-baserade formella specifikationer som vägledning, vilket säkerställer att de syntetiserade sårbarheterna är både representativa och realistiska. 

Med insikten om behovet av rigorösa invarianter för att upprätthålla säkerhet utvecklar vi ett semantiskt verktyg för invariantdifferentiering som, givet två smarta kontraktsinvarianter, avgör vilken som är starkare. Våra experiment visar på verktygets effektivitet att filtrera bort redundanta eller svaga invarianter och därigenom ge mer användbara dynamiskt utvunna invarianter. Därutöver, beaktandes vikten av blockchain-orakelsäkerhet, föreslår vi en modell för datalivscykeln för orakel som löper från dataskapande till dess utfasning. Vi identifierar systematiskt sårbarheter i varje steg av denna modell och kartlägger hindrande strategier. 

Sammanfattningsvis erbjuder dessa bidrag ett helhetsangreppssätt för smart kontraktssäkerhet genom att koppla ihop formell design och analys, dynamisk övervakning samt förfining av invarianter – allt för att bygga mer motståndskraftiga decentraliserade applikationer.

urn.kb.se/resolve?urn=urn:nbn:se:kth:diva-363085