用大模型+符号与具体执行，精准验证以太坊智能合约漏洞
Validating Solidity Code Defects using Symbolic and Concrete Execution powered by Large Language Models
- 结合大模型与符号/具体执行，自动识别漏洞
- 对三种高危漏洞检测准确率显著提升
- 适合安全审计人员和自动化工具开发者
静态分析工具和大语言模型（LLMs）在以太坊智能合约漏洞检测中存在高误报率，难以可靠验证缺陷。本文提出一种新型检测流程，整合基于Slither的自定义检测器、大语言模型（LLMs）、Kontrol和Forge。该方法能有效识别七类关键缺陷，并在三种复杂漏洞——重入攻击、复杂回退函数、访问控制策略错误——上取得显著成果。传统验证方案常产生误报或漏检，而本方法通过符号或具体执行正确分类缺陷，显著减少人工验证工作量。尽管存在大模型不一致性和成本问题，研究结果表明，将启发式分析与形式化验证结合，可构建更可靠、自动化的智能合约审计框架。
原文摘要 · Abstract (English)
The high rate of false alarms from static analysis tools and Large Language Models (LLMs) complicates vulnerability detection in Solidity Smart Contracts, demanding methods that can formally or empirically prove the presence of defects. This paper introduces a novel detection pipeline that integrates custom Slither-based detectors, LLMs, Kontrol, and Forge. Our approach is designed to reliably detect defects and generate proofs. We currently perform experiments with promising results for seven types of critical defects. We demonstrate the pipeline's efficacy by presenting our findings for three vulnerabilities -- Reentrancy, Complex Fallback, and Faulty Access Control Policies -- that are challenging for current verification solutions, which often generate false alarms or fail to detect them entirely. We highlight the potential of either symbolic or concrete execution in correctly classifying such code faults. By chaining these instruments, our method effectively validates true positives, significantly reducing the manual verification burden. Although we identify potential limitations, such as the inconsistency and the cost of LLMs, our findings establish a robust framework for combining heuristic analysis with formal verification to achieve more reliable and automated smart contract auditing.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。