WebAssembly Validationアルゴリズムの学び方

どーもちょびえです。余暇でUnity向けにWebAssembly Specification 2.0に準拠したWebAssemblyのRuntimeとWGSL派生言語からWasmへコンパイルする機能を開発しています。

この記事はWebAssembly / Wasm Advent Calendar 2024の4日目で、WebAssembly Validationアルゴリズムの学び方について仕様書をもとに具体的な手法を解説します。

対象の読者

本記事ではWebAssemblyのデザインゴールの確認から、平易に書かれたHTML+JavaScriptで実装された簡易WebAssemblyインタプリタで動作するサンプルを使ってValidationと制御構造の問題に取り組みます。そのため初学者は仕様を理解していないと難解な部分もあります。もし難しいと感じた場合はstep by stepで説明されている「RustでWasm Runtimeを実装する」を読むことを推奨します。

また、WebAssembly Specification 2.0 (Draft)をお供に解説を行います。WebAssemblyの仕様書は世間的に難解であると評価されることがしばしばある仕様書です。とはいえ、RFCを元になにかしらの実装をした経験がある筆者としては、記述は難解な部分もあるけれど親切で明快な仕様書という認識です。

現代では仕様書を読んでよくわからない部分があったとしても、ChatGPTにコピペして解説してください!と質問すれば大抵いい感じに解説してくれるので身構えなくても大丈夫ですよ!


補足

私はWebAssemblyの仕様書pdfをChatGPTにuploadして使っています。2024年12月現在のChatGPTよくある問題としては、何もコンテキストを与えずに質問するとWebAssembly 1.0の仕様で返してくることが多いので注意が必要です。

なお、生成AIを業務で利用する際は所属企業のルールに準じてください。

WebAssemblyが目指すデザインゴール

まずはWebAssemblyのDesign Goalsの確認をします。このゴールを読むことでなぜValidationが必要なのか分かります。

英文だと分かりづらいので日本語に翻訳して引用します。原文をChatGPTにコピー&ペーストして「次の英語を日本語に翻訳してください」でおおよそ正確な日本語訳を出力してくれます。もちろんそのまま鵜呑みにせずに自身の基礎的な英語力でニュアンスがあっているかを再検証する力は必要です。

WebAssemblyの設計目標は以下の通りです:

  • Fast, safe, and portable semantics:

    • Fast: ほぼネイティブコードのパフォーマンスで実行され、現代のすべてのハードウェアに共通する機能を活用します。
    • Safe: コードは検証され、メモリ安全な、サンドボックス化された環境で実行され、データ破損やセキュリティ侵害を防ぎます。
    • Well-defined: 有効なプログラムとその挙動を完全かつ正確に定義し、非公式および公式の両方で容易に理由付けできるようにします。
    • Hardware-independent: すべての現代的なアーキテクチャ、デスクトップやモバイルデバイス、組み込みシステム上でコンパイル可能です。
    • Language-independent: 特定の言語、プログラミングモデル、オブジェクトモデルを優遇しません。
    • Platform-independent: ブラウザに組み込まれたり、スタンドアロンのVMとして実行されたり、他の環境に統合されたりできます。
    • Open: プログラムがシンプルかつ普遍的な方法で環境と相互運用可能です。
  • Efficient and portable representation:

    • Compact: テキストやネイティブコード形式よりも小さく、転送が速いバイナリ形式を持ちます。
    • Modular: プログラムを小さな部分に分割し、別々に転送、キャッシュ、利用することができます。
    • Efficient: Just-in-time (JIT) または Ahead-of-time (AOT) コンパイルのどちらでも、単一の高速なパスでデコード、検証、コンパイルが可能です。
    • Streamable: データ全体を受け取る前に、可能な限り早くデコード、検証、コンパイルを開始できます。
    • Parallelizable: デコード、検証、コンパイルを多数の独立した並列タスクに分割可能です。
    • Portable: 現代のハードウェアで広くサポートされるアーキテクチャ以外の仮定をしません。

WebAssemblyのデザインゴールは、現代のハードウェア上で高速かつ安全に動作し、移植性と空間効率に優れた汎用的なプログラムの実行環境を提供し続けることだと言えます。これらの項目はWebAssemblyの性能や安全性や移植性を支える重要な指針で、実現する為には各モジュールが期待通りに動作することを保証するなにかしらの仕組みが必要となります。

WebAssemblyにおけるValidationの位置づけ

Validationという言葉を聞いても、具体的に何をするのかがすぐにはイメージしづらいかもしれません。WebAssembly関連の用語については、IntroductionのOverviewで説明されており、その中でSemantic PhasesとしてWebAssemblyのフェーズが定義されています。ここでは簡潔に要点をまとめます。

  • Decoding: バイナリ形式のデータを内部的な表現に変換する手続き
  • Validation: デコードされたデータが正しい形式かどうかを確認し、型チェックなどを行う手続き
  • Execution: 実際にモジュールを実行する手続き。インスタンス化と関数呼び出しの2つに分けられる

