Securing Smart Contracts Against Business Logic Flaws

QC 20250507

Abstract

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.

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