WebAssembly Core — バイナリ・WAT・スタックマシン・形式的安全性

WebAssembly (Wasm) のコア仕様の基礎構造。バイナリフォーマット、テキスト表現 (WAT)、スタックマシンアーキテクチャ、および数学的に証明された安全性保証を扱う。

バイナリフォーマット

Wasm の実体は .wasm 拡張子のバイナリファイル。人間には読めない 16 進数の列だが、ブラウザ（やランタイム）にとっては翻訳不要でそのまま実行できるデータ。

マジックナンバーとバージョン

00 61 73 6d  → "\0asm" (マジックナンバー)
01 00 00 00  → バージョン 1

すべての .wasm ファイルはこの 8 バイトで始まる。

セクション構造

バイナリは順序付きのセクション列で構成される:

ID	セクション	内容
1	Type	関数シグネチャ (パラメータ型 → 戻り値型)
2	Import	外部から取り込む関数・メモリ・テーブル・グローバル
3	Function	関数インデックス → Type セクションへの参照
4	Table	間接呼び出し用のテーブル (funcref 等)
5	Memory	線形メモリの宣言 (初期サイズ, 最大サイズ)
6	Global	グローバル変数 (型, ミュータビリティ, 初期値)
7	Export	外部に公開する関数・メモリ等
8	Start	モジュールロード時に自動実行される関数
9	Element	テーブルの初期化データ
10	Code	関数本体 (ローカル変数宣言 + 命令列)
11	Data	線形メモリの初期化データ
12	DataCount	Data セグメント数 (シングルパスバリデーション用)
0	Custom	デバッグ情報 (name セクション等)。バリデーション対象外

具体例: 足し算関数

0061 736d 0100 0000 0107 0160 027f 7f01
7f03 0201 0007 0701 0361 6464 0000 0a09
0107 0020 0020 016a 0b

これは (i32, i32) -> i32 の足し算関数を1つだけ持つ最小モジュール。バイナリの 6a が i32.add 命令に対応する。

WAT (WebAssembly Text Format)

バイナリと 1:1 で相互変換可能 なテキスト表現。S 式 (S-expression) を採用している。

なぜ S 式か

S 式は (演算子引数1 引数2 ...) という単一ルールですべての構造を表現する。

パーサが極めて単純 — 括弧のネストがそのまま AST
ツール (デバッガ、ブラウザの DevTools) がバイナリ ↔ テキストを一瞬で変換できる
Lisp / Scheme の系譜。コードとデータの区別がない均質な構造

具体例: 上記バイナリの WAT 表現

(module
  (type $t0 (func (param i32 i32) (result i32)))
  (func $add (type $t0) (param $p0 i32) (param $p1 i32) (result i32)
    local.get $p0
    local.get $p1
    i32.add)
  (export "add" (func $add)))

i32.add は「スタック上の 2 つの i32 を取り出して加算し、結果を積む」命令。バイナリでは 0x6a の 1 バイト。

S 式 (folded form) とフラット形式

WAT には 2 つの記法がある:

;; folded form (S式のネスト)
(i32.add (local.get $p0) (local.get $p1))

;; flat form (スタック操作を順に書く)
local.get $p0
local.get $p1
i32.add

どちらも同一バイナリにコンパイルされる。folded form は人間の可読性向けのシンタックスシュガー。

スタックマシンアーキテクチャ

Wasm はスタックマシンとして設計されている。レジスタマシン (x86, ARM 等の実 CPU) ではなくスタックマシンを選んだ理由は、Web という特殊な制約に対する合理的な最適解。

なぜスタックマシンか

1. バイナリサイズの最小化

レジスタマシンの命令は「どのレジスタからどのレジスタへ」というオペランド指定が必要:

add r0, r1, r2    ; r0 = r1 + r2 (3つのオペランド指定が必要)

スタックマシンは「上から2つ取って足せ」だけ:

i32.add            ; 1バイトで済む (0x6a)

オペランド指定のバイトが不要なので、命令がコンパクトになる。ネットワーク転送が前提の Web において、バイナリサイズの小ささは直接的にロード速度に影響する。

2. ハードウェア非依存のポータビリティ

レジスタの数や構成は CPU アーキテクチャごとに異なる (x86 は 16 本、ARM は 31 本、RISC-V は 32 本)。スタックマシンは特定のレジスタ構成を前提としないため、どの CPU でも均等にネイティブコードへ変換 (JIT/AOT) できる。

3. バリデーション (安全性検証) の容易さ

