  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.
