Blockchain smart contracts empower decentralized applications (DApps) by enabling trustless, transparent, and immutable transactions. However, this immutability means that flaws in design or implementation lead to irreversible and costly security breaches. Therefore, rigorous verification and analysis of smart contracts before deployment is crucial. Furthermore, since not all vulnerabilities are detectable pre-deployment, monitoring after deployment is equally critical.

One particularly challenging yet understudied class of vulnerabilities in smart contracts is business logic flaws (BLFs), which occur when the implemented logic deviates subtly but critically from the intended behavior. BLFs are challenging to detect because they often require a deep understanding of the intended business rules rather than merely code-level analysis. This class of vulnerabilities has largely been overlooked in existing literature. This thesis introduces a comprehensive framework to address vulnerabilities across the entire DApp security lifecycle from specification and pre-deployment analysis to post-deployment monitoring with an emphasis on detecting, preventing, and mitigating BLFs.

At its core, our work formalizes high-level business logic of contracts using Dynamic Condition Response (DCR) graphs. We categorize design patterns into low-level platform/implementation specific and high-level business logic design patterns. We formalize the high-level patterns such as time-based constraints and action dependencies into precise graphical formal models. These models provide developers with a clear visual blueprint of intended contract workflows. Formalized contracts not only facilitate automated verification and analysis but also lay the groundwork for our "model to mitigate" approach. In this methodology, smart contract functions are mapped to DCR activities and its logic is modeled using DCR relations to expose design flaws by making implicit assumptions about the code explicit. 

Complementing our design-phase contributions, we propose an off-chain monitoring tool that observes on-chain transactions. By mapping each transaction against the DCR-specified logic, this tool detects deviations from intended behavior without instrumenting the deployed contract. Furthermore, our method effectively detects complex cross-chain attacks and violations of the specified behavior to secure the increasingly popular cross-chain DApps.

We address the lack of concrete exploit scenarios for business logic vulnerabilities using Large Language Models (LLMs) to inject realistic BLFs into contracts and synthesize corresponding exploits. Our approach uses DCR-based formal specifications as guidance, ensuring that synthesized vulnerabilities are both representative and realistic.

Recognizing the need for rigorous invariants to enforce security, we develop a semantic invariant differencing tool that given two smart contract require/assert statements it produces a verdict of which one is stronger. Our experiments prove its effectiveness in filtering out redundant or weak invariants to enhance the usefulness of dynamically mined invariants. In parallel, acknowledging the pivotal role of blockchain oracle security, we propose an oracle data lifecycle model spanning from the creation of data to its deprecation. We systematically identify vulnerabilities at each stage of this model and survey mitigation strategies.

Collectively, these contributions provide an end-to-end approach to smart contract security by bridging formal design and analysis, dynamic monitoring, and invariant refinement to build more resilient decentralized applications.

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.