ざっくりいうとWebAssemblyのValidationはJavaのbytecode verifierのような位置づけとなります。もしくは、WebAPIを扱った経験がある方であればFormのValidationと似たものと考えると分かりやすいかもしれません。こう考えると必要性が判断しやすいと思います。

Runtime実装勢からみるValidation

趣味から始まっているようなRuntime実装勢的にはValidationはどうしても省かれがちです。命令の数だけ検証コードを書いていくため単純に実装量が増えてしまうからです。たしかに省略しようとする気持ちも分かります。しかし、実装することで「よくわからないバグのような挙動との遭遇確率を減らすことが出来る」という超特大のメリットがあります。

私自身、自作言語から出力したWebAssemblyバイナリを自作Runtimeで動かしているときに、しばしばバグのような挙動に悩まされました。その原因を調査してみるとWebAssemblyの仕様に反したバイナリを実行していたことが問題というケースが多くありました。

もしValidationを正確に実装していれば、検証エラーとしてすぐに問題の切り分けができたので時間が節約できたはずです。

Validationの実装方法を考える

WebAssemblyの検証はどうすればいいのか、設計・実装に悩む部分もたしかにあります。そんな私達のためにWebAssembly SpecificationのAppendixに7.3 Validation Algorithmというそのものズバリなセクションがあります。この一連のセクションでは擬似コードを通してValidationアルゴリズムを解説しています。この通りに設計して考えながら実装していけば大まかに仕様に準拠した動作をするRuntimeとValidationの設計ができてしまいます。なんて優しいんだ!英文は毎度のごとくChatGPTに翻訳してもらいつつ読み進めてみてください。

7.3 Validation Algorithmの序文の翻訳文を引用します。

WebAssemblyのバリデーション仕様は純粋に宣言的です。モジュールや命令列が有効であるために満たすべき制約が記述されています。

このセクションでは、コード、つまり命令列を効果的にバリデーションするための、健全かつ完全なアルゴリズムの骨組みを概略的に説明します。(バリデーションの他の側面は実装が比較的容易です。)
実際、このアルゴリズムはバイナリ形式で出現する命令コードの平坦な列に対して表現され、これを単一のパスで処理します。そのため、デコーダに直接統合することが可能です。
アルゴリズムは型付きの擬似コードで表現されており、その意味は自明であることを意図しています。

と説明されています。

自分でRuntimeをどう実現するか考えるのも楽しいのですが、WebAssemblyの制御構造を満たす設計をするのは少し難易度が高めです。例えば、WebAssemblyのジャンプ系では移動先がラベルで指定されており、次に移動すべき場所の絶対的な位置がわかりません。これはセキュアな実行をするためでもあります。またbr命令で制御構造の途中で抜けることもよくあります。当然のように制御構造はネストしていくため、正確に情報をトラッキングしないと正しく動作しません。WebAssemblyの制御構造にまつわる仕様をすべて抑えておかないと大幅に書き直す羽目になります。

Runtimeを作る場合は、最初に明確な基準となる実装を作ってから自分の用途にあった方向に調整していく方が容易に実現しやすいです。せっかく仕様書で設計の骨組みを説明してくれていることですし、この構造を実装のたたき台として使いましょう。

Validationのしくみ

命令列のValidationでは、主に2つの検証を行います。1つ目は、命令と即値を基に入力と出力の型をチェックする作業です。2つ目は、この型情報を活用し、スタック操作を通じて整合性を検証するプロセスです。これらを実現するためには、制御構造の情報を管理するスタックと値を管理するスタックの2種類を使うと比較的簡単に検証と実行ができる実装がつくれます。

このような構造を取ることで複雑な制御構造をもつWebAssemblyのパラメーターやスタックの整合性の検証を行うことができます。7.3.2 Validation of Opcode Sequencesではこの数十行ほどの型情報を使ってValidationをするコンセプトが提示がされています。最終結果となる疑似コードだけをみるとそんなに難しくないのです。WebAssemblyの命令は一部では高レベルな制御構造があるものの、基本的には低レベル操作が多いためシンプルなValidationとなります。

実際に動作するサンプルコード

サンプルコードとしてSukoshi WebAssembly Simulatorというのをざっくりと書きました。

仕様書のAppendix記載の擬似コードからHTMLとJavaScriptに変えて実装したコードです。今回のコードではWebAssemblyモジュールのParseやバイナリフォーマットは省略して、文字列で表現したOpCodeとパラメーター類や即値をまとめた命令セットの配列を検査・処理していく形にしています。

このHTMLとJavaScriptの小さなツールは次のような手順で遊べます。

  • https://chobie.github.io/sukoshi_webassembly/ にブラウザでアクセスする
  • Instruction Setより「5.ローカル変数(検証エラー)」を選ぶ
  • Validationボタンを押してValidation Errorが出ることを確認する
  • Runを押すと未定義動作でエラーとなることを確認する
  • 2行目に["local", [], [], [1, "i32"]],// ローカル変数1 i32を宣言を追加する
  • Validationボタンを押してPassとなることを確認する
  • Runを押すと結果が3となることを確認する

ローカルにGithubリポジトリをcloneして命令を追加したりして改造していくと実装や設計上の疑問点などが浮かぶと思うので良い学習になると思います。なお、このリポジトリはAdvent Calendar用にざっと書いたコードで積極的にメンテはしないつもりです。ご了承ください。

