決定論的なバイナリ全体翻訳:ヒューリスティックを超えて
バイナリ翻訳(実行ファイルをある命令セットアーキテクチャ(ISA)から別のものへ変換するプロセス)は、長らくパフォーマンスと正確性の間の戦いとなってきました。伝統的に、開発者はJust-In-Time (JIT) コンパイル、またはヒューリスティックに基づいた静的翻訳に依存してきました。JITは高いパフォーマンスを提供しますが、実行時のオーバーヘッドとセキュリティリスクを伴い、一方でヒューリスティックは、複雑なバイナリパターンや難読化されたコードに遭遇した際に失敗することがよくあります。
論文 Deterministic Fully-Static Whole-Binary Translation Without Heuristics (「Elevator」と呼ばれるツールを導入)では、新しいアプローチが提案されています。それは、ヒューリスティックを完全に排除するという急進的な転換です。バイナリ内のすべてのバイトのあらゆる可能な解釈を考慮することで、Elevatorは、実行時の翻訳レイヤーを必要とせずに正確性を保証する決定論的な翻訳を目指しています。
コアメカニズム:Superset CFG
静的翻訳における主な課題は「デサセンブル(逆アセンブル)問題」です。多くのバイナリでは、コードとデータが混在しており、特定のバイトが命令なのかデータの一部なのかを静的に判断することはしばしば不可能です。
ヒューリスティックに基づいた翻訳機は推測を行おうとしますが、間違いを犯すことがあります。
Elevatorは、Superset Control Flow Graph (CFG) を構築することでこれを解決します。コードがどこから始まるかを推測する代わりに、、すべてのバイトを命令の潜在的な開始点として扱います。そして、バイナリのバイトのあらゆる実行可能な解釈に対して、個別の翻訳を生成します。もし複数のパスが同じバイトに到達する可能性がある場合、Elevatorはそれらすべてのパスに対してコードを生成します。
このアプローチにより、元のプログラムがコードブロックにどのようにジャンプしたとしても、翻訳されたバージョンには対応する有効なパスが存在することが保証されます。削除される唯一のパスは、「異常終了」(例:即時のクラッシュ)につながるパスのみであり、これにより、結果として得られるバイナリは元のプログラムの完全かつ決定論的なマッピングとなります。
トレードオフ:パフォーマンス vs. ブロート(肥大化)
Elevatorの決定論的な性質は画期的なものですが、それには大きなコストが伴います。コミュニティの議論では、いくつかの重要なトレードオフが強調されています。
1. バイナリサイズの爆発
最も顕著な結果の一つは、バイナリサイズの増加です。翻訳されたバイナリは、元のバイナリよりも最大50倍大きくなることがあります。
"A 50x increase in the size of the .text section is enormous, but seems to be a reasonable price to pay for a fully-deterministic translation." — @linkregister
しかし、他の人々はこれを「キャッシュの災難」であると主張しています。コードセクションが50倍に増加すると、大規模な命令キャッシュミスが発生し、JITレイヤーを排除することで得られたパフォーマンスの利点が相殺される可能性があります。
2. 実行効率
生の速度の観点からは、ElevatorはQEMUのuser-mode JITエミュレーションと比較して、約4.75xの実行速度の向上を示しています。これはQEMUに対する大きな改善ですが、Box64やAppleのRosetta 2のような高度に最適化された翻訳機よりも遅いままです。このパフォーマンスの差は、Elevatorがx86 CPUの状態(EFLAGSなど)の大部分をエミュレートし、複雑な移動命令を個別に計算しなければならないという事実に起因しています。
3. 現在の制限事項
現状では、プロジェクトにはいくつかのアーキテクチャ上の制約があります。
- Single-threaded only: 現在、マルチスレッドをサポートしていません。
- No Exception Handling: スタックの巻き戻し(unwinding)や例外処理のサポートが欠けてています。
- Partial ISA Support: x86_64命令セットの全機能をサポートしていません。
- No Self-Modifying Code: 翻訳が完全に静的かつ決定論的であるため、実行時に自身を書き換えるコードを扱うことができません。
実社会への影響とユースケース
肥大化と制限があるものの、決定論的なアプローチは特定の業界への道を開きます。最も説得力のあるユースケースは、認証済み環境(航空宇宙や医療機器など)です。これらの規制された業界では、JITコンパイルはしばしば禁止されています。なぜなら、実行されるコードは、認証および署名されたコードと全く同一でなければならないからです。
"Static translation that produces a signable binary is a real unlock there, code bloat notwithstanding." — @fizza_pizza
理論的な障壁:ライスの定理
一部の批評家は、静的解析の根本的な問題はライスの定理(Rice's Theorem)によって支配されていると指摘しています。この定理は、プログラムのすべての非自明な意味論的特性は決定不能であると述べています。これは、「敵対的なコード」——翻訳機を欺くために特別に設計されたコード——に対しては、完全な静的翻訳はあらゆるケースにおいて証明可能な不可能であることを意味します。
@dmitrygrが指摘するように、Elevatorは「協調的なバイナリ」(標準的なコンパイラによって生成されたもの)に対しては機能しますが、手書きの、あるいは意図的に難読化されたアセットムブリは、依然として大きな課題として残ります。「Superset CFG」アプローチは、あらゆる可能性をカバーすることでこれを軽減しますが、ISAの複雑さの理論的な限界は残ります。
結論
Elevatorは、空間を確実性との交換で取引する、非常に興味深い実験です。ヒューリスティックを放棄し、あらゆる可能な実行パスの包括的なマッピングに切り替えることで、決定論的なバイナリ翻訳への道を提供します。50倍のバイナリ肥大化は、汎用的な消費者向けソフトウェアには不実用的なものですが、その有用性は、認証と決定論が最優先事項である高信頼性システムにおける、この研究の最も重要な貢献となるでしょう。