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

要約

Ethereumで実行されるスマートコントラクトを管理するために、それぞれがスマート契約の行動を導くための一連のルールを持っているコメント（ERC）標準の複数のイーサリアムリクエストが開発されました。
ERCルールに違反すると、深刻なセキュリティの問題と経済的損失を引き起こす可能性があり、ERCに従うスマートコントラクトを確認することの重要性を示しています。
このような検証の今日の慣行は、各単一の契約を手動で監査したり、専門家が開発したプログラム分析ツールを使用したり、大規模な言語モデル（LLMS）を使用したりすることです。これらはすべて、ERCルール違反の特定に効果的ではありません。
このペーパーでは、Symgptを紹介します。Symgptは、大規模な言語モデル（LLMS）の自然言語の理解と、Smart ContractsのERCルールへのコンプライアンスを自動的に検証するためのシンボリック実行の正式な保証を組み合わせたツールを紹介します。
Symgptを開発するために、コンテンツ、セキュリティの意味合い、自然言語の説明を調べる、広く使用されている3つのERC標準から132のERCルールの経験的研究を実施します。
この研究に基づいて、最初にLLMにERCルールを定義されたEBNF文法に変換するよう指示することによりSymgptを設計します。
次に、正式なルールからの制約を統合して、違反が発生する可能性のあるシナリオを表し、シンボリック実行を使用してそれらを検出します。
私たちの評価は、Symgptが、金融資産を盗むための明確な攻撃経路を伴う1,375の違反を含む4,000の実世界契約で5,783のERCルール違反を特定し、その有効性を実証することを示しています。
さらに、Symgptは、6つの自動化された手法とセキュリティ専門家の監査サービスを上回り、現在のスマート契約分析方法よりも優位性を強調しています。

要約(オリジナル)

To govern smart contracts running on Ethereum, multiple Ethereum Request for Comment (ERC) standards have been developed, each having a set of rules to guide the behaviors of smart contracts. Violating the ERC rules could cause serious security issues and financial loss, signifying the importance of verifying smart contracts follow ERCs. Today’s practices of such verification are to manually audit each single contract, use expert-developed program-analysis tools, or use large language models (LLMs), all of which are far from effective in identifying ERC rule violations. This paper introduces SymGPT, a tool that combines the natural language understanding of large language models (LLMs) with the formal guarantees of symbolic execution to automatically verify smart contracts’ compliance with ERC rules. To develop SymGPT, we conduct an empirical study of 132 ERC rules from three widely used ERC standards, examining their content, security implications, and natural language descriptions. Based on this study, we design SymGPT by first instructing an LLM to translate ERC rules into a defined EBNF grammar. We then synthesize constraints from the formalized rules to represent scenarios where violations may occur and use symbolic execution to detect them. 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 stealing financial assets, demonstrating its effectiveness. Furthermore, SymGPT outperforms six automated techniques and a security-expert auditing service, underscoring its superiority over current smart contract analysis methods.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google