論文の概要: Soliduzz: Finding Miscompilations in Smart-Contract Compilers with Assertion-Driven Equivalence Oracles
- arxiv url: http://arxiv.org/abs/2610.18165v1
- Date: Tue, 13 Oct 2026 11:10:04 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-10-17 07:02:56.084395
- Title: Soliduzz: Finding Miscompilations in Smart-Contract Compilers with Assertion-Driven Equivalence Oracles
- Title(参考訳): Soliduzz: Assertion-Driven Equivalence Oracleによるスマートコントラクトコンパイラの誤コンパイルを見つける
- Abstract要約: Soliduzzは、アサーション駆動の等価オーラクルを使用して、EVMスマートコントラクトコンパイラの誤コンパイルを見つけるためのアプローチである。
私たちのシンボリックEMIは、元の計算でカバレッジを記録し、変換された突然変異を保護するためにそれを使用します。
いくつかの解析ツールを用いて3つのEVMスマートコントラクトコンパイラ(ソルク、ソルク、ビーパー)上でSoliduzzを評価した。
- 参考スコア(独自算出の注目度): 42.57282810107734
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Smart contracts compiled to the Ethereum Virtual Machine (EVM) can manage high-value assets and are difficult to patch after deployment. Compiler miscompilations are therefore especially dangerous: compilation succeeds, but the generated bytecode does not preserve the semantics of the source program. Existing smart-contract compiler fuzzers either focus on robustness failures or rely on differential oracles that compare compiler configurations. We present Soliduzz, an approach for finding miscompilations in EVM smart-contract compilers using assertion-driven equivalence oracles. Soliduzz uses product programs to encode semantic equivalence as executable assertions. The key shift is to compile these self-checking programs and let off-the-shelf fuzzers and symbolic execution engines explore the resulting bytecode for assertion violations, without requiring compiler-specific support from the analyzer. Soliduzz instantiates this idea with two complementary families of metamorphic transformations. The first starts from equivalent expressions and lifts them into smart-contract code that deliberately exercises EVM-specific features such as storage, data locations, control flow, contract interactions, and inline assembly. The second generalizes Equivalence Modulo Inputs (EMI) from fixed concrete inputs to symbolic input spaces. Our symbolic EMI records coverage in the original computation and uses it to guard mutations in the transformed computation. Together, these transformations produce product programs that assert that paired computations yield the same outputs. We evaluate Soliduzz on three EVM smart-contract compilers (solc, solx, and vyper) using several analysis tools. Overall, Soliduzz exposes 29 bugs. Of these, 24 are compiler bugs: 6 miscompilations, 17 internal compiler errors, and 1 hang. The remaining 5 are bugs in the analysis tools.
- Abstract(参考訳): Ethereum仮想マシン(EVM)にコンパイルされたスマートコントラクトは、高価値な資産を管理することができ、デプロイ後にパッチを適用できない。
コンパイルは成功するが、生成されたバイトコードはソースプログラムのセマンティクスを保存しない。
既存のスマートコントラクトコンパイラファザは、堅牢性障害に焦点を当てるか、あるいはコンパイラ構成を比較するための差分オラクルに依存している。
本稿では,アサーション駆動等価オラクルを用いたEVMスマートコントラクトコンパイラの誤コンパイル検出手法であるSoliduzzを提案する。
Soliduzzは製品プログラムを使用してセマンティック等価性を実行可能なアサーションとしてエンコードする。
重要なシフトは、これらの自己チェックプログラムをコンパイルし、アナライザからコンパイラ固有のサポートを必要とせずに、既製のファズーとシンボリック実行エンジンがアサーション違反の原因となるバイトコードを探索することです。
Soliduzzはこのアイデアをメタモルフィック変換の2つの相補的な族でインスタンス化する。
1つ目は同等の式から始まり、ストレージ、データロケーション、制御フロー、コントラクトのインタラクション、インラインアセンブリといったEVM固有の機能を意図的に実行したスマートコントラクトコードへと持ち上げる。
2つ目は、Equivalence Modulo Inputs (EMI) を固定されたコンクリート入力からシンボル入力空間へ一般化する。
我々のシンボリックEMIは、元の計算におけるカバレッジを記録し、変換された計算における突然変異を保護するためにそれを使用する。
これらの変換は、ペア化された計算が同じ出力を得ると主張する製品プログラムを生成する。
いくつかの解析ツールを用いて3つのEVMスマートコントラクトコンパイラ(ソルク、ソルク、ビーパー)上でSoliduzzを評価した。
Soliduzzは29のバグを公開している。
そのうち24は、コンパイラのバグである。6つの誤コンパイル、内部のコンパイラエラー17、ハング1である。
残りの5つは分析ツールのバグである。
関連論文リスト
- SCDBench: A Benchmark for LLM-Based Smart Contract Decompilers [55.39407031861402]
本稿では,スマートコントラクトデコンパイルのためのデータセットとベンチマーク手法であるSCDBenchを紹介する。
データセットには600の現実のSolidityコントラクトと、ペア化されたバイトコード入力、地味なソースコード、再生可能なセマンティックチェックポイントが含まれている。
我々は,GLM-5の変種を含むゼロショット逆コンパイル設定において,Claude Opus 4.7,GPT-5.3-Codex,GLM-5を評価した。
論文 参考訳(メタデータ) (2026-05-27T20:08:47Z) - Decaf: Improving Neural Decompilation with Automatic Feedback and Search [64.02615739798277]
高レベルな構文、識別子、カスタムデータ型は一般的に失われ、コンパイラは人間可読なコードを低レベルなマシンコードに変換する。
生成AIモデルは、ハイレベルな構文、識別子、型を再構築するのに自然なものだ。
コンパイラフィードバックは,サーチによるニューラルデコンパイラ出力のセマンティックな正当性の向上に有効である,と我々は主張する。
論文 参考訳(メタデータ) (2026-05-12T04:21:26Z) - ParityFuzz: Finding Inconsistencies across Solidity Compilers via Fine-Grained Mutation and Differential Analysis [37.31248744457945]
ParityFuzzは、Solidity用のクロスコンパイラ差分テストフレームワークである。
コンパイラと実行環境を分析して、構文や境界指向のルールを含む突然変異ルールを導出する。
複数のコンパイラにまたがってプログラムをコンパイルして実行し、その結果を正規化し、比較して不整合を検出する。
論文 参考訳(メタデータ) (2026-05-09T16:53:45Z) - Finding Compiler Bugs through Cross-Language Code Generator and Differential Testing [4.072167151876496]
CrossLangFuzzerは多種多様な型パラメータと複雑な継承構造を持つ言語横断のテストプログラムを生成する。
Kotlinコンパイラの10のバグ、Groovyコンパイラの4つのバグ、Scala 3コンパイラの7つのバグ、Scala 2コンパイラの2つのバグ、Javaコンパイラの1つのバグを発見した。
論文 参考訳(メタデータ) (2025-07-09T06:33:06Z) - ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。
このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
論文 参考訳(メタデータ) (2025-02-17T12:38:57Z) - Towards Understanding the Bugs in Solidity Compiler [11.193701473232851]
本稿では,533のSolidityコンパイラのバグに関する最初の系統的研究について述べる。
本研究は, その特徴(症状, 根本原因, 分布など)とトリガー試験例について検討した。
次に,Solidityコンパイラファザの限界について検討するため,Solidityコンパイラファザを3つ評価した。
論文 参考訳(メタデータ) (2024-07-08T14:22:50Z) - Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。
確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。
Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文 参考訳(メタデータ) (2023-09-25T15:42:18Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。