Project title : Detecting Logic Vulnerabilities in Smart Contracts
Team No.: 2
Team Members: Amisha Verma
Merina Thoppil
Ashita Salis
Shaun Rodrigues
Problem Definition:
Smart contracts are self-executing programs deployed on blockchain platforms, designed to operate with
trustless execution. However, due to the immutable nature of smart contracts once deployed, any logic flaw
or vulnerability can lead to severe consequences such as financial loss, data leakage, or exploitation by
malicious users.Traditional bug detection tools are often insufficient in capturing nuanced logic
vulnerabilities that are specific to the behavior and state changes of smart contracts. Therefore, there is a
critical need to develop and apply advanced techniques such as formal verification, symbolic execution, and
comprehensive static and dynamic analysis to detect these logic flaws early in the development cycle.This
project aims to explore and implement a systematic approach that improves the accuracy and coverage of
logic vulnerability detection in smart contracts, ensuring more secure decentralized applications.
Objectives:
1. To identify and classify logic vulnerabilities in smart contracts that can cause unintended behaviors
or financial loss.
2. To explore and apply advanced techniques such as:
- Formal verification (mathematical correctness proofs),
- Symbolic execution (systematic path exploration),
- Static and dynamic analysis (code and runtime behavior inspection).
3. To design or use an automated tool/framework that detects logic flaws during smart contract
development.
4. To evaluate the effectiveness of the detection methods by testing them on real-world smart contracts
(e.g., Ethereum-based).
5. To minimize false positives and false negatives in vulnerability detection through hybrid or enhanced
techniques.
6. To provide recommendations or best practices for secure smart contract development.
Scope:
This project focuses on detecting logic-level vulnerabilities in smart contracts, particularly those written in
the Solidity programming language and deployed on the Ethereum blockchain. The primary aim is to
identify flaws such as reentrancy, improper access control, integer overflows/underflows, front-running, and
incorrect state transitions—vulnerabilities that can lead to financial loss or unintended contract behavior.
The scope involves the use and evaluation of advanced detection techniques, including formal verification,
symbolic execution, and static and dynamic analysis. Existing tools such as Mythril, Slither, Manticore, and
Oyente may be utilized or extended to support the analysis process. The project does not cover
vulnerabilities caused by compiler bugs, gas inefficiencies, or consensus-level blockchain issues. The
outcome will include a comprehensive assessment of vulnerabilities in selected smart contracts and the
effectiveness of the detection techniques used, along with recommended best practices for developing secure
smart contracts.
Summary of Research paper:
Year Title Author Summary Limitation
2024 GPTScan: Detecting Yuqiang Sun, Combines GPT (LLM) and static Limited precision on
Logic Vulnerabilities Daoyuan Wu, analysis to detect logic large projects like
in Smart Contracts by Yue Xue, et vulnerabilities in smart contracts. Web3Bugs (57.14%);
Combining GPT with al. Achieves high precision and cost- relies on GPT-3.5, may
Program Analysis effective detection across 400 miss complex logic
projects. beyond context size.
2024 Uncover the Shuo Yang, Introduces BlockWatchdog to Focused on reentrancy;
Premeditated Attacks: Jiachi Chen, detect exploitable reentrancy other vulnerability types
Detecting Exploitable et al. vulnerabilities by identifying not addressed; relies
Reentrancy attacker contracts. Uses static heavily on bytecode-level
Vulnerabilities by cross-contract dataflow analysis. analysis.
Identifying Attacker
Contracts
2024 Efficiently Detecting Zexu Wang, Proposes SliSE, a two-stage tool Designed mainly for
Reentrancy Jiachi Chen, combining program slicing and reentrancy in complex
Vulnerabilities in et al. symbolic execution for detecting contracts; other
Complex Smart reentrancy vulnerabilities in vulnerability types not
Contracts complex contracts. Achieves high deeply explored.
F1 and recall scores.
2024 Smart Contract and Stefanos Evaluates real-world effectiveness Most tools fail on
DeFi Security Tools: Chaliasos, of five security tools across 127 logic/protocol
Do They Meet the Arthur attacks; shows only 8% of attacks vulnerabilities; current
Needs of Practitioners? Gervais, et al. could be prevented. Highlights tools generate too many
practitioner feedback. false positives.
2024 Defining Smart Jiachi Chen, Defines 20 types of smart contract Focuses on classification
Contract Defects on Xin Xia, defects from empirical analysis and and perception, not
Ethereum David Lo, et survey. Categorizes defects into automatic detection; does
al. five quality aspects. not provide a detection
tool.
2020 VERISMART: A Sunbeom So, Proposes VERISMART for precise Mainly targets arithmetic
Highly Precise Safety Hakjoo Oh, et and exhaustive arithmetic safety bugs; does not address
Verifier for Ethereum al. verification using transaction broader vulnerability
Smart Contracts invariants. Achieves negligible categories.
false positives.
2019 MPro: Combining William Introduces MPro combining Primarily focused on
Static and Symbolic Zhang, Vijay Mythril and Slither to detect depth- depth-n vulnerabilities;
Analysis for Scalable Ganesh, et al. n vulnerabilities efficiently via may miss shallow bugs
Testing of Smart symbolic and data dependency and complex logic issues.
Contracts analysis.
2018 ZEUS: Analyzing Sukrit Kalra, Proposes ZEUS, a symbolic model Limited Solidity support
Safety of Smart Seep Goel, et checking framework using LLVM initially; fairness
Contracts al. bitcode and CHCs for verifying conditions depend on
correctness and fairness. Evaluated user input; does not
on 22.4K contracts. support dynamic
Year Title Author Summary Limitation
2024 GPTScan: Detecting Yuqiang Sun, Combines GPT (LLM) and static Limited precision on
Logic Vulnerabilities Daoyuan Wu, analysis to detect logic large projects like
in Smart Contracts by Yue Xue, et vulnerabilities in smart contracts. Web3Bugs (57.14%);
Combining GPT with al. Achieves high precision and cost- relies on GPT-3.5, may
Program Analysis effective detection across 400 miss complex logic
projects. beyond context size.
2024 Uncover the Shuo Yang, Introduces BlockWatchdog to Focused on reentrancy;
Premeditated Attacks: Jiachi Chen, detect exploitable reentrancy other vulnerability types
Detecting Exploitable et al. vulnerabilities by identifying not addressed; relies
Reentrancy attacker contracts. Uses static heavily on bytecode-level
Vulnerabilities by cross-contract dataflow analysis. analysis.
Identifying Attacker
Contracts
2024 Efficiently Detecting Zexu Wang, Proposes SliSE, a two-stage tool Designed mainly for
Reentrancy Jiachi Chen, combining program slicing and reentrancy in complex
Vulnerabilities in et al. symbolic execution for detecting contracts; other
Complex Smart reentrancy vulnerabilities in vulnerability types not
Contracts complex contracts. Achieves high deeply explored.
F1 and recall scores.
behavior.