全体で700行程度ではありますが、記事ですべてを解説するには長すぎるのでValidation実装で間違いやすい2つのポイントに絞って解説します。

ポイント1: ControlFrameの設計

現状のWebAssemblyではMulti-Value拡張を標準でサポートしており、結果としてブロックが想定するスタック状態(parameter types/result typesの両方)を宣言できるようになっています。次のWATの例ではblockがi32の値を2つ必要としていることを明示できます。

こうしたblockifなどの複雑なブロック制御を実現するためにControlFrameという情報をStackで管理します。これはRuntime実装上よくある手法です。ControlFrameの管理を正確に行わないと、brend命令の処理時に問題が発生しがちです。

私も自分のRuntimeの初期実装ではControlFrameの一部の情報を省略した結果、ブロックのネストが深くなるとスタックの不整合や誤ったジャンプ先に飛んでしまう不整合が頻発しました。この課題を解決するために、Appendixで説明されているControlFrameに情報を保持する方法を採用しています。

ブロックの動作を正確に再現するには開始時の仮引数と終了時に返す値を保持しておかないと実現が困難です。block, if, loopなどのブロックはすべて共通のend命令で終わることもあり、何も考えずに設計するとendbrが複雑になる要因の一つでもあります。

サンプルコードのexecution部分を見てみるとend部はpop_ctrl関数のみでシンプルです。開始時の仮引数と終了時に返す値を持っているのでほぼ共通処理でendの処理が実現できます。重要なポイントとしてはlabel_types関数で現在のControlFrameがloopの場合かどうかで開始/終了どちらの型を返すか分岐している部分です。

loopのブロックの中でbrをするとloopに戻ります。通常のblock系ではbrをすると対応するendに飛びます。ブロックの種類に応じてstart typesend typesを適切に返せるようにするとシンプルな実装にしやすいです。

ポイント2: unreachableとスキップ処理の実装

初学段階だとunreachableといえばTrapするだけの機能だと思いがちです。実際仕様書の本文にもそうとしか書かれていません。しかし、実装的には条件分岐等で実行しない命令を正確にスキップする為にも到達不能なことを判別し正確にスキップする仕組み(ややこしいですが、これもunreachableと呼称します)が必要です。このような仕組みがないとどこまでスキップすればいいかが区別できません。

おそらく、Validationや制御構造周りの実装で一番困るのは処理を実行せずに正確にスキップする部分だと思います。Validationでは全ての分岐を通過しつつ正しく検証が行えるようにしないといけません。

実装していないとよくわからないと思うので、実例としてifの制御構造からelseまでジャンプしたい、というケースで説明します。

以前のセクションで話題に上げましたが、WebAssemblyではアセンブラでよく使われるアドレス指定のジャンプ機能がありません。どこにジャンプすればいいかはifのタイミングではわからないのです。これは、ifに対応したelseにジャンプしたいという場合にとても困ります。素直にこの挙動を実現するには実際に各種命令や制御構造を一つずつチェックして、現在のifに対応したelseendを正確に判定する必要があります。

簡単と思いきや、実際のWebAssemblyの命令列は平坦な状態です。正確に判定する処理は実装上の難しい部分となります。説明のためにWebAssemblyの疑似命令に対してインデントを入れてみます。

1行目で偽となる条件であれば、13行目のelseまでの命令は無視する必要があります。しかし、2行目のifの段階では対応するelseがどこにあるのか情報を持っていません。そのために、3行目から12行目までの命令では実行せずに制御構造を正しく管理しながら命令を進ませるunreachable相当の仕組みが必要となります。

ControlFrameのunreachbleの情報を元に実操作を省略すればスキップする挙動が実現できます。

今回説明したネストしているifの類似系をSukoshi WebAssemblyのサンプル「6.ネストしたブロック」で試すことができます。6行目を["br", [], [], [0]]に変えると内側のブロックのみ到達不可として扱い、外側のブロックは実行されるようになります。正確に到達不能なことを判別できないと誤った値を返してしまうことがあります。

終わりに

WebAssembly Specification: Appendix 7.3 Validation AlgorithmからみるRuntime設計のポイントということでControlFrameとunreachableに絞って解説をしました。この2つのポイントを抑えておけばWebAssemblyのValidationの実装の基礎が学べます。WebAssemblyは仕様書がしっかりと書かれているので、わからない部分はAIに解説してもらいつつ実装していくと楽しく遊べますよ。

私の自作WebAssembly RuntimeはWASIp1も不完全ながら実装してあり、container2wasmが動作するまでは実装しました。WebAssemblyはお手軽に作れるわりに本格的に動いてしまうので面白いです。(Runtimeの公開は実サービスで実際に使ってから検討しようと思います)

なお、Validationはあくまでも与えられたWebAssemblyモジュールが最低限仕様に準拠してあることを確認する仕組みであり、実際に使われる環境に応じて必要なエッジケースの処理や最適化が別途必要になる場合もあります。線引きが難しい処理になるので他のVMの前例などをしらべると良いと思います。

それでは!