CHC-based Automated Verification of WebAssembly Programs
本論文は、制約付きホーン節を用いてWebAssemblyのサブセットに対する自動静的検証手法を提案するものであり、型ベースのフィルタリングを通じて間接関数呼び出しを効果的に処理し、制御フロー解析の要約を通じて大規模なパニックハンドラを管理する。
原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。 免責事項の全文を読む
インターネットを、あらゆる建物がウェブサイトである、巨大で賑やかな都市だと想像してみてください。長年、これらの建物は、安全ではあるものの建設に時間がかかる、特定の重厚な設計図に基づいて建てられてきました。その後、WebAssemblyと呼ばれる、新しい超効率的な言語が登場しました。これは、ウェブ上のどこへでも飛び、ゲームやツール、アプリをブラウザ内で直接実行するための、重い荷物を運ぶユニバーサルで高速な配送ドローンシステムのようです。これらのドローンは非常に高速で強力であるため、建物に衝突したり、荷物を間違った場所に落としたりしないようにする必要があります。これが「検証（verification）」の仕事です。これは、プログラムを実行する前に、それが安全であることを数学的に証明するという、少し凝った言葉です。
これを行うために、コンピュータ科学者はしばしば「充足可能性ソルバー（Satisfiability Solver）」というツールを使用します。このソルバーを、ルールの一覧を見て、あるシナリオが可能か不可能かを即座に判断できる、超スマートな探偵だと考えてください。もしルールが「ドローンは空にいなければならない」かつ「ドローンは地上にいなければならない」と同時に言っていれば、探偵はその矛盾を見抜き、その計画は安全ではないと判断します。この論文は、その探偵に、WebAssemblyの特定のトリッキーなルール、特に他の関数を間接的に呼び出す部分や、膨大なエラーメッセージを処理する部分を理解させる方法を教えています。
変身する呼び出しの謎
著者である東京大学の八木昭久、坂寄健、小林直樹氏は、トリッキーなパズルに直面しました。WebAssemblyプログラムは、本（関数）が動的に棚から取り出されることもある、巨大な図書室のようなものです。時として、コードは「本Aを開け」と言う代わりに、「棚番号5にある本を開け」と言います。これは**間接関数呼び出し（indirect function call）**と呼ばれます。
問題は、もし棚番号5に何があるかを確認するために図書室中のすべての本を調べようとすると、探偵（ソルバー）が圧倒されてしまうことです。それは、正しい鍵を見つけるために、100万個の鍵穴のあらゆる組み合わせをすべてチェックしようとするようなものです。素朴なアプローチでは、あらゆる可能性を列挙することになりますが、それではコンピュータが妥当な時間内に解決できないほどの膨大な事務作業を生み出してしまいます。
著者たちの解決策は、非常に厳格な司書のように振る舞うことでした。彼らは、WebAssemblyにはルールがあることに気づきました。つまり、探している特定のジャンル（型）と一致する場合にのみ、棚から本を取り出すことができるというルールです。そのため、図書室のすべての本をチェックする代わりに、彼らの手法は、呼び出し箇所で要求されている「ジャンル」を確認し、それに適合しないすべての本を排除します。これにより、候補のリストが劇的に縮小され、探偵の仕事が格段に容易になります。彼らはもう一つのトリックも加えました。もし図書室の棚がロックされており、決して変化しない（読み取り専用）場合、どの本がどこにあるかを事前に計算し、複雑なパズルを単純な「もし〜ならば、〜である」というルールのリストに変えることができます。
巨大なパニックボタン
第二の課題は「パニックハンドラー（panic handler）」でした。プログラムがミスをした際、単に停止するのではなく、エラーが発生した理由を診断チャートやエラーコードと共に、10,000ステップにも及ぶ膨大な説明を展開してから、ようやく諦める様子を想像してみてください。WebAssemblyにおいて、これらのパニックハンドラーは、問題が発生したときにトリガーされる巨大なコードブロックです。
安全性チェッカーにとって、これらの膨大なスピーチは邪魔な存在です。重要なのは、プログラムがいずれ安全に停止すること（「unreachable」命令に到達すること）だけです。エラーメッセージを構築するための長く、回りくどい経路は、プログラムがクラッシュしているという事実自体を変えることはありません。しかし、もし探偵がその10,000ステップのスピーチの全行程を追跡しようとすれば、足を取られてしまいます。
著者らは「要約（summarization）」という手法を導入しました。彼らは、あるコードブロックが単にクラッシュへと繋がっているだけである場合、仲介者を省けることに気づきました。彼らは制御フロー解析を使用して、これらの長く回りくつろいだ経路を特定し、それらを単純なショートカット、「この部屋に入れば、最終的にクラッシュする」というものに置き換えました。これは、ツアーガイドに対して、「ロビーに関する50分の歴史講義は飛ばして、出口が塞がれているということだけ伝えてください」と言うようなものです。これにより、検証をエラーメッセージのノイズに迷い込むことなく、重要な安全性問題に集中させることができます。
結果：進行中の作業
アイデアをテストするために、チームはWASMVERIFIERというプロトタイプツールを構築しました。彼らはRustやCで書かれたものを含む90種類のプログラムをこれに投入し、それらが安全であることを証明するよう求めました。
結果は有望でしたが、完璧ではありませんでした。2つの異なる探偵ソルバー（Z3 SpacerとEldarica）を使用することで、このツールは約54から56のプログラムの安全性を検証、あるいは否定することに成功しました。しかし、約20から22のプログラムについては、実行時間の制限（タイムアウト）やメモリ不足により壁に突き当たりました。また、約11から12のケースでは、実際には安全であるにもかかわらず、安全ではないと判断する「誤検知（false alarm）」が発生しました。著者らは、これらの誤検知について、サポートされていない命令を「クラッシュ」のプレースホルダーに置き換える必要があったため、安全性チェックが慎重になりすぎたことが原因であると説明しています。
この論文は、このアプローチが完全自動化された安全性チェックへの強力な一歩ではあるものの、まだ魔法の杖ではないことを示唆しています。著者らは、特にビット（bit-vectors）に関する複雑な数学の扱い方や、まだ完全には理解できていない命令への対処法において、手法がまだ洗練されている段階であると述べています。彼らは、この手法は健全（sound）かつ完全（complete）であると考えていますが、そのための形式的な数学的証明はまだ書き終えておらず、それを将来の課題として残しています。
要約すると、この論文は、間接呼び出しをフィルタリングする方法を賢くし、エラーハンドリングの乱雑な部分を要約することで、WebAssemblyの自動安全性チェックをより実用的なものにできることを示しています。これは強固な基礎ですが、探偵がすべての事件を解決するには、まださらなる訓練が必要です。
自分の分野の論文に埋もれていませんか？
研究キーワードに一致する最新の論文のダイジェストを毎日受け取りましょう——技術要約付き、あなたの言語で。