Hunting DeFi Vulnerabilities via Context-Sensitive Concolic Verification
Yepeng Ding, Arthur Gervais, Roger Wattenhofer, Hiroyuki Sato
TL;DR
The paper addresses DeFi vulnerability detection by analyzing 80 real-world incidents and identifying six root causes that challenge existing analysis tools. It introduces Context-Sensitive Concolic Verification (CSCV), which combines context construction and optimization with concolic verification to search for attack vectors under user-defined temporal properties, using a context-carrying transition system to guide exploration. The authors formalize context construction, optimization, and concolic verification, and demonstrate the approach on a Java-based prototype backed by the Z3 solver, achieving detection across all six vulnerability types and substantial attack-vector coverage, with a notable fraction of previously unknown vectors discovered under heuristic guidance. The work offers a practical pathway to more robust automated DeFi security, improving coverage of diverse vulnerability classes and enabling scalable, property-driven analysis for smart contracts in decentralized finance.
Abstract
Decentralized finance (DeFi) is revolutionizing the traditional centralized finance paradigm with its attractive features such as high availability, transparency, and tamper-proofing. However, attacks targeting DeFi services have severely damaged the DeFi market, as evidenced by our investigation of 80 real-world DeFi incidents from 2017 to 2022. Existing methods, based on symbolic execution, model checking, semantic analysis, and fuzzing, fall short in identifying the most DeFi vulnerability types. To address the deficiency, we propose Context-Sensitive Concolic Verification (CSCV), a method of automating the DeFi vulnerability finding based on user-defined properties formulated in temporal logic. CSCV builds and optimizes contexts to guide verification processes that dynamically construct context-carrying transition systems in tandem with concolic executions. Furthermore, we demonstrate the effectiveness of CSCV through experiments on real-world DeFi services and qualitative comparison. The experiment results show that our CSCV prototype successfully detects 76.25% of the vulnerabilities from the investigated incidents with an average time of 253.06 seconds.