スタックマシンは命令列を先頭から順になぞるだけで、各時点のスタック状態（何が何個積まれているか、型は何か）を静的に決定できる。この性質が後述する形式的安全性の基盤。

実行モデル

命令: local.get $p0    スタック: [ ]        → [ 5 ]
命令: local.get $p1    スタック: [ 5 ]      → [ 5, 3 ]
命令: i32.add          スタック: [ 5, 3 ]   → [ 8 ]

ローカル変数 (local) とグローバル変数 (global) はスタック外に存在するが、値の受け渡しはすべてスタック経由。

構造化制御フロー

Wasm には goto がない。制御フローは block / loop / if / br の構造化された命令のみ:

(block $exit
  (br_if $exit (i32.eqz (local.get $n)))  ;; $n == 0 なら block を抜ける
  ;; ... 処理 ...
)

任意のジャンプ先を指定できないため、制御フローグラフが reducible (帰納的) であることが構造的に保証される。これにより:

バリデーションが線形時間で完了する
不正なジャンプ (ROP 攻撃等) が原理的に不可能

形式的安全性保証

Wasm の仕様は操作的意味論 (Operational Semantics) で数学的に定義されており、以下の性質が形式的に証明されている。

型安全性: Progress & Preservation

Progress (進行性): 正しく型付けされた状態の命令は、必ず次の状態へ進める (フリーズしない)。

Preservation (保存性): 命令が 1 ステップ進んでも、スタック上の型の整合性は崩れない。

この 2 つの定理により、「実行中にデータの型が壊れて暴走する」ことが数学的に排除される。ブラウザは .wasm のバリデーション時にこの型チェックを行い、合格したもののみ実行する。

線形メモリの境界安全性

Wasm プログラムがアクセスできるメモリは、1 本の連続バイト配列 (Linear Memory) に限定される:

[ 0, 1, 2, ..., N-1 ]   ← この範囲外へのアクセスは trap (即時停止)

範囲外アクセスは数学的な境界チェックで検知 → trap
ホスト (ブラウザ) のメモリ空間には原理的に到達不可能
バッファオーバーフローによるサンドボックスエスケープを構造的に排除

実装レベルでは Wasmtime のガードページ (前後 2GB) により、明示的なバウンズチェックなしでハードウェア例外として捕捉する最適化が行われる。

構造化制御フローの安全性

goto の不在 → 任意アドレスへのジャンプが不可能
call_indirect は型チェック付き → 型が一致しない関数へのジャンプは trap
制御フローの reducibility が構造的に保証 → バリデーションが決定的かつ線形時間

仕様の数学的基盤

Wasm の仕様書は、小ステップ操作的意味論 (small-step operational semantics) で挙動を定義している。これは:

各命令の効果を数学的な遷移規則 (⟨S; F; instr*⟩ → ⟨S'; F'; instr'*⟩) として厳密に定義
型システムの健全性 (Soundness) を Progress + Preservation として証明
実装者がこの数学的定義に基づいてテストスイートを構築

Google, Apple, Mozilla, Microsoft が共同で策定した理由: 各社のブラウザに「出所不明のバイナリ」を載せる以上、「絶対に安全」と言い切れる数学的保証が必要だった。

形式検証プロジェクト

プロジェクト	内容
WasmCert (Isabelle/HOL)	Wasm 仕様の機械検証。型安全性の証明を定理証明支援系で検証
CT-Wasm	暗号定数時間実行を保証する Wasm 拡張。タイミング攻撃耐性
Cranelift regalloc2	シンボリックチェッカーによるレジスタ割り当ての形式検証

4 つの数値型

Core Wasm が持つ値の型は 4 つだけ:

型	説明
`i32`	32-bit 整数 (符号なし/あり解釈は命令依存)
`i64`	64-bit 整数
`f32`	32-bit IEEE 754 浮動小数点
`f64`	64-bit IEEE 754 浮動小数点

文字列、構造体、配列などの高水準型は存在しない。それらは線形メモリ上のバイト列として表現する。高水準型の相互運用は Component Model の Canonical ABI が担う。

バージョン史

仕様	時期	追加内容
WebAssembly 1.0	2019-12 (W3C Rec)	Core: MVP。4数値型、線形メモリ、テーブル
WebAssembly 2.0	2024-12 (W3C Standard)	mutable globals, multi-value, reference types, bulk memory, SIMD
WebAssembly 3.0	2025-09 (W3C Standard)	tail calls, exception handling, WasmGC, Relaxed SIMD, memory64