SymGPT: Auditing Smart Contracts via Combining Symbolic Execution with Large Language Models

TL;DR

SymGPT is a novel tool that combines large language models with symbolic execution to automatically verify Ethereum smart contracts' compliance with ERC rules, significantly improving detection of violations and potential security breaches.

Contribution

This paper introduces SymGPT, the first system to integrate LLMs with symbolic execution for automated ERC compliance verification in smart contracts.

Findings

Identified 5,783 ERC rule violations in real-world contracts

Detected 1,375 violations with attack paths for theft

Outperformed existing automated tools and expert audits

Abstract

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each defining a set of rules governing contract behavior. Violating these rules can cause serious security issues and financial losses, signifying the importance of verifying ERC compliance. Today's practices of such verification include manual audits, expert-developed program-analysis tools, and large language models (LLMs), all of which remain ineffective at detecting ERC rule violations. This paper introduces SymGPT, a tool that combines LLMs with symbolic execution to automatically verify smart contracts' compliance with ERC rules. We begin by empirically analyzing 132 ERC rules from three major ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, SymGPT instructs an LLM to translate ERC rules into a domain-specific language, synthesizes constraints from the translated rules to model potential rule violations, and performs symbolic execution for violation detection. Our evaluation shows that SymGPT identifies 5,783 ERC rule violations in 4,000 real-world contracts, including 1,375 violations with clear attack paths for financial theft. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.