はじめに

最終更新: 2026-05-24

このドキュメントは、STARK Ballot Simulator の公開向けガイドです。

目的

• システムの全体像を短時間で把握できるようにする
• 暗号プロトコルと検証パイプラインの設計根拠を説明する
• 検証手順を再現できる情報を提供する

公開状態

本書はライブデモと公開用ソース snapshot の読者に向けたドキュメントです。公開 repository snapshot は hwatanabe-jp/stark-ballot-simulator-public で確認できます。ソースコードへのアクセスが必要な再現手順は、対象リリースの公開 repository snapshot と照合して実行してください。bundle.zip だけで実行できる確認範囲は 第三者検証ガイド にまとめています。

想定読者

• 暗号検証・監査に関心のある技術者
• 本アプリケーションに興味のある技術者

本書の用語表記

語彙の揺れを避けるため、本書では次のように表記を統一しています。詳細な定義は 用語集 を参照してください。

• 日本語に統一する語: コミットメント（文脈に応じて「投票コミットメント」「入力コミットメント」を区別）、包含証明、整合性証明、投票レシート、掲示板、集計確定
• 英語のまま使う語: STARK、zkVM、Image ID、RFC 6962、capability、bundle.zip、fail-closed、journal
• バンドル関連の正規形: 配布されるファイル本体は `bundle.zip`（コードフォント）、配布対象としての論理名は「配布対象アーカイブ」、上位概念（非公開アーティファクトを含む全体）は「証明バンドル」を使い分けます。階層関係は バンドル構造 を参照。

本書の読み方

標準ルート

1. まず 全体像 でシステムの概要を掴む
2. アーキテクチャ語彙マップ（試験的） で UI、API、掲示板、zkVM、検証、バンドル境界の関係を 1 枚で確認する（試験的な語彙地図）
3. 暗号プロトコル でコミットメント・Merkle ツリー等の基盤を理解する
4. zkVM 設計 でゲストプログラムと証明生成の仕組みを学ぶ
5. 検証パイプライン で 4 段階検証モデルの全体を把握する
6. 改ざんシナリオ で教育的シミュレーションの動作を確認する
7. 品質保証と形式手法 でテスト・PBT・Lean による品質境界を確認する
8. AWS アーキテクチャ で非同期証明インフラを理解する
9. API リファレンス でエンドポイント仕様を参照する
10. 実際に検証する場合は 第三者検証ガイド で bundle.zip を使ったローカル検証手順を実行する
11. 設計上の判断については 設計判断 を参照する
12. 設計根拠の一次資料は 参考文献 を参照する

読者別ルート

監査者向け

bundle.zip を検証ページから取得し、独立にローカル監査したい読者向け。

1. 全体像 で 4 段階モデルとバンドル階層を把握する
2. 検証パイプライン で /verify の最終判定ロジックを理解する
3. チェック一覧 で各チェック ID と判定条件を確認する
4. 第三者検証ガイド で bundle.zip のローカル監査手順を実行する
5. 用語集 で「検証」「監査」「fail-closed」などの用語を確認する
6. 品質保証と形式手法 で、テストと形式化がどの境界を守っているかを確認する

飛ばしてよい: 暗号プロトコル の数式詳細、AWS アーキテクチャ のインフラ詳細

実装者向け

クライアント/サーバー/zkVM のいずれかの実装を変更・追従したい読者向け。

1. 全体像 でシステム境界を確認する
2. アーキテクチャ語彙マップ（試験的） で境界づけられた語彙と主要データフローを共有する（試験的な語彙地図）
3. 暗号プロトコル でコミットメント・Merkle・入力コミットメントの正準形を把握する
4. zkVM 設計 でゲスト/ホストの責務分担と Image ID 管理を理解する
5. 検証パイプライン でチェック評価とゲーティングを把握する
6. 品質保証と形式手法 で、テスト・PBT・Lean のレイヤー分担を確認する
7. API リファレンス でエンドポイント仕様と session-scoped 認可を確認する

飛ばしてよい: 第三者検証ガイド（実装変更後の動作確認には 改ざんシナリオ を使う方が早い）

運用者向け

AWS インフラ・非同期プローバー・デプロイを担当する読者向け。

1. 全体像 で sync / async finalize の違いを確認する
2. AWS アーキテクチャ で現行構成、環境分離、Amplify / Terraform の連携点を把握する
3. 非同期プローバー で SQS / Step Functions / ECS の責務を理解する
4. イメージ署名 と Image ID で署名検証と Image ID 解決の連動を確認する
5. バンドル構造 で公開/非公開アーティファクトの境界を把握する
6. API リファレンス で本番運用で監視すべきエンドポイントを確認する

飛ばしてよい: 暗号プロトコル の数式、改ざんシナリオ の教育的デモ詳細

全体像

STARK Ballot Simulator は、投票の完全性を段階的に検証するための PoC です。

flowchart LR
  A[Cast-as-Intended] --> B[Recorded-as-Cast]
  B --> C[Counted-as-Recorded]
  C --> D[STARK Verification]

データフロー概観

sequenceDiagram
  participant V as 投票者
  participant S as サーバー
  participant B as 掲示板
  participant Z as zkVM
  participant VS as 検証サービス

  V->>S: 投票意図（選択肢・乱数）+ コミットメント
  S->>B: 掲示板に追記
  S-->>V: 投票レシート
  Note over S: ボット投票を自動追加
  S->>Z: 全投票 + Merkle パス
  Z-->>S: STARK レシート + ジャーナル
  S->>VS: STARK レシート検証
  VS-->>S: 検証レポート
  S-->>V: 検証結果

コアコンセプト

• 投票コミットメントと投票レシートにより Cast-as-Intended を検証
• RFC 6962 / CT スタイルの掲示板で Recorded-as-Cast を検証
• zkVM ジャーナル、入力整合、ビットマップ証明により Counted-as-Recorded を検証
• RISC Zero レシート検証で STARK 実行の正当性を検証
• AWS クラウド費用の目標月額を 1 USD（デプロイなし、アプリのアクセスなし時）

バンドル用語の階層

検証で扱うアーティファクト群は階層的な 3 つの用語で呼び分けます。

証明バンドル ⊃ 配布対象アーカイブ ⊃ bundle.zip（ファイル）

詳細: バンドル構造、定義: 用語集 > 証明バンドル。

プロジェクト規模

概算（2026-05-23 時点、tracked files ベース、生成物を除く、千行単位に丸め）。

各章への案内

アーキテクチャ語彙マップ（試験的）

注意: このページは試験的な語彙整理であり、overview.md のような確定仕様ではありません。 Bounded context の切り方や Aggregate / Value Object の対応付けは PoC 進行に合わせて変更される可能性があります。 実装上の真実は各章（protocol/, zkvm/, verification/）および現行コードを優先してください。

この図は、STARK Ballot Simulator の bounded context を 1 枚の context map にまとめた語彙地図です。中心には「必要な証拠が揃い、required checks が成功するまで Verified と表示しない」という中核の約束があります。

%%{init: {"flowchart": {"nodeSpacing": 36, "rankSpacing": 58, "curve": "basis"}}}%%
flowchart TB
  Promise["中核の約束<br/>必要な証拠が揃い、required checks が成功するまで<br/>Verified と表示しない"]

  subgraph VOTE["Bounded Context: 投票セッション"]
    direction TB
    VoteLang["Ubiquitous Language<br/>Election Session / Voter / Vote Choice<br/>Opening / Commitment / Vote Receipt"]
    VoteAggregate["Aggregate Root<br/>Session<br/>(electionId, electionConfigHash, logId,<br/>phase, contractGeneration)"]
    VoteVO["Value Objects<br/>Capability / Opening<br/>Commitment / Vote Receipt"]
    VoteEvent["Conceptual Domain Events<br/>SessionOpened / VoteCast / SessionFinalized"]
    VoteInvariant["Invariants<br/>opening から commitment が再計算可能<br/>private opening は公開 bundle に含めない"]

    VoteLang --> VoteAggregate
    VoteAggregate --> VoteVO
    VoteVO --> VoteEvent
    VoteEvent --> VoteInvariant
  end

  subgraph BOARD["Bounded Context: 公開掲示板"]
    direction TB
    BoardLang["Ubiquitous Language<br/>Append-only Log / Leaf / Tree Size<br/>Root / Inclusion Proof / Consistency Proof / STH"]
    BoardAggregate["Aggregate Root<br/>BulletinLog<br/>(logId, treeSize, root)"]
    BoardVO["Value Objects<br/>VoteEntry / InclusionProof<br/>ConsistencyProof / STH Digest"]
    BoardEvent["Conceptual Domain Events<br/>EntryAppended / LogClosed"]
    BoardInvariant["Invariants<br/>Log は append-only<br/>検証成功条件として<br/>rootAtCast → finalRoot の consistency proof が必須<br/>（欠落時は fail-closed）"]

    BoardLang --> BoardAggregate
    BoardAggregate --> BoardVO
    BoardVO --> BoardEvent
    BoardEvent --> BoardInvariant
  end

  subgraph PROOF["Bounded Context: 集計証明"]
    direction TB
    ProofLang["Ubiquitous Language<br/>ZkVM Input / Witness / Journal<br/>Receipt / Image ID / Input Commitment / Method Version"]
    ProofAggregate["Aggregate Root<br/>ProofRun<br/>(methodVersion, imageId)"]
    ProofVO["Value Objects<br/>ZkVMInput / Journal<br/>RISC Zero Receipt / Input Commitment"]
    ProofEvent["Conceptual Domain Events<br/>ProofRequested / ProofGenerated"]
    ProofInvariant["Invariants<br/>Receipt は expected Image ID で verify 成功<br/>RISC0_DEV_MODE=1 は production proof ではない"]

    ProofLang --> ProofAggregate
    ProofAggregate --> ProofVO
    ProofVO --> ProofEvent
    ProofEvent --> ProofInvariant
  end

  subgraph AUDIT["Bounded Context: 検証監査"]
    direction TB
    AuditLang["Ubiquitous Language<br/>Evidence / Check / Stage / Report<br/>Bundle / Verdict / Fail-closed"]
    AuditAggregate["Aggregate Root<br/>VerificationRun<br/>(sessionId, executionId)"]
    AuditVO["Value Objects<br/>Public Bundle / Verification Report<br/>Check / Stage / Verdict"]
    AuditEvent["Conceptual Domain Events<br/>VerificationCompleted"]
    AuditInvariant["Invariants<br/>Verified only when effective required checks all succeed,<br/>no unresolved required checks remain (not_run / pending / running),<br/>configured STH consensus is not violated,<br/>and no fail-closed exclusion signal remains<br/>private artifacts は公開 bundle に入らない"]

    AuditLang --> AuditAggregate
    AuditAggregate --> AuditVO
    AuditVO --> AuditEvent
    AuditEvent --> AuditInvariant
  end

  subgraph POLICY["Domain Policy: 教育的シナリオ"]
    direction TB
    Scenario["Scenario<br/>S0 normal<br/>S1/S3 exclusion<br/>S2/S4 claimed tally tamper<br/>S5 combined educational case"]
    ClaimedTally["Claimed Tally<br/>UI に見せる主張値"]
    VerifiedTally["Verified Tally<br/>journal が束縛する集計値"]
    Scenario --> ClaimedTally
    Scenario --> VerifiedTally
  end

  subgraph ADAPTERS["Adapters / delivery mechanisms"]
    direction TB
    Browser["Browser UI<br/>/ /vote /aggregate /result /verify"]
    SharedApi["Shared API<br/>Next route wrappers と Hono route registry"]
    VoteStore["VoteStore implementations<br/>Mock / FileMock / Amplify"]
    SyncProver["Sync finalize<br/>local zkVM executor + ProofBundleService"]
    AsyncAws["Async AWS<br/>SQS / Step Functions / ECS / S3 / callback runners"]
    ReportDelivery["Bundle and report delivery<br/>public bundle.zip<br/>protected verification.json"]

    Browser --> SharedApi
    SharedApi --> VoteStore
    SharedApi --> SyncProver
    SharedApi --> AsyncAws
    SharedApi --> ReportDelivery
  end

  Promise --> VOTE
  Promise --> BOARD
  Promise --> PROOF
  Promise --> AUDIT

  VOTE -- "Published Language<br/>commitment + vote receipt" --> BOARD
  VOTE -- "Private witness<br/>opening data for proving" --> PROOF
  BOARD -- "Published Language<br/>logId + timestamp + closed root + inclusion paths" --> PROOF
  PROOF -- "Published Language<br/>journal + RISC Zero receipt + inputCommitment" --> AUDIT
  VOTE -- "Private knowledge<br/>opening recomputes commitment" --> AUDIT
  BOARD -- "Evidence<br/>inclusion + consistency + optional STH" --> AUDIT
  POLICY -- "Demo policy<br/>exclusion scenarios affect proof input" --> PROOF
  POLICY -- "Mismatch becomes audit evidence" --> AUDIT

  ADAPTERS -. "drives use cases" .-> VOTE
  ADAPTERS -. "persists log and session state" .-> BOARD
  ADAPTERS -. "runs or queues prover work" .-> PROOF
  ADAPTERS -. "serves bundles and reports" .-> AUDIT

  AUDIT --> Promise

DDD としての読み方

• Bounded Context は 4 つ（投票セッション / 公開掲示板 / 集計証明 / 検証監査）。
• 各 context の内側は Ubiquitous Language を頭に、Aggregate Root / Value Objects / Conceptual Domain Events / Invariants の 4 段で表す。
• Published Language ラベル付きの太矢印は公開契約を示し、同じ単語でも context が違えば意味を分ける（例：「投票レシート」は VOTE の語彙、「RISC Zero receipt」は PROOF の語彙）。
• 教育的シナリオ S0–S5 は bounded context ではなく Domain Policy として外側に置き、claimed tally と verified tally の不一致を AUDIT へ伝える。
• UI / API / Store / AWS は別ドメインの言語ではなくアダプタなので、Adapters / delivery mechanisms として図の下部に分離する。

Verified を表示してよい厳密な条件は ゲーティングロジック を参照してください。

暗号プロトコル

投票の検証可能性を支える暗号プリミティブをまとめる部です。

公開データに対する投票の秘匿性（hiding）と束縛性（binding）を支えるコミットメントスキームから、RFC 6962 に基づく CT スタイルの Merkle ツリー、zkVM 入力の正準エンコーディングまで、検証可能性の基盤となる暗号構成要素を網羅します。

本書で「コミットメント」は 投票コミットメント（個々の投票の束縛）と 入力コミットメント（zkVM 公開入力全体の束縛）の 2 種を指します。両者は対象とドメイン分離タグが異なるため、それぞれ独立した章を設けています。

この部に含まれる章

• コミットメントスキーム — 投票コミットメントの構成と安全性
• CT Merkle ツリー — CT スタイルの追記専用掲示板
• 入力コミットメント — zkVM 公開入力に対するコミットメントの正準エンコーディング
• STH ダイジェスト — 分割ビュー緩和のためのツリーヘッドダイジェスト
• ビットマップ Merkle — 投票カウント証明のためのビットマップツリー

想定読者と前提

• 想定読者: 暗号プリミティブの仕様を実装・監査する技術者
• 前提: SHA-256 ハッシュ計算と Merkle ツリーの基本概念を把握していること

本章で扱わないもの

• SHA-256 や Pedersen コミットメントなど暗号プリミティブの数学的安全性証明
• RFC 6962 / CT エコシステムの運用詳細（証明書ログ、Monitor 役割など）
• 暗号ライブラリ実装の詳細（定数時間実装、サイドチャネル対策）

関連する章

• zkVM 設計 — このプロトコルが zkVM 入力としてどう使われるか
• 検証パイプライン — このプロトコルに対応する検証チェック
• 用語集 — 暗号プリミティブの用語定義

コミットメントスキーム

投票者の選択を秘匿しつつ後から変更できないようにするコミットメントスキームを扱う章です。

SHA-256 ベースのコミットメントにより、投票内容の hiding（秘匿性）と binding（束縛性）を実現します。ドメイン分離タグにより、他プロトコルとのコミットメント衝突を防止します。

概要

投票コミットメントは、投票者が選んだ選択肢を公開データからは隠したまま、その選択に束縛されることを可能にする暗号プリミティブです。掲示板に記録されるのはコミットメント値のみで、選択肢と乱数（opening）は公開配布物（掲示板や bundle.zip 内の public-input.json など）には現れません。投票者は Cast-as-Intended 検証のために opening をローカルに保持します。

flowchart LR
  subgraph 入力
    E[選挙 ID<br/>16 バイト UUID]
    C[選択肢<br/>1 バイト]
    R[乱数<br/>32 バイト]
  end
  E --> H[SHA-256]
  C --> H
  R --> H
  T["ドメインタグ<br/>&quot;stark-ballot:commit|v1.0&quot;"] --> H
  H --> CM[コミットメント<br/>32 バイト]

コミットメントの正準フォーマット

コミットメント値は、以下の入力を連結し SHA-256 で圧縮して生成されます。

commitment = SHA-256(
    domain_tag  ||   ← "stark-ballot:commit|v1.0" (24 バイト, UTF-8)
    election_id ||   ← UUID v4 のバイナリ表現 (16 バイト)
    choice      ||   ← 選択肢の値 (1 バイト, 0〜4)
    random           ← 一様乱数 (32 バイト)
)

各フィールドの仕様

SHA-256 への入力は合計 73 バイト、出力は 32 バイト（16 進数表記で 64 文字、0x プレフィックス付きでは 66 文字）です。

ドメイン分離

ドメインタグ "stark-ballot:commit|v1.0" は、このコミットメントが他のプロトコルで使用されるハッシュ値と偶発的に衝突することを防ぐための仕組みです。

本システムの主要なハッシュ用途では、用途ごとに以下のようなドメインタグまたは構造的プレフィックスを使い、ハッシュ入力の意味を分離します。

STH ダイジェストは専用のドメインタグを持たず、ログ ID を含む正準フォーマットで束縛されます（STH ダイジェスト を参照）。

安全性

Hiding（秘匿性）

乱数フィールドが 32 バイト（256 ビット）のエントロピーを持つため、公開されたコミットメント値から選択肢を推測することは計算量的に不可能です。

前提条件:

• 乱数は暗号学的に安全な乱数生成器（CSPRNG）から生成される
• 同じ乱数は決して再利用しない（再利用すると、同じ選択肢で同じコミットメント値が現れて情報が漏洩する）

PoC の制約: 本 PoC は operator に対する完全な秘匿性を目的としていません。投票 API に送信された opening（選択肢と乱数）はサーバー側ストアに保持されうるため、ここでいう hiding は公開観測者と公開配布物に対する性質を指します。

Binding（束縛性）

SHA-256 の原像耐性（preimage resistance）と第二原像耐性（second-preimage resistance）により、一度コミットした値と異なる選択肢に対して同じコミットメント値を生成することは計算量的に不可能です。

つまり、投票者はコミットメント公開後に「別の選択肢に投票した」と主張を変えることができません。

TypeScript と Rust の実装同期

コミットメントは TypeScript（クライアント・サーバー）と Rust 実装（zkVM guest/host から共有される zkvm/contract-core）の双方で計算されます。この 2 系統の実装は、バイトレベルで完全に同一の出力を生成する必要があります。

同期が必要な要素:

• ドメインタグの文字列とエンコーディング（UTF-8）
• UUID からバイト列への変換規則（ハイフン除去 → 16 進数デコード）
• 選択肢の整数エンコーディング（1 バイト、符号なし）
• 乱数の 16 進数デコード規則

ドメインタグやエンコーディング規則を変更する場合は、TypeScript と Rust の両実装を同時に更新する必要があります。どちらか一方のみの変更は、コミットメント照合の失敗を引き起こします。

検証パイプラインにおける役割

コミットメントは、4 段階検証モデルの最初の 3 段階で中心的な役割を果たします。

注意: Cast-as-Intended と Counted-as-Recorded は同じコミットメント計算式を使いますが、opening の出所が異なります（投票者ローカル / prover に渡された値）。

Recorded-as-Cast は投票時点（cast-time）のツリー状態に対する包含証明を使い、レシートの bulletinRootAtCast と整合させます。rootAtCast の保存と再導出の詳細は CT Merkle ツリー を参照してください。

各チェックの判定ロジックは チェック一覧 > Cast-as-Intended を参照してください。

sequenceDiagram
    participant V as 投票者
    participant S as サーバー
    participant B as 掲示板
    participant Z as zkVM

    V->>V: (選択肢, 乱数) を選び<br/>コミットメントを計算
    V->>S: コミットメント, 選択肢, 乱数を送信
    S->>S: opening から<br/>コミットメントを再計算して照合
    S->>B: コミットメントを掲示板に追記
    S-->>V: 投票レシート（インデックス,<br/>bulletinRootAtCast）
    Note over V: ローカルに (選択肢, 乱数) を保存
    Note over Z: ゲストプログラムが<br/>コミットメントを再計算し<br/>掲示板の値と照合

CT Merkle ツリー

RFC 6962 を参照した追記専用 Merkle ツリーで、掲示板の透明性をどう作るかを扱う章です。

リーフハッシュ（0x00 プレフィックス）とノードハッシュ（0x01 プレフィックス）の区別により、second-preimage 攻撃を防止します。包含証明と整合性証明により、投票の記録と掲示板の追記専用性を検証可能にします。

なぜ RFC 6962 CT スタイルか

• 整合性証明で追記専用性を示せるため、Recorded-as-Cast に必要な「後から削除・改変されていない」保証を与えられる。
• 包含証明と整合性証明の両方を同一モデルで扱える。
• STH ダイジェストと組み合わせてスプリットビュー攻撃の検出力を上げられる。

概要

本システムの掲示板（Bulletin Board）は、Certificate Transparency (CT) で実績のある追記専用ログの設計を投票に応用しています。各投票コミットメントは Merkle ツリーのリーフとして追記され、一度記録されたエントリは削除も改変もできません。

graph TD
  subgraph "8 リーフのツリー（N=8）"
    R["ルート<br/>SHA-256(0x01 || L || R)"]
    N1["ノード"]
    N2["ノード"]
    N3["ノード"]
    N4["ノード"]
    N5["ノード"]
    N6["ノード"]
    L0["リーフ 0"]
    L1["リーフ 1"]
    L2["リーフ 2"]
    L3["リーフ 3"]
    L4["リーフ 4"]
    L5["リーフ 5"]
    L6["リーフ 6"]
    L7["リーフ 7"]

    R --> N1
    R --> N2
    N1 --> N3
    N1 --> N4
    N2 --> N5
    N2 --> N6
    N3 --> L0
    N3 --> L1
    N4 --> L2
    N4 --> L3
    N5 --> L4
    N5 --> L5
    N6 --> L6
    N6 --> L7
  end

RFC 6962 参照ハッシュ規則

RFC 6962 Section 2 に従い、リーフノードと内部ノードに異なるドメイン分離プレフィックスを適用します。

リーフハッシュ

LeafHash = SHA-256(0x00 || "stark-ballot:leaf|v1" || leaf_data)

内部ノードハッシュ

NodeHash = SHA-256(0x01 || left_hash || right_hash)

ドメイン分離の安全性

0x00（リーフ）と 0x01（内部ノード）のプレフィックス区別は、second-preimage 攻撃を防止するために不可欠です。この区別がなければ、攻撃者はリーフノードを内部ノードとして解釈させる（またはその逆の）偽造データを構築できる可能性があります。

使用タグ "stark-ballot:leaf|v1" は、他システムのリーフハッシュとの偶発的な衝突を防止する追加の防御層です。

Merkle Tree Hash（MTH）アルゴリズム

RFC 6962 で定義される MTH アルゴリズムは、任意のサイズのデータセットからルートハッシュを計算します。

アルゴリズムの定義

1. 空のツリー: MTH({}) = SHA-256() （空入力のハッシュ）
2. 単一リーフ: MTH({d₀}) = LeafHash(d₀)
3. 複数リーフ: サイズ n のツリーに対し、k を n 未満の最大の 2 のべき乗とする

MTH({d₀, ..., dₙ₋₁}) = SHA-256(0x01 || MTH({d₀, ..., dₖ₋₁}) || MTH({dₖ, ..., dₙ₋₁}))

非 2 のべき乗サイズへの対応

ツリーサイズが 2 のべき乗でない場合（例: 5, 6, 7 リーフ）、MTH アルゴリズムは「n 未満の最大の 2 のべき乗」で分割を行います。これにより、左部分木は常に完全二分木（2 のべき乗サイズ）となり、右部分木にのみ不完全さが集中します。

graph TD
  subgraph "5 リーフのツリー（k=4 で分割）"
    Root["ルート"]
    Left["左部分木<br/>MTH(d₀..d₃)<br/>完全二分木"]
    Right["右部分木<br/>MTH(d₄)<br/>単一リーフ"]
    Root --> Left
    Root --> Right
  end

デフォルトのデモ構成では 64 票（2⁶）を扱うため、最終的なツリーは完全二分木になります。ただし投票の追加途中や小規模な検証ケースでは非 2 のべき乗サイズが現れるため、実装は任意の treeSize に対する一般対応を備えます。

掲示板のリーフデータ形式

掲示板に追記される各投票のリーフデータは、コミットメントの正規化された 16 進数表現（0x なし、小文字、64 文字）を 32 バイトにデコードした生バイト列です。

leaf_data = hex_decode(normalized_commitment_hex) (32 バイト)

掲示板は以下の不変条件を維持します:

• 単調増加インデックス: 各投票に 0 から始まる連番が割り当てられる
• 重複排除: 同一の投票 ID やコミットメントの二重追記を拒否する
• ルート履歴: 各追記時点のルートハッシュをタイムスタンプとともに保存する

包含証明（Inclusion Proof）

包含証明は、特定のコミットメントがツリーの特定位置に含まれていることを、ルートハッシュに対して暗号学的に証明するものです。

構造

包含証明は以下の要素で構成されます:

実装での名称

本章では RFC 6962 の抽象名を使いますが、API では異なるフィールド名で返します。

/api/verify の userVote.proof や /api/bulletin/:voteId/proof がこの構造に対応します。

PATH アルゴリズム

RFC 6962 の PATH 関数に従い、監査パスを再帰的に生成します。

1. ツリーをサイズ k（n 未満の最大の 2 のべき乗）で左右に分割
2. 対象リーフが左部分木にある場合（index < k）:
   • 左部分木の PATH を再帰計算
   • 右部分木のハッシュを監査パスに追加
3. 対象リーフが右部分木にある場合（index >= k）:
   • 右部分木の PATH を再帰計算（インデックスを index - k に調整）
   • 左部分木のハッシュを監査パスに追加

検証手順

検証者は以下の手順で包含を確認します:

1. コミットメントのリーフハッシュを計算: LeafHash(commitment)
2. PATH アルゴリズムと同じ木構造に従い、監査パスのノードを順に結合
3. 計算されたルートが期待するルートハッシュと一致するか確認

Recorded-as-Cast では、包含証明に加えて以下の cast-time 一貫性も確認します:

• leafIndex がレシートの bulletinIndex と一致すること
• treeSize が bulletinIndex + 1 と一致すること（投票時点のツリーサイズ）

監査パスのサイズは O(log n) であり、64 票のツリーでは最大 6 ノードです。

graph TD
  subgraph "インデックス 5 の包含証明"
    Root["ルート ✓"]
    N1["H(N3, N4)"]
    N2["H(N5, N6) ← 計算対象"]
    N3["H(L0,L1)<br/>監査パス"]
    N4["H(L2,L3)<br/>監査パス"]
    N5["H(L4,L5) ← 計算対象"]
    N6["H(L6,L7)<br/>監査パス"]
    L4["L4<br/>監査パス"]
    L5["L5 ← 対象リーフ"]

    Root --> N1
    Root --> N2
    N1 --> N3
    N1 --> N4
    N2 --> N5
    N2 --> N6
    N5 --> L4
    N5 --> L5
  end

  style L5 fill:#4CAF50,color:#fff
  style N3 fill:#2196F3,color:#fff
  style N4 fill:#2196F3,color:#fff
  style N6 fill:#2196F3,color:#fff
  style L4 fill:#2196F3,color:#fff

整合性証明（Consistency Proof）

整合性証明は、古いツリー状態（サイズ m）が新しいツリー状態（サイズ n）の前方互換的なプレフィックスであること、つまり追記専用性を暗号学的に証明するものです。

構造

補足: /api/bulletin/consistency-proof は proofNodes に加えて rootAtOldSize と rootAtNewSize も返します。/verify の recorded_consistency_proof 判定は、主に bulletin provider から取得した old/new root と整合性証明を検証する経路で、HTTP エンドポイントは consistency-verifier.ts の補助系で利用されます。判定では old root をレシートの bulletinRootAtCast、new root を最終 bulletinRoot と照合します。

SUBPROOF アルゴリズム

RFC 6962 の SUBPROOF 関数に基づき、整合性証明を再帰的に生成します。

1. m = n かつ古いツリーが完全部分木: 空の証明を返す
2. m = n かつ完全部分木でない: 部分木のルートハッシュを返す
3. k を n 未満の最大の 2 のべき乗とし:
   • m <= k の場合: 左部分木の SUBPROOF + 右部分木のハッシュ
   • m > k の場合: 右部分木の SUBPROOF + 左部分木のハッシュ

検証の意味

整合性証明の検証が成功することは、以下を意味します:

• 古いツリーのすべてのリーフが、新しいツリーにも同じ位置・同じ値で存在する
• 新しいツリーは古いツリーの末尾にリーフを追加しただけで構成されている
• 古いツリーのルートハッシュと新しいツリーのルートハッシュの両方が、提供された証明ノードから独立に再構成できる

これにより、サーバーが過去に記録した投票を密かに削除したり順序を変更したりする攻撃を検出できます。

検証パイプラインにおける役割

CT Merkle ツリーは、4 段階検証モデルの主に 2 段階で使用されます。

Recorded-as-Cast では recorded_inclusion_proof と recorded_consistency_proof が表の役割を担当し、他の派生チェックもこれらの結果に基づきます。ハッシュ規則の不一致は zkVM ゲスト内での検証失敗として即座に検出されます。

各チェックの判定ロジックは チェック一覧 > Recorded-as-Cast を参照してください。

RFC 6962 参照範囲

本システムはリーフハッシュに使用タグ "stark-ballot:leaf|v1" を追加しています。これは RFC 6962 の拡張であり、他システムとのリーフハッシュ衝突を防止するための措置です。標準の CT 実装との直接的な相互運用は意図していません。

入力コミットメント

zkVM 入力のうち公開検証に使うフィールドを正準エンコーディングで束縛し、ジャーナルから再計算できる入力コミットメントを定義する章です。

入力コミットメントにより、「証明されたデータセット」と「主張されたデータセット」の一致を検証可能にします。バイトレベルの正準化により、TypeScript と Rust の間で決定的な一致を保証します。

概要

入力コミットメントは、公開可能な検証フィールドにドメインタグとバージョンを加えて正準連結し、SHA-256 で集約したハッシュ値です。対象フィールドの一覧と並び順はバイトレイアウトとフィールド一覧を参照してください。

このハッシュ値は zkVM のジャーナル（公開出力）にコミットされるため、第三者はジャーナルに記録された入力コミットメントと、public-input.json などの公開可能な検証データから再計算した値を照合することで、zkVM が実際にどのデータセットを処理したかを独立に検証できます。

flowchart TB
  IN["入力データ<br/>electionId / bulletinRoot / treeSize<br/>/ totalExpected / votes (index 昇順)"]
  SPEC["固定値<br/>domainTag: stark-ballot:input|v1.0<br/>version: 10"]

  IN --> ENC[正準エンコーディング]
  SPEC --> ENC
  ENC --> H[SHA-256]
  H --> IC[入力コミットメント<br/>32 バイト]
  IC --> CMP["第三者照合<br/>再計算値 = journal.inputCommitment"]

入力コミットメントが解決する問題

zkVM の STARK 証明は「ゲストプログラムが正しく実行された」ことを証明しますが、「どの入力に対して実行されたか」は証明のスコープ外です。入力コミットメントがなければ、悪意あるサーバーは以下の攻撃が可能になります:

1. 投票を除外した入力で zkVM を実行し、有効な STARK 証明を取得する
2. 公開用の入力データには除外されていない投票を含めて提示する
3. 第三者は STARK 証明が有効であることを確認できるが、実際に処理された入力は異なる

入力コミットメントをジャーナルに含めることで、第三者は「公開データから再計算した入力コミットメント」と「ジャーナルに記録された入力コミットメント」を照合し、不一致を検出できます。

正準エンコーディング

入力コミットメントの計算には、すべてのフィールドを決定的な順序・エンコーディングで連結する正準化が不可欠です。

バイトレイアウト

input_commitment = SHA-256(
    domain_tag       ← "stark-ballot:input|v1.0" (23 バイト, UTF-8)
    || version       ← u32 リトルエンディアン (4 バイト) = 10
    || election_id   ← UUID v4 バイナリ (16 バイト)
    || bulletin_root ← 32 バイト
    || tree_size     ← u32 リトルエンディアン (4 バイト)
    || total_expected← u32 リトルエンディアン (4 バイト)
    || votes_count   ← u32 リトルエンディアン (4 バイト)
    || [投票データ]  ← インデックス昇順でソートされた各投票
)

各投票のエンコーディング

投票配列の各要素は以下の形式でエンコードされます:

vote_entry =
    index            ← u32 リトルエンディアン (4 バイト)
    || commitment_len← u16 リトルエンディアン (2 バイト) = 32 (固定)
    || commitment    ← 32 バイト
    || path_len      ← u16 リトルエンディアン (2 バイト)
    || path_nodes    ← path_len × 32 バイト

フィールド一覧

public-input.json と公開監査アーティファクトとの関係

要点: public-input.json の全フィールドが入力コミットメントに束縛されるわけではありません。残りのフィールドは別チェックで補完的に検証されます。

public-input.json は、zkVM 検証に使う秘密データを含まない検証用レコードです。現行実装では schema、version、contractGeneration、electionId、electionConfigHash、bulletinRoot、treeSize、totalExpected、logId、timestamp、methodVersion と、各投票の index・コミットメント値・Merkle パスを含みます。

入力コミットメントが直接束縛するのはフィールド一覧に示した対象のみで、schema、version、contractGeneration、electionConfigHash、logId、timestamp、methodVersion は対象外です。これら対象外のフィールドは proof bundle 内の election-manifest.json や close-statement.json を組み合わせて、次のように照合されます。

• electionConfigHash → counted_election_manifest_consistent（manifest と journal 等を照合）
• logId・timestamp → counted_close_statement_consistent（close statement と journal 等を照合）
• schema・version・contractGeneration → public-input.json の互換性マーカーとして artifact 採用時に検証
• methodVersion → public-input.json 採用時に journal と照合。Image ID 解決では正規化済み journal 値を使用

正準化規則

エンコーディングの決定性を保証するために、以下の規則が厳守されます。

ソート規則

投票はエンコーディング前にインデックスの昇順にソートします。各投票の index は一意であることが前提であり、これにより同じ投票集合から常に同一のバイト列が生成されます。この規則に違反すると、TypeScript と Rust で異なるハッシュ値が計算され、検証が失敗します。

異常系の補助: 重複インデックスはプロトコル違反です。TS/Rust 双方は決定性のために commitment / merklePath で tie-break しますが、正常系仕様は index 昇順のままです。

エンディアン規則

すべての整数フィールドはリトルエンディアンでエンコードされます。

16 進数正規化

コミットメント値やパスノードなどの 16 進数表現は、0x プレフィックスを除去した上でバイト列にデコードされます。16 進数文字列のまま連結するのではなく、常にバイナリ表現を使用します。

TypeScript と Rust の同期

入力コミットメントは TypeScript（サーバー側）と Rust（zkVM ゲスト内）の双方で独立に計算され、結果が一致する必要があります。

flowchart LR
  subgraph TypeScript
    TS_IN[public-input.json から抽出した<br/>入力コミットメント対象フィールド] --> TS_CALC[正準エンコーディング<br/>+ SHA-256]
    TS_CALC --> TS_IC[入力コミットメント A]
  end

  subgraph "Rust (zkVM ゲスト)"
    RS_IN[ゲスト入力] --> RS_CALC[正準エンコーディング<br/>+ SHA-256]
    RS_CALC --> RS_IC[入力コミットメント B]
  end

  TS_IC --> CMP{A = B ?}
  RS_IC --> CMP
  CMP -->|一致| OK[検証成功]
  CMP -->|不一致| NG[検証失敗:<br/>入力データが異なる]

同期が破壊される典型的な原因:

• ソート順序の不一致
• エンディアンの不一致
• ドメインタグの文字列差異
• バージョン番号の不一致
• 16 進数正規化規則の差異（大文字/小文字、0x プレフィックスの有無）

検証パイプラインにおける役割

入力コミットメントは、Counted-as-Recorded 段階での検証チェック counted_input_commitment_match として使用されます。

このチェックが失敗すると、zkVM が処理した入力データと公開可能な検証データから再構成される対象フィールドが食い違うことを意味し、結果の信頼性が根本的に損なわれます。なお対象外フィールドは counted_election_manifest_consistent と counted_close_statement_consistent で補完的に検証されます（対応関係は上記を参照）。

各チェックの判定ロジックは チェック一覧 > Counted-as-Recorded を参照してください。

注意事項

入力コミットメントには投票者の秘密データ（選択肢や乱数）は含まれません。したがって、入力コミットメントの公開は投票の秘密性を損ないません。

入力順序に依存しない正準エンコーディングは、Property-based Testing の permutation invariance と、Lean による形式化 の input-commitment vectors で検査します。

STH ダイジェスト

Signed Tree Head ダイジェストを第三者と照合することで、分割ビュー攻撃をどう緩和するかを扱う章です。

ログ ID、ツリーサイズ、タイムスタンプ、掲示板ルートを束縛するダイジェストにより、サーバーが異なるクライアントに異なるツリー状態を提示する攻撃を検出可能にします。

概要

分割ビュー攻撃（split-view attack）とは、悪意あるサーバーが異なる検証者に対して異なる掲示板の状態を提示する攻撃です。例えば、投票者 A には「全 64 票が含まれたツリー」を見せながら、投票者 B には「特定の票が除外されたツリー」を見せることが考えられます。

STH ダイジェストは、掲示板の状態を（ログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュ）の組として束縛し、独立した第三者ソースとの合意確認を通じてこの攻撃を検出します。

flowchart TD
  subgraph "STH ダイジェストの構成"
    LID[ログ ID<br/>32 バイト]
    TSZ[ツリーサイズ<br/>4 バイト]
    TS[タイムスタンプ<br/>8 バイト]
    BR[掲示板ルート<br/>32 バイト]
  end

  LID --> H[SHA-256]
  TSZ --> H
  TS --> H
  BR --> H
  H --> STH[STH ダイジェスト<br/>32 バイト]

  STH --> J[zkVM ジャーナルに記録]
  STH --> CS[close-statement.json に記録]
  STH --> TP[第三者ソースの STH と照合]

本実装での検証対象: 本章で言う「STH ダイジェスト」は sthDigest 自体です。本実装は STH の署名検証は行いません（スコープの詳細は 合意ロジック を参照）。

ダイジェストフォーマット

sth_digest = SHA-256(
    log_id        ← 32 バイト
    || tree_size  ← u32 リトルエンディアン (4 バイト)
    || timestamp  ← u64 リトルエンディアン (8 バイト, Unix 時刻ミリ秒)
    || bulletin_root ← 32 バイト
)

SHA-256 への入力は合計 76 バイトです。

各フィールドの仕様

ログ ID

ログ ID は掲示板インスタンスを一意に識別するための値であり、以下のように生成されます:

log_id = SHA-256("stark-ballot:bulletin-log|v1.0" || seed)

ドメインタグ "stark-ballot:bulletin-log|v1.0" と任意のシード値を連結し、SHA-256 でハッシュします。ログ ID は掲示板のライフタイム中に変化しない固定値です。

ログ ID を STH ダイジェストに含めることで、異なる掲示板インスタンスの STH が偶然に衝突することを防止します。

分割ビュー攻撃と検出メカニズム

攻撃シナリオ

sequenceDiagram
    participant A as 投票者 A
    participant S as 悪意あるサーバー
    participant B as 投票者 B

    S->>A: ツリー状態 X<br/>(64 票、ルート R₁)
    S->>B: ツリー状態 Y<br/>(63 票、ルート R₂)
    Note over A,B: A と B は互いに異なる<br/>ツリー状態を見ている

この攻撃では、サーバーは投票者 B に対して特定の票を除外したツリーを見せています。投票者 B は自身に提示されたツリーに対する包含証明や整合性証明を検証できますが、投票者 A とは異なるツリーを見ていることに気づけません。

第三者合意による検出

検証者は、NEXT_PUBLIC_STH_SOURCES に設定された独立ソースへ問い合わせ、ジャーナル内の STH ダイジェストと照合することで分割ビューを検出できます。

sequenceDiagram
    participant V as 検証者
    participant S as サーバー
    participant T1 as 第三者ソース 1
    participant T2 as 第三者ソース 2

    V->>S: ジャーナルから STH ダイジェスト D' を取得
    V->>T1: STH を問い合わせ → D₁
    V->>T2: STH を問い合わせ → D₂
    V->>V: D' = D₁ = D₂ ?
    alt 全て一致
        V->>V: 合意成立 → 検証成功
    else 不一致あり
        V->>V: 分割ビューの疑い → 検証失敗
    end

合意ロジック

第三者 STH 検証は以下の条件をすべて満たした場合に成功します:

1. 十分な一致数: 一致するソースの数が最小要求数（コードフォールバック値: 2）以上
2. 全会一致: 応答可能なすべてのソースが一致すること（matchingSources = comparableSources）

各ソースに対して以下のフィールドが照合されます:

第三者ソースの応答は sthDigest を中心としたスナップショット情報として扱います。応答署名の検証、外部アンカリング、STH の自動公開は本実装のスコープ外です。

zkVM との連携

zkVM ゲストプログラムは、入力として受け取ったログ ID、ツリーサイズ、タイムスタンプ、掲示板ルートから STH ダイジェストを再計算し、ジャーナルにコミットします。

finalize 時には、同じツリー状態から close-statement.json も構築され、sthDigest が配布対象アーカイブ bundle.zip に含まれる公開監査アーティファクトへ反映されます。

この仕組みにより、STARK 証明と bundle.zip 内の close-statement.json がともに特定のツリー状態へ束縛されます。第三者はジャーナルの STH ダイジェストを独立ソースの値と照合することで、サーバーが証明と異なるツリー状態を提示していないかを確認できます。

検証パイプラインにおける役割

STH ダイジェストは 2 つの段階で利用されます。

recorded_sth_third_party は既定では任意チェック（optional）ですが、STH ソースが設定されている場合は必須扱いへ昇格します。昇格後は成功以外の状態にある限り「Verified」になりません（状態区分の扱いは チェック一覧 を参照）。

counted_close_statement_consistent は常に必須チェック（required）です。close-statement.json がジャーナルと整合しない場合、検証は失敗します。

各チェックの判定ロジックは チェック一覧 > Recorded-as-Cast と チェック一覧 > Counted-as-Recorded を参照してください。

設定

第三者 STH 検証は環境変数で制御されます。

STH ソースが未設定の場合、recorded_sth_third_party は not_run（未実行）となり、第三者照合は行いません。

開発用の .env.local.example では次の値が設定されています:

• NEXT_PUBLIC_STH_SOURCES=/api/sth
• NEXT_PUBLIC_STH_MIN_MATCHES=1

same-origin と /api/sth の取り扱い

same-origin 解決と認証ヘッダ転送: 相対パス（例: /api/sth）はリクエスト元のオリジンに対して解決されます。/api/sth は same-origin の session-scoped 開発用 API で、アクセスにはセッション capability が必要です。検証ロジックはセッション認証ヘッダーを same-origin ソースにのみ転送し、cross-origin ソースへは送りません。独立第三者ソースを absolute URL で構成する場合、それらはセッション認証に依存しない公開 STH エンドポイントである必要があります。

/api/sth の timestamp: /api/sth が返す timestamp はジャーナル内の canonical な時刻ではなく session.lastActivity です。そのため、第三者合意の一致判定で実際に照合するのは必須の sthDigest と、ソースが返した場合の bulletinRoot / treeSize です。

PoC における制約

本 PoC の開発用テンプレート（.env.local.example）では、STH ソースとして同一サーバー上の API エンドポイント（/api/sth）を使用します。同一サーバー上のソースのみでは防御力が限定的であるため、独立した組織が運営する複数ソースを NEXT_PUBLIC_STH_MIN_MATCHES >= 2 で構成することを推奨します。

ビットマップ Merkle

自票が集計に含まれたかを Merkle 証明で開示するためのビットマップツリーを扱う章です。

zkVM ゲスト内で計算されるビットマップにより、各投票インデックスが集計に含まれたかどうかを個別に検証可能にします。Merkle 証明により、自分の投票が含まれていることをサーバーを信頼せずに確認できます。

概要

Counted-as-Recorded 段階の検証では、zkVM に提示された入力に対する集計の正しさは STARK 証明で保証されますが、個々の投票者にとって「自分の票が集計に含まれたか」を直接確認する手段が別途必要です。

ビットマップ Merkle ツリーは、この「個別のカウント証明」を提供します。zkVM ゲストは投票ごとの状態をビットマップとしてエンコードし、その Merkle ルートをジャーナルにコミットします。投票者は自分のインデックスに対応するビットの Merkle 証明を取得し、「自分の票がカウントされたか」「そもそも prover に提示されたか」を独立に検証できます。

flowchart TD
  subgraph "zkVM ゲスト内"
    BM["ビットマップ<br/>[true, true, false, true, ...]"] --> PK[ビットパッキング<br/>LSB-first]
    PK --> CH[32 バイトチャンク分割]
    CH --> LH["リーフハッシュ<br/>SHA-256(0x00 || tag || chunk)"]
    LH --> MT[Merkle ツリー構築]
    MT --> ROOT["includedBitmapRoot / seenBitmapRoot"]
  end

  ROOT --> JNL[ジャーナルにコミット]

ビットマップの構造

ビットマップの定義

ビットマップは、ツリーサイズ（投票数）と同じ長さのブール配列です。現行実装では同じエンコーディング規則を持つ 2 種類のビットマップを扱います。

• includedBitmap[i] = true: インデックス i の投票が正常に検証され、集計に含まれた
• includedBitmap[i] = false: インデックス i の投票が除外された
• seenBitmap[i] = true: インデックス i の投票が prover に提示された
• seenBitmap[i] = false: インデックス i の投票が prover に提示されなかった

本 PoC では 64 票を扱うため、ビットマップは 64 ビット（= 8 バイト）です。

LSB-first ビットパッキング

ブール配列は LSB-first（Least Significant Bit first）方式でバイト列にパッキングされます。

ビット配列: [b₀, b₁, b₂, b₃, b₄, b₅, b₆, b₇, b₈, ...]

バイト 0 = b₀ | (b₁ << 1) | (b₂ << 2) | ... | (b₇ << 7)
バイト 1 = b₈ | (b₉ << 1) | ...

64 ビットのビットマップは 8 バイトにパッキングされます。

32 バイトチャンク分割

パッキングされたバイト列は 32 バイト（256 ビット）単位のチャンクに分割されます。各チャンクが Merkle ツリーの 1 つのリーフとなります。

• 1 チャンク = 32 バイト = 256 ビット分の投票カウント状態
• 最後のチャンクが 32 バイトに満たない場合はゼロパディング

本 PoC の 64 票は 8 バイトであるため、1 つのチャンク（24 バイトのゼロパディング付き）に収まります。

Merkle ツリーの構築

ハッシュ規則

ビットマップ Merkle ツリーは、CT Merkle ツリーと同一のハッシュ規則を使用します。

リーフハッシュ:

LeafHash = SHA-256(0x00 || "stark-ballot:leaf|v1" || chunk)

内部ノードハッシュ:

NodeHash = SHA-256(0x01 || left_hash || right_hash)

ドメイン分離プレフィックス（0x00 / 0x01）と使用タグ（"stark-ballot:leaf|v1"）は、CT Merkle ツリーの章で解説したものと同一です。

ツリー構築アルゴリズム

1. 各 32 バイトチャンクにリーフハッシュを適用
2. ボトムアップでペアを結合し、内部ノードハッシュを計算
3. 奇数ノードがある場合は、そのまま次のレベルに昇格（ハッシュなし）
4. ルートに到達するまで繰り返す

graph TD
  subgraph "3 チャンクの場合"
    R["ルート<br/>SHA-256(0x01 || N1 || C2)"]
    N1["ノード<br/>SHA-256(0x01 || C0 || C1)"]
    C2["リーフ 2<br/>SHA-256(0x00 || tag || chunk₂)"]
    C0["リーフ 0<br/>SHA-256(0x00 || tag || chunk₀)"]
    C1["リーフ 1<br/>SHA-256(0x00 || tag || chunk₁)"]

    R --> N1
    R --> C2
    N1 --> C0
    N1 --> C1
  end

Merkle 証明の生成と検証

証明の構造

GET /api/bitmap-proof?i=<bitIndex>&kind=included|seen のレスポンスは、以下の要素で構成されます:

leafIndex（floor(bitIndex / 256)）と bitOffset（bitIndex mod 256）は、クライアント側で bitIndex クエリから導出します。サーバーは返しません。

kind は省略可能で、既定値は included です。

• kind=included: includedBitmapRoot に対する証明を返す
• kind=seen: seenBitmapRoot に対する証明を返す

このエンドポイントは無認証の公開 API ではなく、セッション ID と capability token を要する証明材料 API です（仕様は外部クライアント向けに文書化されています）。

ビット抽出

投票者は受け取ったチャンクから、自分が指定した bitIndex のビットを以下の手順で抽出します:

bit_offset  = bit_index mod 256
byte_index  = bit_offset / 8    (整数除算)
bit_in_byte = bit_offset mod 8

included = (chunk[byte_index] AND (1 << bit_in_byte)) != 0

kind=included で included = true なら、自分の投票がカウントされたことを意味します。kind=seen で included = true なら、自分の投票が prover に提示されたことを意味します。

検証手順

1. チャンクからビット値を抽出し、自分の投票がカウントされたか確認
2. チャンクのリーフハッシュを計算: SHA-256(0x00 || "stark-ballot:leaf|v1" || chunk)
3. 監査パスに沿ってルートまで再計算:
   • 兄弟の位置が left → SHA-256(0x01 || sibling || current)
   • 兄弟の位置が right → SHA-256(0x01 || current || sibling)
4. 計算されたルートが、kind に対応するジャーナル上のルートと一致するか確認
   • kind=included → includedBitmapRoot
   • kind=seen → seenBitmapRoot

flowchart TD
  CK[チャンク受信] --> EX[ビット抽出<br/>included = true/false]
  CK --> LH["リーフハッシュ計算"]
  LH --> AP[監査パスに沿って<br/>ルートを再計算]
  AP --> CMP{計算ルート =<br/>bitmap root ?}
  CMP -->|一致| V[証明有効]
  CMP -->|不一致| IV[証明無効]

zkVM ゲストとの連携

ビットマップルートは zkVM ゲストプログラム内で計算され、ジャーナルにコミットされます。

ゲストプログラムは以下の手順を実行します:

1. 各投票に対してコミットメントの再計算と包含証明の検証を実施
2. prover に提示された投票インデックスを seenBitmap に記録
3. 検証に成功して集計対象になった投票インデックスを includedBitmap に記録
4. それぞれのビットマップを LSB-first でパッキングし、32 バイトチャンクに分割
5. CT スタイルのハッシュ規則で Merkle ルートを計算
6. seenBitmapRoot と includedBitmapRoot をジャーナルにコミット

この計算はゲスト内で行われるため、STARK 証明がビットマップの正しさも保証します。サーバーが事後的にビットマップを改ざんしても、ジャーナルのルート値と一致しなくなるため検出されます。

サーバーのビットマップデータ管理

サーバーは /api/bitmap-proof 用に、最終化時の zkVM 出力（includedBitmap、ある場合は seenBitmap / seenBitmapRoot）を非公開 sidecar として保持します。これらは配布対象アーカイブ bundle.zip には含まれず、async finalize 経路では必要に応じて S3 の sibling object から復元されます。

安全性ゲートと検証結果の分岐

採用前と採用後で、counted_my_vote_included の判定が次の 2 つに分岐します。

• 採用前に弾かれる、または証明材料が取得できない → counted_my_vote_included は not_run（証拠不足による fail-closed）。例:
  • zkVM 出力に bitmap データが無い
  • 保存・復元時の root 一致ゲートで採用されなかった
  • cast-time 証跡（voteReceipt / userVote.proof）が store から再構成できず voteReceipt.bulletinIndex が確定しない
• 採用後にクライアント側の root 照合が失敗 → counted_my_vote_included は failed。サーバーが返した chunk と audit path から再計算したルートが、ジャーナルの includedBitmapRoot（または seenBitmapRoot）と一致しない。

採用前ゲートおよび counted_my_vote_included の評価詳細は チェック一覧 > counted_my_vote_included を参照してください。

検証パイプラインにおける役割

ビットマップ Merkle 証明は、Counted-as-Recorded 段階のチェックとして使用されます。

seenBitmapRoot が利用可能な場合は、このチェックが「prover に提示されたが無効化された」と「そもそも提示されなかった」も区別して説明します。

各チェックの判定ロジックは チェック一覧 > Counted-as-Recorded を参照してください。

プライバシーに関する注意

ビットマップ Merkle 証明では、対象ビットを含む 32 バイトチャンク全体がクライアントに提供されます。1 チャンクは 256 ビット分のカウント状態を含むため、近傍のインデックスのカウント状態が同時に開示されます。

本 PoC では 64 票が 1 チャンクに収まるため、チャンクを受け取った投票者は全 64 票のカウント状態を知ることができます。これは 63 票がボットのためチャンク漏洩の情報価値が限定的という割り切りで成立しています。影響評価と将来の緩和策は PoC の意図的な制約 > ビットマップチャンク漏洩 を参照してください。

LSB-first packing とビット境界の扱いは、Property-based Testing で生成入力を使って境界条件を探索し、Lean による形式化 の bitmap vectors で抽象モデルとの対応を検査します。

zkVM 設計

投票集計の正当性を STARK 証明として外部に持ち出す zkVM パイプラインを扱う部です。

この部に含まれる章

• zkVM の基礎 — zkVM の概念、RISC Zero の選択理由、データフロー、保証境界
• ゲストプログラム — zkVM 内で実行される検証・集計ロジック
• ホストと証明生成 — ホストプログラムと同期/非同期の証明パス
• 検証サービス — Rust ベースのレシート検証
• Image ID — ゲストバイナリの暗号的識別子と管理

想定読者と前提

• 想定読者: 集計の正当性を STARK で証明したい実装者・運用者
• 前提: 暗号プロトコル の入力コミットメントと Merkle ツリーを把握していること

本章で扱わないもの

• RISC Zero SDK の API リファレンスやアップグレード手順
• STARK / FRI の数学的構成証明（概念のみ zkVM の基礎 で扱う）
• ECS Fargate などインフラ側の構成（AWS アーキテクチャ を参照）

関連する章

• 暗号プロトコル — ゲストプログラムが入力として受け取るプリミティブ
• 検証パイプライン — 生成されたレシートとジャーナルがどのように検証されるか
• AWS アーキテクチャ — 非同期プローバーの実行環境
• 第三者検証ガイド — bundle.zip でレシートをローカル監査する手順

zkVM の基礎

RISC Zero zkVM を採用した理由、データフロー、暗号学的保証の境界を整理する章です。

なぜ RISC Zero か

• Trusted setup 不要で扱いやすい。
• RISC-V 上で通常の Rust コードを使えるため、実装と監査の往復がしやすい。
• Image ID による実行バイナリ照合と組み合わせやすい。

アーキテクチャ概要

zkVM パイプラインは 3 つのコンポーネントで構成されます。

flowchart TB
  subgraph C1["第1フェーズ: 入力構築"]
    SES[セッションデータ] --> IB[入力ビルダー]
    IB --> INP[ZkVMInput]
  end

  subgraph C2["第2フェーズ: 証明生成"]
    INP --> HOST[ホストプログラム]
    HOST --> GUEST["ゲストプログラム<br/>(zkVM 内実行)"]
    GUEST --> JNL[ジャーナル]
    HOST --> RCP[レシート<br/>STARK 証明]
  end

  subgraph C3["第3フェーズ: 検証"]
    RCP --> VS[検証サービス]
    VS --> VR[検証レポート]
  end

zkVM とは

RISC Zero zkVM は、RISC-V（RV32IM）命令列として実行されるゲストプログラムに対して、その実行が正しいことを STARK 証明で示すゼロ知識 VM です。

本システムでは「投票検証と集計」をゲストとして実行し、ホストがレシート（seal + journal）を生成します。第三者は Receipt::verify(image_id) により、指定したゲストバイナリ（Image ID）で実行された結果であることを検証できます。

30 秒で要点

ジャーナルは証明に束縛される公開出力で、検証成功時に改ざんできません。ジャーナル項目の一覧と各フィールドが何を保証するかは ゲストプログラム > ジャーナル出力 を参照してください。配布対象ファイル（bundle.zip 等）との違いは バンドル構造 を参照してください。

RISC Zero zkVM 実装の要点

RISC Zero 公式ドキュメントに基づく実装上の要点:

1. 実行モデル: ゲストは RV32IM として決定論的に実行され、外部との境界は syscall (ecall) で扱う
2. 証明の分割: 長い実行はセグメント証明に分割される（大規模実行を扱うため）
3. 再帰合成と圧縮: SDK は再帰合成や succinct / Groth16 への圧縮をサポートするが、本 PoC は Composite receipt のまま配布する
4. 検証 API: Receipt::verify(image_id) が、証明本体と Image ID の束縛を同時に検証する
5. 公開出力の束縛: journal は証明に束縛されるため、検証成功後に改ざんできない

ジャーナルとレシート

• ジャーナル: ゲストが公開出力としてコミットするデータ（検証済み集計、除外情報、入力コミットメントなど）
• レシート: ジャーナルと STARK 証明（seal）のペア。検証成功時、ジャーナルは正しいゲスト実行結果として受理できる

flowchart TB
  R[レシート]
  R --> S[Seal<br/>STARK 証明]
  R --> J[ジャーナル<br/>公開出力]

ジャーナル各フィールドの定義と検証チェックとの対応は ゲストプログラム > ジャーナル出力 を、excludedSlots と rejectedRecords の使い分けは スロット / レコード分離モデル を参照してください。

数学ミニ補足（読み飛ばし可）

STARK の直感的理解に必要な最小限の説明だけを記します。

1. 巡回ドメイン（cyclic domain）

有限体 F の乗法群の部分群 H = {1, w, w^2, ..., w^(n-1)} を評価点集合（ドメイン）として使います。RISC Zero はこれを cyclic domain と呼びます。実行トレース（レジスタ値や遷移）は、この H 上で評価される多項式として扱われます。

2. 有限体上の多項式除算

制約違反の有無は、概念的には次の形で整理できます。

• 制約多項式を C(x) とする
• 評価領域 H の零化多項式を Z_H(x) とする（典型例: Z_H(x) = x^n - 1）
• すべての点で制約を満たすなら C(h)=0（h in H）となり、C(x) は Z_H(x) で割り切れる
• したがって Q(x) = C(x) / Z_H(x) が多項式として成立するかを検査すれば、制約満足性をチェックできる

実際の STARK では、これを FRI（Fast Reed-Solomon IOP）と Merkle コミットメントを組み合わせて効率的に検証します。

この PoC での保証境界

Receipt::verify(image_id) の成功は強い保証ですが、それ単体で「全票が提示された」ことまでは保証しません。Verified 表示は次がすべて揃った場合にのみ成立します。

1. STARK 検証成功（正しいゲスト実行）
2. excludedSlots == 0（除外スロットなし）
3. totalExpected == treeSize（期待数と掲示板ツリーサイズの一致）
4. 追記専用性と締切 STH の必須チェック成功

加えて、必須チェックが not_run / pending / running のままでは Verified にはなりません。第三者 STH チェックは source 設定時に限り required に昇格します。詳細なゲーティング規範と判定ロジックは ゲーティングロジック を参照してください。

参考資料（RISC Zero 公式）

• zkVM Technical Specification
• Recursion (proof composition)
• STARK by Hand

データフロー

投票セッションの開始からレシート検証までの全体的なデータフローを示します。

sequenceDiagram
  participant V as 投票者
  participant S as サーバー
  participant B as 掲示板
  participant H as ホスト
  participant G as ゲスト (zkVM)
  participant VS as 検証サービス

  Note over V,B: 投票フェーズ
  V->>S: 投票意図（選択肢・乱数）+ コミットメント
  S->>B: 掲示板に追記
  S-->>V: 投票レシート (インデックス, ルート)
  Note over S: ボット投票を自動追加

  Note over S,G: 集計フェーズ
  S->>S: 入力ビルダーで ZkVMInput を構築
  S->>H: ZkVMInput を渡す
  H->>G: ゲスト実行を開始
  G->>G: 各投票のコミットメント検証
  G->>G: 各投票の包含証明検証
  G->>G: 集計 + ビットマップ計算
  G-->>H: ジャーナル出力
  H-->>S: STARK レシート + ジャーナル

  Note over S,VS: 検証フェーズ
  S->>VS: 検証 bundle 参照 + 期待 Image ID
  VS->>VS: bundle 内の receipt.json を解決
  VS->>VS: Receipt::verify(image_id)
  VS-->>S: 検証レポート
  S-->>V: 検証結果を提供

ゲストプログラム

zkVM 内のゲストが、入力検証から集計・ビットマップ計算までをどう構成するかを扱う章です。

ゲストプログラムは、投票コミットメントの再計算、RFC 6962 包含証明の検証、集計の実行、ビットマップルートの計算を行い、結果をジャーナルにコミットします。

契約上重要なヘルパー（コミットメント計算、正準エンコーディング、RFC 6962 包含証明、ビットマップルートなど）は zkvm/contract-core/ に集約されており、ゲストとホストが同じ実装を参照します。

概要

ゲストプログラムは RISC Zero zkVM 上で動作する Rust プログラムです。ホストから投票データ（選択肢・乱数・コミットメント・Merkle パスと選挙メタデータ）を受け取り、以下の処理を行います:

1. 各投票の正当性検証（コミットメント再計算 + 包含証明）
2. 有効投票の集計
3. カウント状態と提示状態のビットマップ計算
4. 入力コミットメントと STH ダイジェストの計算
5. 結果のジャーナルへのコミット

ゲスト内の処理はすべて STARK 証明に含まれるため、出力（ジャーナル）の正しさが暗号学的に保証されます。

入力構造

ゲストプログラムが受け取る入力（AggregatorInput）の構造を示します。

各 VoteWithProof は以下のフィールドを持ちます:

処理パイプライン

ゲストプログラムの処理は、入力検証、投票検証・集計、出力構築の 3 フェーズで構成されます。

flowchart TD
  subgraph "フェーズ 1: 入力検証"
    I1[入力デシリアライズ] --> I2{掲示板ルート<br/>が非ゼロ?}
    I2 -->|Yes| I3{ツリーサイズ<br/>が正の値?}
    I2 -->|No| FAIL[不正入力]
    I3 -->|Yes| I4{Phase 4 境界と<br/>Merkle パス長が有効?}
    I3 -->|No| FAIL
    I4 -->|Yes| NEXT[フェーズ 2 へ]
    I4 -->|No| FAIL
  end

  subgraph "フェーズ 2: 投票検証と集計"
    NEXT --> LOOP[各投票に対して]
    LOOP --> V1[6 段階検証]
    V1 -->|有効| TALLY[集計に加算]
    V1 -->|無効| EXCL[却下カウントと<br/>スロット統計に反映]
    TALLY --> BIT[ビットマップ更新]
  end

  subgraph "フェーズ 3: 出力構築"
    LOOP -->|全投票完了| O1[ビットマップルート計算]
    O1 --> O2[入力コミットメント計算]
    O2 --> O3[STH ダイジェスト計算]
    O3 --> O4[ジャーナルにコミット]
  end

Note: 次のいずれかに該当する入力は、ジャーナル生成前に fail-closed で拒否されます。

• bulletin_root がゼロ
• tree_size が 0
• tree_size > 1,000,000
• total_expected > 1,000,000
• votes.length > 1,000,000
• 候補別 tally bucket が 1,000,000 を超える
• Merkle パス長が u16::MAX を超える

votes.length > tree_size のような入力は、上記境界内であれば事前 reject されません。重複や範囲外は record 単位で rejectedRecords に反映されます。

投票の 6 段階検証

各投票に対して、以下の 6 つの検証が順に実行されます。いずれかが失敗した投票は即座に「無効」として除外され、以降の検証はスキップされます。

flowchart TD
  V[投票] --> C1{"第1検証<br/>インデックス範囲チェック"}
  C1 -->|失敗| INV[無効として除外]
  C1 -->|成功| C2{"第2検証<br/>インデックス重複チェック"}
  C2 -->|失敗| INV
  C2 -->|成功| C3{"第3検証<br/>選択肢範囲チェック"}
  C3 -->|失敗| INV
  C3 -->|成功| C4{"第4検証<br/>コミットメント再計算と照合"}
  C4 -->|失敗| INV
  C4 -->|成功| C5{"第5検証<br/>コミットメント重複チェック"}
  C5 -->|失敗| INV
  C5 -->|成功| C6{"第6検証<br/>包含証明検証"}
  C6 -->|失敗| INV
  C6 -->|成功| VALID[有効: 集計に加算]

各検証の失敗条件と、失敗したレコードがどのカウンタに反映されるかを示します。

範囲内かつ初出のスロットが #3〜#6 で無効化された場合、seenBitmap ではビットが立ち（提示はされた）、includedBitmap ではビットが立たない（計上されない）ため、invalidPresentedSlots として観測されます。範囲外（#1）や既処理スロットへの重複レコード（#2）は rejectedRecords のみに反映され、スロット単位の指標には影響しません。

コミットメント再計算と照合（#4）

ゲスト内で投票者の（選択肢, 乱数, 選挙 ID）からコミットメントを再計算し、入力として渡された値と照合します。これにより、投票者が主張する選択肢が掲示板上のコミットメントと一致することが保証されます。計算規則は コミットメントスキーム を参照してください。

RFC 6962 包含証明検証（#6）

投票のコミットメントが掲示板 Merkle ツリーに含まれることを、RFC 6962 PATH 関数ベースの CT スタイル包含証明で検証します。投票のインデックスと Merkle パスから掲示板ルートを再計算し、入力の bulletin_root と一致するかを確認します。リーフ・ノードハッシュの規則とドメインタグは CT Merkle ツリー を参照してください。

集計ロジック

6 段階検証をすべて通過した投票は「有効」として集計に加算されます。

• 集計は選択肢ごとの配列（5 要素）で管理
• 有効投票のインデックスに対応する includedBitmap のビットを true に設定
• 無効投票はカウントされず、includedBitmap のビットは false のまま
• 範囲内かつ初出として提示された無効票は seenBitmap では true になり、提示済みだが未計上のスロットとして扱われる

スロット / レコード分離モデル

現行のゲストプログラムは、掲示板スロットに対する完全性と、入力レコードの異常を別々に記録します。

flowchart LR
  TS["ツリーサイズ<br/>(全スロット)"]
  TS --> CNT["カウント済み<br/>validVotes"]
  TS --> INV["提示されたが未計上<br/>invalidPresentedSlots"]
  TS --> MIS["未提示<br/>missingSlots"]
  REC["入力レコード"] --> REJ["却下レコード<br/>rejectedRecords"]

スロット単位の 3 分類は、現行実装では常に次の関係を満たします:

validVotes + invalidPresentedSlots + missingSlots = treeSize

fail-closed 判定に使われる除外数は、スロット単位の excludedSlots です:

excludedSlots = missingSlots + invalidPresentedSlots

excludedSlots > 0 は検証失敗の決定的な指標です。1 スロットでも未提示または未計上であれば、集計結果の完全性が損なわれていることを意味します。

一方で rejectedRecords はレコード単位の補助指標です。たとえば次のようなケースでは rejectedRecords は増えても excludedSlots は増えません。

• 既に正しくカウント済みのスロットに対する重複インデックスレコード
• tree_size の外側を指す範囲外レコード

旧 public contract の互換名は現行 journal にも公開レスポンスにも現れませんが、参考までに 1 対 1 対応を示します。

※ rejectedRecords は record 単位の新設カウントで、旧 invalidIndices の mirror は invalidPresentedSlots 側。

ジャーナル出力

ゲストプログラムがジャーナルにコミットする出力構造（VerificationOutput）を示します。

ジャーナルの信頼モデル

ジャーナルの各フィールドは、対応する STARK 証明により「ゲストプログラムが正しく計算した結果」であることが保証されます。

一方、STARK 証明だけでは保証されないものがあります。「ゲストに提示されなかった票」「第三者 STH との合意」「ホストやサーバーの正直性」はジャーナル外の独立チェックで確認します。第三者はレシートの STARK 検証を行うだけで上記の保証を取得でき、ゲストロジックの信頼以外にホスト・サーバーを信頼する必要はありません。

ビットマップルートの計算

ゲストプログラムは投票検証と並行して seenBitmap（範囲内かつ初出として提示されたインデックス集合）と includedBitmap（6 段階検証を通過したインデックス集合）の 2 種類を構築し、それぞれの Merkle ルートをジャーナルにコミットします。この 2 つのルートを併用することで、公開検証側は「prover に提示されたが無効化された票」と「そもそも提示されなかった票」を区別できます。

LSB-first のバイト列パッキング、32 バイト境界による単一リーフ / 分割リーフの扱い、leaf / node hash 規則は ビットマップ Merkle を参照してください。

入力コミットメントと STH ダイジェスト

ゲストプログラムは投票処理の後、2 つの追加ハッシュ値を計算してジャーナルにコミットします。

入力コミットメント

ゲストに渡された入力のうち、公開フィールドを正準エンコーディングで連結し SHA-256 で圧縮します。現行実装では固定のドメインタグと format version を先頭に付与した上で、electionId・bulletinRoot・treeSize・totalExpected・votesCount と各投票の index・コミットメント値・Merkle パスを束縛します。投票列はハッシュ前に index 昇順で正規化されます（異常入力時の tie-break 補助ルールは 入力コミットメント > ソート規則 を参照）。

第三者は public-input.json などの公開検証用レコードから同じ値を再計算し、ジャーナルの値と照合することで、zkVM が処理した入力の同一性を検証できます。

詳細は 入力コミットメント を参照してください。

STH ダイジェスト

掲示板のログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュを結合して SHA-256 で圧縮します。このダイジェストは第三者の STH ソースとの照合に使用され、サーバーが異なる投票者に異なる掲示板ビューを提示する分割ビュー攻撃を緩和します。

詳細は STH ダイジェスト を参照してください。

ゲストプログラムのバージョニング

ゲストプログラムにはバージョン番号が割り当てられ、ジャーナルの methodVersion フィールドに記録されます。現行のジャーナル契約は 14 です。

バージョン番号は Image ID の管理と連動しており、ゲストプログラムの変更は新しい Image ID の生成を伴います。検証時には、期待 Image ID との一致が確認されます。

ゲストの抽象 tally / rejection model と guest bounds は、Lean による形式化 で説明しています。Rust 側の guest-vector tests は、抽象モデルと実装の対応付けを検査します。

ホストと証明生成

ホストプログラムが zkVM 入力を組み立て、同期 / 非同期で STARK 証明を生成する流れを扱う章です。

同期モード（ローカルプロセス起動）と非同期モード（ECS Fargate タスク）の 2 つの証明パスがあり、どちらも同一のホストバイナリを使用します。入力構築からレシート出力までのフローを、両モードの差異とともに説明します。

パイプライン全体像

証明生成パイプラインは、入力構築、ホスト実行、出力処理の 3 フェーズで構成されます。

flowchart TD
  subgraph "第1フェーズ: 入力構築 (TypeScript)"
    SD[セッションデータ] --> IB[入力ビルダー]
    IB --> ZI[ZkVMInput]
    ZI --> SER[シリアライズ<br/>JSON ファイル]
  end

  subgraph "第2フェーズ: ホスト実行 (Rust)"
    SER --> HOST[ホストバイナリ]
    HOST --> ENV[ExecutorEnv 構築]
    ENV --> PROVER[デフォルトプローバー]
    PROVER --> GUEST[ゲスト実行]
    GUEST --> PROOF[STARK 証明生成]
  end

  subgraph "第3フェーズ: 出力処理"
    PROOF --> RCP["レシートラッパー JSON<br/>(seal + journal)"]
    PROOF --> OUT["出力 JSON<br/>(デコード済みジャーナル)"]
  end

入力構築

セッションデータからの抽出

入力ビルダーは、投票セッションに蓄積されたデータから zkVM 入力を構築します。

flowchart LR
  subgraph セッションデータ
    EID[選挙 ID]
    ECFG[選挙設定<br/>+ 設定ハッシュ]
    VOTES["投票データ<br/>(選択肢, 乱数, コミットメント)"]
    BULL["掲示板<br/>(ルート履歴, 包含証明)"]
    LID[ログ ID]
  end

  subgraph ZkVMInput
    EID2[election_id]
    ECFG2[election_config_hash]
    BR[bulletin_root]
    TS[tree_size]
    TE[total_expected]
    VWP["votes[]<br/>(VoteWithProof)"]
    LID2[log_id]
    TSTAMP[timestamp]
  end

  EID --> EID2
  ECFG --> ECFG2
  ECFG --> TE
  BULL --> BR
  BULL --> TS
  VOTES --> VWP
  LID --> LID2

入力構築で行われる主要な処理:

1. 掲示板の最新 STH スナップショット取得: ルートハッシュ、ツリーサイズ、タイムスタンプを取得
2. 選挙設定の整合性確認: electionConfig と electionConfigHash が一致することを確認
3. 投票データの変換: 各投票の選択肢を整数に変換（A=0, B=1, C=2, D=3, E=4）
4. Merkle パスの解決: 各投票について、掲示板から最新の包含証明を取得
5. 総投票数の設定: 選挙設定の totalExpected（本 PoC ではボット 63 票 + ユーザー 1 票 = 64）

通常のセッション入力では、投票インデックスは 0 から連続する canonical CT index であることを要求します。教育的な除外シナリオでは、元の掲示板インデックスを保つために sparse index を許可します。これによりゲスト側で missingSlots として観測できるようになります。

Merkle パスの解決戦略

各投票の Merkle パスは、以下の優先順位で解決されます:

flowchart TD
  START[Merkle パス解決] --> P1{掲示板から<br/>包含証明を取得可能?}
  P1 -->|Yes| USE1[掲示板の証明を使用]
  P1 -->|No| P2{投票データに<br/>事前計算パスが存在?}
  P2 -->|Yes| CHK{treeSize が一致?}
  CHK -->|Yes| USE2[事前計算パスを使用]
  CHK -->|No| ERR[エラー]
  P2 -->|No| ERR

ホストプログラムの実行

ホストバイナリの役割

ホストバイナリは Rust で記述された CLI プログラムです。証明モードでは以下の処理を行います:

1. JSON 形式の入力ファイルを読み込み
2. JSON のバイト配列表現を Rust の固定長配列型へ変換（Vec<u8> → [u8; 16/32]）
3. ExecutorEnv に入力をシリアライズして設定
4. デフォルトプローバーを使用して zkVM ゲストを実行
5. レシート（STARK 証明 + ジャーナル）を取得
6. ジャーナルをデコードし、出力ファイルに書き出し

入力 JSON は TypeScript 側のエグゼキューターが事前に正規化して生成します（UUID/ハッシュ文字列をバイト配列へ変換）。

ImageID の確認だけを行う場合は host --print-image-id [--json] を使います。このモードでは入力ファイルを読まず、証明生成やアーティファクト出力も行いません。--json 付きでは imageId と methodVersion を含む JSON を stdout に出力します。

境界に違反する入力が渡された場合、host run は fail-closed で停止し、receipt / journal を出力しません。境界条件の詳細は 処理パイプライン を参照してください。

非同期モードで S3 に置かれる work input には、host CLI の証明入力に加えて contractGeneration と election_config も含まれます（コンテナ entrypoint 側で public-input.json / election-manifest.json を生成・検査するために使う）。

出力ファイル

証明モードのホストバイナリは 2 つの JSON ファイルを出力し、ビットマップ整合性検査を通過した場合は private bitmap artifact も追加で出力します。

レシートラッパー JSON には top-level image_id フィールドも含まれます。検証サービスでの使われ方は 検証サービス を参照してください。

また、ホストはビットマップの整合性を確認し、一致した場合のみ以下の非公開アーティファクトを出力します。

非同期モードでは、これらの host 生出力は included-bitmap.json / seen-bitmap.json として bundle.zip の隣に配置されます。どちらも非公開アーティファクトであり、配布対象アーカイブ bundle.zip には含めません。

同期モード

同期モードでは、TypeScript のサーバーサイドプロセスからホストバイナリを直接起動します。

sequenceDiagram
  participant S as サーバー (TypeScript)
  participant E as エグゼキューター
  participant H as ホストバイナリ (Rust)
  participant FS as ファイルシステム

  S->>E: executeZkVM(input)
  E->>FS: 入力 JSON を一時ファイルに書き出し
  E->>H: 子プロセスとして起動
  Note over H: zkVM ゲスト実行<br/>+ STARK 証明生成
  H->>FS: レシートラッパー JSON + 出力 JSON を書き出し
  H-->>E: プロセス終了
  E->>FS: 出力ファイルを読み取り
  E->>FS: 一時ファイルを削除
  E-->>S: ZkVMExecutionResult

同期モードの特性

結果の変換

エグゼキューターは出力 JSON のフィールドを TypeScript の命名規則へ正規化し、文字列だけでなくバイト配列形式の値も受理します。ハッシュ系フィールドは 0x 付き 16 進文字列に、election_id は UUID 文字列に変換して ZkVMExecutionResult を構築します。

非同期モード

AWS 環境では、証明生成を ECS Fargate タスクとして非同期に実行します。STARK 証明の生成に数分を要するため、Lambda のタイムアウト制限を回避し、専用のコンピューティングリソースを割り当てます。

sequenceDiagram
  participant S as サーバー
  participant SQS as SQS
  participant D as ディスパッチ Lambda
  participant SFN as Step Functions
  participant ECS as ECS Fargate
  participant S3 as S3
  participant CB as コールバック Lambda

  S->>SQS: ファイナライズリクエスト
  SQS->>D: work message
  D->>S3: 入力 JSON アップロード
  D->>SFN: SFN 実行開始<br/>(inputS3Key を渡す)
  Note over SFN: イメージ署名チェック
  SFN->>ECS: プローバータスク起動
  ECS->>S3: 入力 JSON ダウンロード
  Note over ECS: ホストバイナリ実行<br/>+ STARK 証明生成
  ECS->>S3: レシート・ジャーナル・<br/>バンドルをアップロード
  ECS-->>SFN: タスク完了
  SFN->>CB: 成功コールバック
  CB->>CB: セッションデータ更新

イメージ署名チェック

Step Functions はプローバータスク起動前にコンテナイメージの署名を検証し、承認されたイメージ以外の実行を拒否します。署名と digest pin の運用は イメージ署名 を参照してください。

配布対象アーカイブの構築

非同期モードでは、ホストバイナリの出力のうち秘密データを含まないファイルだけを bundle.zip に同梱し、input.json などの秘密入力は含めません。同梱対象の一覧、整合性検査ルール、取得経路は バンドル構造 を参照してください。public-input.json の項目と inputCommitment の関係は 入力コミットメント。

async Docker entrypoint は methodVersion 14 の host output を受け付け、journal.json / public-input.json / election-manifest.json / close-statement.json を生成する際に methodVersion と inputCommitment の整合性を検査します。methodVersion 14 契約と一致しない host artifact は fail-closed で停止します。

非同期モードの特性

開発モードの動作

RISC0_DEV_MODE=1 を設定すると、RISC Zero は STARK 証明を生成せず、フェイクレシートを返します。

開発モードのレシートは内部的には InnerReceipt::Fake 型で、検証サービス では通常 dev_mode 扱い（image_id 不一致などの事前条件違反時のみ Failed）になります。dev_mode は診断ステータスであり、本番モードの成功検証としては採用されません。

開発モードは以下の用途に限定されます:

• host CLI や verifier 連携を含むローカルの高速フィードバック
• TypeScript と Rust の契約を短時間で確認する smoke test
• dev-mode receipt 分岐を明示的に通す CLI / E2E 検証

UI 開発などで使う USE_MOCK_ZKVM=true は、TypeScript の mock executor を選ぶ別経路です。この経路はホストバイナリも RISC Zero SDK も呼ばず、TypeScript 内で完結します。

検証サービス

STARK レシートを検証する Rust サービスの構造と、ローカル / Lambda 双方での使い方を扱う章です。

レシートの STARK 検証をサーバー側で行い、結果をレポートとしてクライアントに提供する Rust コンポーネントです。

概要

STARK 証明の検証は計算コストが証明生成に比べて低いものの、ブラウザ上で RISC Zero の検証ロジックを実行することは現時点では実用的ではありません。そのため、本システムではサーバー側で検証を行い、その結果をレポートとしてクライアントに提供する設計を採用しています。

flowchart LR
  subgraph 入力
    RCP[レシート / バンドル]
    EID["期待 Image ID"]
  end

  RCP --> VS[検証サービス]
  EID --> VS
  VS --> RPT[検証レポート]

検証フロー

検証サービスは以下の手順でレシートを検証します。

flowchart TD
  START[レシート / バンドル読み込み] --> FORMAT{入力形式<br/>の判定}
  FORMAT -->|フラット JSON| F1[直接パース]
  FORMAT -->|ネスト JSON| F2[receipt フィールドを抽出]
  FORMAT -->|ディレクトリ| F3[receipt.json または<br/>*-receipt.json を探索]
  FORMAT -->|ZIP アーカイブ| F4[末尾が receipt.json のファイルを探索]
  F1 --> EXTRACT[Image ID 抽出]
  F2 --> EXTRACT
  F3 --> EXTRACT
  F4 --> EXTRACT

  EXTRACT --> MODE[InnerReceipt を判定<br/>Fake は dev_mode 候補として記録]
  MODE --> PRESENT{メタデータ image_id<br/>が存在?}
  PRESENT -->|欠落 + 非 Fake| FAIL0[failed]
  PRESENT -->|欠落 + Fake| VERIFY
  PRESENT -->|存在| MATCH{メタデータ Image ID<br/>= 期待 Image ID ?}
  MATCH -->|不一致| FAIL1[failed:<br/>Image ID 不一致]
  MATCH -->|一致| VERIFY["Receipt::verify(expected_image_id)<br/>STARK 検証実行"]
  VERIFY -->|成功 かつ Fake| DEVMODE[dev_mode]
  VERIFY -->|失敗 かつ Fake + InvalidProof| DEVMODE
  VERIFY -->|成功 かつ 非 Fake| SUCCESS[success]
  VERIFY -->|失敗（その他）| FAIL2[failed]

入力形式の解決

検証サービスは単一のレシートファイルだけでなく、レシートを含むバンドルディレクトリや ZIP にも対応しています。image_id はラッパーの top-level フィールドで、レシート本体の内部フィールドではありません。同期ファイナライズ経路では proof bundle ディレクトリ全体を渡し、その中の receipt.json を解決させる実装になっています。

Image ID 照合と Fake receipt の扱い

ラッパーの image_id を期待値と照合し、不一致なら failed として即時拒否します。Image ID の管理は Image ID を参照してください。

レシートの内部構造（InnerReceipt）が Fake 型の場合は開発モードで生成されたレシートですが、即 dev_mode にはなりません。Image ID 不一致なら failed、Image ID 一致時のみ Receipt::verify の結果に応じて dev_mode に振り分けられます。

STARK 検証の実行

Image ID 照合に成功した後、RISC Zero SDK の Receipt::verify(expected_image_id) で STARK 証明を検証します。検証成功は次を保証します。

• レシートに含まれる seal（証明データ）が有効
• ジャーナルが指定 Image ID のゲスト実行結果である
• 証明生成後にレシートが改ざんされていない

検証レポート

検証サービスは、検証が最後まで到達した試行について JSON レポートを出力します。exit code とレポート出力の関係は次のとおりです。

呼び出し側は exit code とレポートの両方を見ます。--quiet を指定すると stdout 出力は抑制されるので、その場合は --output も併せて指定してレポートを保存します。

errors は固定のエラーコード一覧ではなく、実装が積む自由形式の診断文字列です。

ステータスの意味づけ

デプロイメントモデル

検証サービス（Rust バイナリ verifier-service）は、呼び出し経路ごとに実行場所が異なります。詳細は下の「呼び出しパターン」を参照してください。

sequenceDiagram
  participant C as クライアント
  participant API as API サーバー
  participant RUNNER as verifier-service-runner Lambda
  participant VS as verifier-service バイナリ
  participant S3 as S3

  C->>API: POST /api/verification/run
  API->>API: session capability と finalization result を確認
  alt S3 bundle locator がある
    API->>RUNNER: 実行要求（sessionId, executionId, bundleKey, expectedImageId）
    RUNNER->>S3: bundle.zip を取得・展開
    RUNNER->>VS: bundle ディレクトリ + 期待 Image ID + reportPath
    VS->>VS: STARK 検証実行 + verification.json 書き出し
    VS-->>RUNNER: 検証レポート
    RUNNER-->>API: 検証レポート + S3 report locator
  else 信頼済み local bundle がある
    API->>VS: bundle ディレクトリ + 期待 Image ID + reportPath
    VS->>VS: STARK 検証実行 + verification.json 書き出し
    VS-->>API: 検証レポート
  end
  API->>API: verificationResult / execution 状態を更新
  API-->>C: 検証結果

呼び出しパターン

検証サービスの呼び出しには主に 3 つのパターンがあります。明示的検証はいずれも、サーバー側で保持している finalization result に紐付いた 権威ある bundle locator だけを使い、クライアントが任意の S3 キーや local パスを指定して検証させることはできません。

非同期ファイナライズのコールバック Lambda は、結果の復元と保存を担当します。STARK 検証は自動実行されず、POST /api/verification/run で実行します。

verificationResult.status が success / failed / dev_mode のような終端状態にある場合、POST /api/verification/run は再検証せず idempotent な応答を返します。running の場合も実行中として idempotent に扱い、status 未設定または not_run のときだけ verifier-service の実行に進みます。

検証パイプラインにおける役割

検証サービスは、4 段階検証モデルの最終段階である STARK 検証を担当します。

stark_image_id_match は verifier report の expected_image_id と receipt_image_id が一致することを検証します。検証パイプラインはさらに claimed / comparison 側の Image ID とも整合することを確認します。

これらのチェックが両方成功した場合に限り、「STARK Verified」のステータスが付与されます。詳細は 4 段階検証モデル を参照してください。

セキュリティ上の考慮事項

サーバー側検証の信頼境界

検証サービスはサーバー側で実行されるため、クライアントはサーバーの検証結果を信頼する必要があります。この PoC における信頼モデルは以下の通りです:

• STARK 証明自体は秘密データを含まない検証データ: レシートと Image ID があれば、第三者が独立に検証可能
• 検証サービスは利便性のための委任: ブラウザでの STARK 検証が実用的になれば、クライアント側のみで完結させることも理論上は可能
• 配布対象アーカイブ: レシートと public-input.json は ZIP ローカル検証（Ubuntu） の手順で独立検証できる

verification.json の非公開性

verification.json は配布対象アーカイブ bundle.zip には含まれません。必要に応じてレポート用の capability 保護エンドポイント経由で配布されますが、第三者検証ではレシートファイルを直接使った独立検証が推奨されます。

Image ID

ゲストバイナリを一意に識別する Image ID をどう発行し、どう検証で照合するかを扱う章です。

Image ID はゲストプログラムの ELF バイナリから決定的に導出される 256 ビットのハッシュ値です。レシート検証時に期待値との一致を確認することで、正しいプログラムの実行結果であることを保証します。

概要

RISC Zero zkVM では、ゲストプログラムの ELF バイナリが Image ID と呼ばれる 256 ビットの識別子に変換されます。この変換は決定的であり、同一のバイナリからは常に同一の Image ID が生成されます。

Receipt::verify(image_id) はレシートが指定した Image ID のゲスト実行結果であることを暗号学的に検証します。期待する Image ID と一致しないレシートは拒否されます。ラッパーメタデータとの照合手順は 検証サービス を参照してください。

flowchart LR
  ELF["ゲスト ELF バイナリ"] --> HASH["RISC Zero<br/>Image ID 導出"]
  HASH --> IID["Image ID<br/>(256 ビット)"]

  IID --> EMBED["ホストバイナリに埋め込み"]
  IID --> MAP["マッピングファイルに記録"]
  IID --> VS["検証サービスの期待値"]

Image ID の導出

Image ID は RISC Zero のビルドシステムによってコンパイル時に自動生成されます。

決定論的導出

同一のゲストソースコードであっても、以下の要因により異なる Image ID が生成され得ます:

アーキテクチャによる差異

本システムでは、同一バージョンのゲストに対して既定 variant 用 (expectedImageID) と x86_64 用 (expectedImageID_x86_64) の 2 つの Image ID をマッピング上で管理できます。expectedImageID は通常、昇格済みの ARM64/ECS 用 Image ID として扱います。

現行実装では、実行環境の自動判定で x86_64 を選びません。未指定時は default variant として expectedImageID を使い、x86_64 用の値を使うには EXPECTED_IMAGE_ID_VARIANT=x86_64 または呼び出し側の明示 variant で選択します。variant 選択と EXPECTED_IMAGE_ID オーバーライドの優先順位は下の Image ID の解決 を参照してください。

Image ID マッピング

期待される Image ID は、バージョンごとにマッピングファイルで管理されます。

マッピングの構造

マッピングファイルには、各バージョンの Image ID、説明、ビルド情報、機能リストが記録されます。

バージョン履歴の管理

マッピングファイルはバージョンの履歴を保持します。current フィールドが現在有効なバージョンを指し、deprecated フィールドが過去のバージョンを列挙します。current バージョンは既定 variant と x86_64 の 2 系統の Image ID を持ちます。

現行実装では current は 14 で、v8〜v13 が deprecated 側にあります。v14 の mapping は、ECS Fargate で使う正式な既定 variant (expectedImageID) と、ローカル / CI の x86_64 検証で使う expectedImageID_x86_64 を保持します。

flowchart LR
  CUR["current<br/>(ARM64 + x86_64)"]
  DEP["deprecated<br/>(履歴のみ)"]
  CUR -. version up .-> DEP

Image ID の解決

検証時に使用する期待 Image ID は、EXPECTED_IMAGE_ID が設定されているか、methodVersion と variant を使ってマッピングから解決するかで挙動が分かれます。

flowchart TD
  START[Image ID 解決] --> P1{EXPECTED_IMAGE_ID?}
  P1 -->|設定済み| USE1[その値を採用]
  P1 -->|未設定| P2[マッピングから解決]
  P2 --> P3{variant?}
  P3 -->|default| F1[expectedImageID]
  P3 -->|x86_64| F2[expectedImageID_x86_64]
  F1 --> CHK[fail-closed 条件を適用]
  F2 --> CHK

解決ルールの要点:

• EXPECTED_IMAGE_ID 環境変数は最優先のオーバーライドです。
• resolveExpectedImageId() / /api/verification/run の version 選択:
  • 省略時: マッピングの current を使用
  • 明示時: CURRENT_METHOD_VERSION と一致する場合のみ受理。deprecated 側は拒否
• 低レベルのマッピング読み取り API は deprecated も含めて明示 version を解決できる（この検証実行経路では使わない）。
• variant は EXPECTED_IMAGE_ID_VARIANT（default または x86_64）または呼び出し側の明示 option で選択し、未指定時は default。それ以外の値は受け付けません。
• 未対応 methodVersion、マッピング読み込み失敗、選択した variant の値が空、いずれも暗黙のフォールバックを行わず fail-closed でエラーになります。
• 現行の検証実行フローでは、正規化済みのジャーナルから methodVersion を取得して resolveExpectedImageId(methodVersion) を呼びます（public-input.json フォールバックは現行未使用）。

検証パイプラインにおける役割

Image ID は 4 段階検証モデルの STARK 検証段階で使用されます。

Image ID 関連チェック

現行実装では、STARK 検証段階で次の 2 つの必須チェックが Image ID に関与します。

• stark_image_id_match: receipt.json ラッパーの image_id と期待値を照合する
• stark_receipt_verify: 同じ期待 Image ID を使って Receipt::verify(expectedImageID) を実行する

詳細は 検証サービス を参照してください。

Image ID が不一致の場合、以下のいずれかの状況を意味します:

Image ID の更新手順

ゲストプログラムを変更した場合、Image ID を更新する必要があります。

1. ゲストコードを変更する
2. zkVM ゲストをビルドし、host --print-image-id [--json] で新しい Image ID を取得する
3. public/imageId-mapping.json を更新する（必要に応じて expectedImageID_x86_64 も更新）
4. 関連コードに残る定数参照も必要に応じて更新する（現行実装では src/lib/verification/expected-image-id.ts の DEFAULT_POC_IMAGE_ID がテストなどで参照される）
5. プローバーイメージとマッピングを同時にデプロイする

--json を付けると {"imageId":"0x...","methodVersion":14} の形で出力されます。CodeBuild は ARM64 prover image のビルド後にこの JSON を取得し、imageId と methodVersion を image metadata として記録します。

更新の同期要件

プローバーイメージと imageId-mapping.json は同一リリースで切り替えます。片方だけが新しい場合は検証時に Image ID 不一致で失敗します。

• 通常の /api/verification/run フローでは、現行の journal contract のみ受け付ける
• 旧成果物は Image ID 照合に進む前に、未対応の journal contract として失敗し得る
• DEFAULT_POC_IMAGE_ID はテスト用定数で、期待 Image ID の解決経路には現れない（マッピングが source of truth）

セキュリティ上の位置づけ

Image ID は、zkVM の信頼モデルにおける重要な信頼アンカーです。

• Image ID を知っている検証者は、ゲストプログラムのロジックを信頼できる: レシートが有効であれば、そのロジックが正しく実行されたことが保証される
• Image ID の管理が破綻すると、検証の信頼性が失われる: 攻撃者が独自のゲストプログラムで有効なレシートを生成し、その Image ID がマッピングに混入すると、不正な集計が「検証済み」として受理される

マッピングファイルは公開リポジトリにコミットされ、変更履歴が追跡可能です。AWS 構成では、イメージ署名検証と組み合わせることで、承認されたプローバーイメージのみが使用されることを保証しています。イメージ署名の詳細は イメージ署名 を参照してください。

検証パイプライン

投票の完全性を 4 段階に分けて検証するパイプラインを扱う部です。

この部に含まれる章

• 設計と実行フロー — 設計原則、パイプライン構造、実行フロー
• 4 段階検証モデル — 検証の全体設計と各段階の保証
• チェック一覧 — 全検証チェック ID とその判定ロジック
• バンドル構造 — 証明バンドルの公開可能・非公開アーティファクト
• ゲーティングロジック — 「Verified」表示の条件と不変条件

想定読者と前提

• 想定読者: /verify 画面の最終判定ロジックを把握したい監査者・実装者
• 前提: 暗号プロトコル と zkVM 設計 の概要を読み終えていること

本章で扱わないもの

• bundle.zip のローカル監査手順（第三者検証ガイド を参照）
• 改ざんシナリオごとの検出表（改ざんシナリオ を参照）
• UI コンポーネントや Storybook 配置の詳細

関連する章

• 暗号プロトコル — チェック対象となるプリミティブ
• zkVM 設計 — ジャーナルとレシートの構造
• 改ざんシナリオ — どのチェックがどの改ざんを検出するか
• 第三者検証ガイド — bundle.zip を使ったローカル監査
• 用語集 — チェック種別・ゲーティング用語の定義

設計と実行フロー

検証パイプラインの設計原則と、リクエストから判定までの実行フローを扱う章です。

設計原則

本システムの検証パイプラインは、以下の 3 つの原則に基づいて設計されています。

原則 1: 必要な検証が未実行なら Verified を表示しない

required チェックが not_run（未実行）、pending（依存待ち）、running（実行中）のいずれかにある場合、システムは「Verified」を表示しません。証拠の不在や未解決状態を成功として扱わないという姿勢です。

原則 2: 失敗した検証は即座にブロックする

いずれかの必須チェックが失敗すれば、「Verified」表示は即座にブロックされます。代表的な失敗条件:

• excludedSlots > 0（除外されたスロットが存在する）
• 整合性証明の失敗
• 公開監査アーティファクトとの不一致
• 第三者 STH 合意の不成立（設定時）

原則 3: チェック評価はサーバー中心、集約はサーバーとクライアントの双方で実施

• GET /api/verify は 22 チェックのレスポンスを組み立てます。サーバーは Stage 2-4 の 18 チェックを評価し、Cast-as-Intended の 4 チェックは not_run で返したうえで、クライアントがローカル再評価で上書きします。
• Recorded-as-Cast は cast-time 証跡（voteReceipt と userVote.proof）を前提とします。store から再構成できない場合でも /api/verify は 200 を返し、関連チェックを not_run にして全体判定を missing_evidence 側へ fail-closed に倒します。
• STARK 検証は専用サービス（POST /api/verification/run）で実行され、GET /api/verify がその結果を読み取ります。
• deriveVerificationSummary はサーバー側の /api/verify とクライアント側の /verify の両方で使われます。
• サーバーは verificationStatus を fail-closed に補正します。unsupported な verifier status でも verificationSteps / verificationChecks を含む 200 応答を返します。
• クライアントの最終判定は、明示的な STARK/server failure、hard-failure チェックの override、summary tone、pending state を優先順に解決します。UI 側の補助分岐については ゲーティングロジック を参照してください。

必要なデータ（userVote.proof.treeSize、journal など）が不在のときの not_run 補正など、ステップ status のガード条件の詳細は ゲーティングロジック を参照してください。

検証パイプラインの全体構造

1. 段階の依存関係

1. Stage 1 — Cast-as-Intended
2. Stage 2 — Recorded-as-Cast
3. Stage 3 — Counted-as-Recorded
4. Stage 4 — STARK Verification
5. 結果表示

2. 実行責務（どこで評価・検証されるか）

flowchart TD
  subgraph SERVER["サーバー側"]
    VFY["GET /api/verify<br/>Stage 2-4 を評価<br/>Cast は not_run（クライアント再評価）"]
    RUN["POST /api/verification/run<br/>bundle 参照と expected Image ID で<br/>Stage 4 を検証"]
  end

  subgraph CLIENT["クライアント（UI）"]
    UI["Cast のローカル再評価<br/>STARK 解決後に step 表示を開始<br/>明示的 failure / hard-failure override / summary / pending を反映"]
  end

  VFY --> UI
  RUN --> UI

検証の実行フロー

検証導線では通常 /result から /verify へ進みます。

1. /result は正準な finalization snapshot をクライアント状態に保存します。「検証へ進む」を押すと verificationRequestedAt を保存し、必要なら POST /api/verification/run を非同期に先行起動します（完了を待たずに /verify へ遷移します）
2. /verify はその継続状態がある場合に検証シーケンスを続行します。STARK が未開始ならシーケンス内で起動できます
3. 継続状態がなく STARK が not_run のまま直接 /verify へアクセスした場合は、自動続行せずブロックします
4. /verify の UI シーケンスは、step を順に見せる前に STARK が terminal status に到達するまでポーリングします。timeout や transport failure は STARK failure として扱われます

sequenceDiagram
  participant U as ブラウザ
  participant R as /result
  participant V as /verify
  participant A as API サーバー
  participant VS as 検証サービス

  Note over R: finalization snapshot は /result 表示時に保存済み
  U->>R: 「検証へ進む」をクリック
  R->>R: verificationRequestedAt を保存
  R->>A: POST /api/verification/run（fire-and-forget）
  R-->>V: /verify へ遷移（run 完了は待たない）

  Note over V: /verify 到達時に未開始なら<br/>同じ POST /api/verification/run を起動

  A->>VS: bundle 参照 + expected Image ID
  VS->>VS: Receipt::verify(imageId)
  VS-->>A: 検証レポート保存

  loop STARK 完了までポーリング
    V->>A: GET /api/verify
    A-->>V: 検証ペイロード<br/>(ステップ, チェック, 証明材料)
  end

  Note over V: 継続には verificationRequestedAt と finalization snapshot が必要<br/>not_run の direct access はブロック<br/>step 表示は STARK 解決後に開始

4 段階の概要

各ステージの導出ルール（required チェック群からの集約、STH source 設定時の昇格、ガード条件）は ゲーティングロジック を参照してください。

各段階の詳細は 4 段階検証モデル を参照してください。

検証チェック数

パイプライン全体で 22 個の検証チェックが定義されており、各チェックには一意の ID が割り当てられています。チェック ID の単一ソースは src/lib/verification/verification-checks.ts です。

Counted-as-Recorded の required には counted_election_manifest_consistent と counted_close_statement_consistent も含まれ、公開された election-manifest.json / close-statement.json との整合が stage success の条件に入ります。チェック詳細は チェック一覧 を参照してください。

4 段階検証モデル

E2E 検証可能投票の各段階（Cast-as-Intended / Recorded-as-Cast / Counted-as-Recorded / STARK Verification）でどんな保証が成り立つかを扱う章です。

段階間の依存関係

概念モデルとしては 4 段階を順に評価しますが、実行場所は段階ごとに異なります（Stage 1 はクライアント、Stage 2-4 はサーバー中心）。実行責務の詳細は 設計と実行フロー を参照してください。

flowchart LR
  subgraph "証拠の生成"
    V["投票時<br/>投票レシート発行"]
    F["集計時<br/>zkVM 実行"]
  end

  subgraph "4 段階検証"
    S1["Stage 1<br/>Cast-as-Intended"]
    S2["Stage 2<br/>Recorded-as-Cast"]
    S3["Stage 3<br/>Counted-as-Recorded"]
    S4["Stage 4<br/>STARK Verification"]
  end

  V --> S1
  V --> S2
  F --> S3
  F --> S4

  S1 ~~~ S2
  S2 ~~~ S3
  S3 ~~~ S4

Stage 1: Cast-as-Intended

目的

投票者が意図した選択肢のコミットメントが、サーバーから返却された投票レシートと一致することを確認します。これにより、サーバーが投票者の選択を差し替える攻撃を検出します。

検証する内容

/verify 画面のクライアントコードがローカルに保持された 3 つの値（選挙 ID、選択肢、乱数）からコミットメントを再計算し、投票レシートのコミットメント値と照合します。

flowchart LR
  subgraph "投票時に確定したデータ"
    EID[選挙 ID]
    CH[選択肢]
    RND[乱数]
  end

  subgraph "再計算"
    HASH["SHA-256<br/>(ドメインタグ || 選挙ID || 選択肢 || 乱数)"]
  end

  subgraph "照合"
    CMP{"一致?"}
    REC[投票レシートの<br/>コミットメント]
  end

  EID --> HASH
  CH --> HASH
  RND --> HASH
  HASH --> CMP
  REC --> CMP

必要な証拠

voteReceipt は cast-time 証跡が再構成できた場合のみ返されます（設計原則 3 参照）。

失敗モード

限界

この段階は投票者の手元データに依存するため、localStorage 消去後や別端末からは検証できません。

Stage 2: Recorded-as-Cast

目的

投票者のコミットメントが、追記専用の掲示板（CT Merkle ツリー）に正しく記録されていることを確認します。さらに、掲示板が追記専用性を維持していること（過去のエントリが削除・改変されていないこと）を検証します。

検証する内容

この段階には 3 系統の検証があります。UI ステップとの対応関係は ゲーティングロジック を参照してください。

flowchart TB
  subgraph "2a: 包含証明"
    IP["包含証明の検証<br/>自分のコミットメントが<br/>ツリーに存在するか"]
  end

  subgraph "2b: 整合性証明"
    CP["整合性証明の検証<br/>投票時のルートから<br/>最終ルートへの追記専用性"]
  end

  subgraph "2c: 第三者 STH 検証"
    STH["STH 合意の検証<br/>独立したソース間で<br/>ツリー状態が一致するか"]
  end

  IP --> RESULT{"Recorded 系の証拠を総合評価"}
  CP --> RESULT
  STH --> RESULT

2a: 包含証明（Inclusion Proof）

RFC 6962 の PATH 関数に基づく CT スタイルの Merkle 包含証明を検証し、投票者のコミットメントが掲示板のツリーに含まれていることを確認します。検証者はリーフハッシュと監査パスからルートハッシュを再計算し、期待されるルートと照合します。

2b: 整合性証明（Consistency Proof）

投票時点のツリー状態（ルートとサイズ）から、最終的なツリー状態への遷移が追記のみで行われたことを検証します。RFC 6962 の SUBPROOF アルゴリズムに基づく整合性証明により、サーバーが過去のエントリを密かに削除したり順序を変更したりするスプリットビュー攻撃を検出します。

2c: 第三者 STH 検証（オプション）

複数の独立した STH（Signed Tree Head）ソースに問い合わせ、合意が成立しているかを確認します。これにより、サーバーが検証者ごとに異なるツリー状態を提示するスプリットビュー攻撃を検出します。照合条件の詳細は チェック一覧 を参照してください。

必要な証拠

userVote.proof.treeSize は整合性証明の oldSize として参照されます。

関連: fail-closed（cast-time 証跡が欠ける場合の動作） / 設計原則 3 / チェック一覧（判定の詳細）。

失敗モード

Stage 3: Counted-as-Recorded

目的

掲示板に記録された全投票が、zkVM の集計処理に正しく含まれたことを確認します。投票の除外、欠落、重複がないことに加え、公開された claimed tally（表示用集計値）が zkVM の verifiedTally と一致することを検証し、集計結果の完全性と整合性を保証します。

検証する内容

この段階では 10 個の required チェックが全て success であることを要求します。導出ルールと journal 省略時のガード補正は ゲーティングロジック を参照してください。

flowchart TD
  subgraph PUBLIC["public 系 required (6)"]
    P["counted_input_sanity<br/>counted_unique_indices<br/>counted_unique_<br/>commitments<br/>counted_election_<br/>manifest_consistent<br/>counted_close_<br/>statement_consistent<br/>counted_input_<br/>commitment_match"]
  end

  subgraph ZK["zk 系 required (4)"]
    Z["counted_tally_consistent<br/>counted_missing_<br/>indices_zero<br/>counted_expected_<br/>vs_tree_size<br/>counted_my_vote_<br/>included"]
  end

  RESULT{"10 required 全て success?"}
  PASS["Counted: success"]
  FAIL["Verified をブロック"]

  P --> RESULT
  Z --> RESULT
  RESULT -->|Yes| PASS
  RESULT -->|No| FAIL

必要な証拠

公開入力サマリーはサーバー内部表現であり、レスポンスにそのまま含まれません。inputCommitment が束縛するのは public-input.json の部分集合です。各チェックの判定ロジックは チェック一覧 を参照してください。

重要な判定: 除外数（excludedSlots）

excludedSlots は authoritative な公開除外数です。

• excludedSlots == 0: 除外なし（正常）
• excludedSlots > 0: 掲示板スロットの未提示または計上失敗（即座に検証失敗）

counted_missing_indices_zero が除外数を解決し、0 でなければ failed になります。解決順序と legacy aliases の扱いは チェック一覧 を参照してください。

失敗モード

Stage 4: STARK Verification

目的

zkVM の実行が正しく行われたことを STARK 証明（レシート）の暗号学的検証により確認します。レシートの検証に成功すれば、ジャーナルの内容（集計結果、除外情報、入力コミットメント等）がゲストプログラムの正しい実行の結果であることが保証されます。

検証する内容

flowchart LR
  subgraph "入力"
    RCP[レシート<br/>Seal + Journal]
    EID[期待 Image ID]
  end

  subgraph "Rust 検証サービス"
    VF["Receipt::verify(imageId)"]
  end

  subgraph "結果"
    OK["success<br/>暗号学的に検証済み"]
    NG["failed<br/>証明が無効"]
    DM["dev_mode<br/>フェイクレシート"]
  end

  RCP --> VF
  EID --> VF
  VF --> OK
  VF --> NG
  VF --> DM

検証の 2 段階

STARK Verification では 2 つのチェックを実行します。

Image ID 照合: verifier-confirmed な receipt_image_id が期待 Image ID と一致し、ホスト主張値（imageId）や comparison-only の journal.imageId とも矛盾しないことを確認します。Image ID はゲストプログラムから導出される暗号的識別子であり、プログラムの改変やホスト主張値の食い違いを検出します。解決順の詳細は チェック一覧 を参照してください。

レシート検証: RISC Zero の Receipt::verify() を呼び出し、Seal（STARK 証明）がジャーナルと Image ID に対して暗号学的に正当であることを検証します。この検証は計算量が多いため、サーバー側の Rust 検証サービスで実行されます。

必要な証拠

開発モードの検出

RISC0_DEV_MODE=1 で生成されたレシートは InnerReceipt::Fake 型であり、暗号学的な保証を持たず、本番 STARK 検証としては受理されません。検証サービスはこれを dev_mode ステータスとして報告し、core evaluator では明示的な dev-mode allowance が有効な場合だけ success に正規化し、それ以外では not_run として扱います。判定の詳細は ゲーティングロジック を参照してください。

失敗モード

UI ステップの対応チェック、集約ルール、最終判定の決定方法は ゲーティングロジック を参照してください。

チェック一覧

全検証チェック ID の定義、判定ロジック、失敗時の影響を一覧で解説します。

各チェックは一意の ID を持ち、success / failed / not_run / running / pending のステータスで管理されます。required チェックが not_run / running / pending のまま残っている場合、「Verified」は表示されません。optional チェックの取り扱いは ゲーティングロジック を参照してください。

チェックの属性

各チェックには以下の属性が定義されています。

証拠種別

現行 22 チェックで使う証拠種別です。

重要度

代表例は recorded_sth_third_party です。

注意: verificationChecks と UI 表示用の verificationSteps は 1 対 1 ではありません。対応関係は ゲーティングロジック を参照してください。

Cast-as-Intended（4 チェック）

投票者の意図通りにコミットメントが生成されたかを検証するチェック群です。 このカテゴリはクライアントが voteReceipt（/api/verify 応答）とローカル投票意図（electionId/myVote/myRand）を使って評価します。

判定ロジックの詳細

cast_receipt_present

voteReceipt が存在し、voteId と commitment フィールドが存在することを確認します（このチェック単体では UUID/hex 形式までは検証しません）。

cast_choice_range

投票時データの選択肢が A〜E のいずれかであることを確認します。範囲外の値は不正な入力として failed となります。

cast_random_format

投票時データの乱数が 32 バイト（64 文字）の 16 進数文字列であることを確認します。0x プレフィックスの有無は正規化により吸収されます。

cast_commitment_match

投票時データから再計算した投票コミットメントが投票レシートの commitment 値と一致することを確認します。再計算規則（ドメインタグ・正準フォーマット）は コミットメントスキーム を参照してください。

Recorded-as-Cast（6 チェック）

コミットメントが掲示板に正しく記録されたかを検証するチェック群です。

判定ロジックの詳細

recorded_inclusion_proof と recorded_consistency_proof は cast-time 証跡（voteReceipt と userVote.proof）の存在を前提とし、まず cast snapshot の一貫性（leafIndex、treeSize、bulletinRootAtCast が receipt と矛盾しないこと）を確認してから個別の検証に進みます。証跡が揃わない場合はどちらも not_run となり、全体判定は fail-closed で missing_evidence 側へ倒れます。

recorded_commitment_in_bulletin

包含証明（recorded_inclusion_proof）の結果から派生します。包含証明が成功すれば、コミットメントがツリーに存在することが暗号学的に証明されています。

recorded_index_in_range

掲示板インデックスが 0 <= index < treeSize の範囲内であることを確認します。範囲外のインデックスは、データの不整合を示します。

recorded_root_at_cast_consistent

整合性証明（recorded_consistency_proof）の結果から派生します。整合性証明が成功すれば、投票時のルートが最終ツリーの有効な追記専用プレフィックスであることが証明されています。

recorded_inclusion_proof

投票者のコミットメントに対する RFC 6962 包含証明（監査パス）を検証します。リーフハッシュと監査パスから cast 時点のルートを再計算し、receipt の bulletinRootAtCast と一致することを確認します。proof の treeSize が voteReceipt.bulletinIndex + 1 と一致しない場合は failed です。

recorded_consistency_proof

投票時のツリー（oldSize, oldRoot）から最終ツリー（newSize, newRoot）への RFC 6962 整合性証明を検証します。bulletin provider から取得した old/new 両時点の root が期待値と一致することを確認し、投票時ルートが最終ツリーの追記専用プレフィックスであることを保証します。treeSize チェックは包含証明と同条件です。

recorded_sth_third_party

設定された STH ソースからスナップショットを取得し、比較可能な応答同士で合意を確認します。判定は matchingSources >= minMatches（デフォルト: 2）に加えて、比較対象になった応答間の全会一致（consensus）が必要です。照合対象は STH ダイジェストが必須で、bulletinRoot / treeSize は各ソースが返した場合に追加で照合されます。STH ソースが未設定の場合は not_run になります。

早見表では optional ですが、STH ソース設定時は required 相当に昇格します。詳細は ゲーティングロジック を参照してください。

Counted-as-Recorded（10 チェック）

記録された全投票が正しく集計に含まれたかを検証するチェック群です。

判定ロジックの詳細

counted_input_sanity

public-input.json 相当から組み立てた公開入力サマリーが存在し、スキーマ検証に成功していることを確認します。加えて、treeSize が正の整数、votesCount <= treeSize、bulletinRoot が 32 バイト hex かつゼロ値でないことを要求します。

counted_unique_indices

zkVM に渡された全投票のインデックスが重複なく一意であることを確認します。重複インデックスは、同一投票の二重カウントを示す可能性があります。

counted_unique_commitments

zkVM に渡された全投票のコミットメントが重複なく一意であることを確認します。重複コミットメントは、同一コミットメントに対する複数投票を示す可能性があります。

counted_tally_consistent

主経路では、公開される claimed tally（tally.counts）が zkVM の verifiedTally と選択肢ごとに一致し、かつ verifiedTally の合計が tally.totalVotes と一致することを確認します。これにより「公開表示された集計値」と「zkVM が証明した集計値」の不一致を検出します。claimed tally が利用できない場合は、フォールバックとして journal.verifiedTally の合計と journal.validVotes の一致を検証します。

counted_missing_indices_zero

fail-closed（安全側に倒す）な除外数が 0 であることを確認します。除外数は次の優先順で解決し、0 でなければ即座に failed とします。

1. journal がある場合: journal.excludedSlots を proof-bound な除外数として使用。excludedSlots / missingSlots / invalidPresentedSlots / validVotes が非負整数であることも先に確認する
2. journal がない場合: excludedSlots → missingSlots + invalidPresentedSlots の順で探索

rejectedRecords は説明用の補助値で、この判定には使いません。旧フィールド (excludedCount / missingIndices / invalidIndices) は fail-closed 補正経路でのみ参照され、本判定では使用しません。

counted_expected_vs_tree_size

totalExpected（期待される投票数）が掲示板のツリーサイズと一致することを確認します。不一致は、暗黙の投票除外を示す可能性があります。

counted_election_manifest_consistent

election-manifest.json の electionConfigHash を再計算し、manifest 自身の宣言値と一致することを確認します。そのうえで electionId と electionConfigHash を、セッション値・publicInputArtifact から導出した内部 publicInputSummary・ジャーナルに含まれる対応値と相互照合します。

counted_close_statement_consistent

close-statement.json から sthDigest を再計算し、宣言された snapshot と一致することを確認します。そのうえで timestamp が publicInputArtifact から導出した内部 publicInputSummary.timestamp と一致し、logId / treeSize / bulletinRoot / sthDigest が検証入力やジャーナルと矛盾しないことを確認します。

counted_my_vote_included

includedBitmapRoot に対する bitmap Merkle 証明を検証し、投票者のインデックスに対応するビットが 1（counted に含まれた）であることを確認します。

seenBitmapRoot もある場合は /api/bitmap-proof?kind=included|seen の両方を使い、presented but invalid / not presented to the prover / unknown excluded を説明可能にします。

証明材料が取得できない場合は not_run になり、補助 note が付くことがあります。

counted_input_commitment_match

公開入力から再構成した入力コミットメントが、zkVM ジャーナルの値と一致することを確認します。対象フィールドの集合と正準エンコーディングは 入力コミットメント を参照してください（public-input.json 全体の単純なハッシュではない点に注意）。

STARK Verification（2 チェック）

STARK 証明の暗号学的正当性を検証するチェック群です。

判定ロジックの詳細

stark_image_id_match

STARK status が success に解決された後で、期待 Image ID・verifier-confirmed Image ID・ホスト主張値が相互に矛盾しないことを確認します。整合条件（report に Image ID フィールドが揃わない場合の挙動を含む）と fail-closed の取り扱いは Image ID を参照してください。

期待 Image ID の解決順:

variant は EXPECTED_IMAGE_ID_VARIANT（default または x86_64）で明示指定します（未指定時は default）。

stark_receipt_verify

サーバー側の Rust 検証サービスが Receipt::verify(image_id) を実行し、Seal（STARK 証明）が暗号学的に正当であることを確認します。チェック結果は success / failed / not_run / running で表現され、dev_mode は ゲーティングロジック に従って正規化されます。

チェックステータスの遷移

stateDiagram-v2
  [*] --> not_run: 初期状態
  not_run --> pending: 依存条件の待機
  not_run --> running: 検証開始
  pending --> running: 依存条件の解消
  running --> success: 検証成功
  running --> failed: 検証失敗

全体判定（集約結果）の決まり方は ゲーティングロジック を参照してください。

全チェック早見表

バンドル構造

証明バンドルの内訳と公開許可リスト、同期・非同期それぞれのモードでの差分を扱う章です。

概要

証明バンドル は、zkVM の実行結果を検証可能な形で保存・配布するためのアーティファクト群です。実際に配布される bundle.zip は、厳格な許可リストによって公開可能アーティファクトだけを含める配布対象アーカイブです。

本書で public / 「公開可能」と記述する場合、秘密情報を含まず第三者検証に利用可能であるという機密性の分類を指します。無認証で誰でも取得できるという意味ではなく、アクセス経路は バンドルのアクセス方法 を参照してください。

bundle.zip 自体は監査用成果物であり、/verify 画面の最終判定を単体で完全再現することは目的としていません。UI 最終判定に必要な追加材料は 第三者検証ガイド を参照してください。

flowchart TB
  subgraph "バンドルディレクトリ"
    subgraph "公開可能アーティファクト"
      PI["public-input.json<br/>公開入力"]
      EM["election-manifest.json<br/>選挙マニフェスト"]
      CS["close-statement.json<br/>締切ステートメント"]
      RC["receipt.json<br/>STARK レシート"]
      JN["journal.json<br/>zkVM ジャーナル"]
      MT["metadata.json<br/>メタデータ（syncのみ）"]
      STH["sth.json<br/>STH スナップショット"]
      CP["consistency-proof.json<br/>整合性証明"]
    end

    subgraph "非公開アーティファクト"
      IN["input.json<br/>秘匿入力（ウィットネス）"]
      VR["verification.json<br/>検証レポート"]
      IB["included-bitmap.json<br/>厳密 counted bitmap"]
      SB["seen-bitmap.json<br/>厳密 presented bitmap"]
    end

    BZ["bundle.zip<br/>配布対象アーカイブ"]
  end

  PI --> BZ
  EM --> BZ
  CS --> BZ
  RC --> BZ
  JN --> BZ
  MT --> BZ
  STH -.-> BZ
  CP -.-> BZ
  IN -.-x BZ
  VR -.-x BZ
  IB -.-x BZ
  SB -.-x BZ

公開許可リスト

バンドルアーカイブ（bundle.zip）に含められるファイルは、許可リストによって厳格に制限されています。

公開可能なアーティファクト

sth.json と consistency-proof.json は許可リストに含まれますが、現行フローでは通常生成されません。

非公開アーティファクト

input.json が公開されると投票の秘匿性が失われます。verification.json は必要時のみ専用の capability 保護エンドポイント経由で扱います。included-bitmap.json と seen-bitmap.json は /api/bitmap-proof の trusted source ですが、配布対象アーカイブ bundle.zip には含めません。

公開入力の構造

public-input.json は、第三者検証に必要で、かつ選択肢と乱数を含まない入力側レコードです。input.json の単純なサブセットではありません。

votes 配列には各投票のインデックスとコミットメント、Merkle パスが含まれますが、選択肢と乱数は含まれません。これにより、入力コミットメントの再計算が可能でありながら、投票内容の秘匿性は維持されます。

public-input.json と inputCommitment は同一ではなく、後者が直接束縛するのはこのレコードの一部です。計算対象フィールドと非対象フィールドの整理は 入力コミットメント を参照してください。

同期バンドルと非同期バンドルの違い

証明生成には 2 つのパスがあります。同期モード はローカルプロセス / Lambda 上で TypeScript がアーティファクトを生成し、検証サービスから戻った verification.json を含めて bundle.zip を作成します。非同期モード は ECS Fargate コンテナの entrypoint.sh が公開可能アーティファクトを生成し、bundle.zip を S3 に置いた後コールバック Lambda がセッションに結果を反映します。両モードとも、public-input.json / election-manifest.json / close-statement.json は journal.json と正準な proof-bound data との整合性検査を通過した場合にのみ bundle 化されます。不一致があれば fail-closed で処理を中断します。

非同期バンドルの生成フロー

非同期モードでは、ECS Fargate コンテナの entrypoint.sh が以下の手順でバンドルを構築します。

1. S3 から入力 JSON をダウンロード
2. ホストバイナリを実行し、レシートと出力を生成
3. 出力から journal.json を変換生成
4. 入力と出力から public-input.json、election-manifest.json、close-statement.json を構築
5. 整合性検査（本節冒頭参照）を通過したものだけを bundle に含める
6. receipt.json、journal.json、public-input.json、election-manifest.json、close-statement.json を bundle.zip にアーカイブ
7. *-receipt.json / *-output.json / public-input.json / election-manifest.json / close-statement.json / included-bitmap.json / seen-bitmap.json / bundle.zip などを S3 にアップロード

コールバック Lambda は S3 の bundle.zip からジャーナル、レシート、public-input.json、election-manifest.json、close-statement.json を復元します。利用可能な場合は隣接オブジェクトの bitmap artifact も取り込み、presigned URL の生成と監査用データの保存を行います。

docker/entrypoint.sh は methodVersion 14 のホスト出力を検証し、journal.json / public-input.json / election-manifest.json / close-statement.json の methodVersion と inputCommitment が一致することを確認してから bundle.zip を生成します。methodVersion が現行契約と一致しない出力は fail-closed で停止します。

バンドルディレクトリ構造

同期モード（ローカルファイルシステム）

{VERIFIER_WORK_DIR}/
  {sessionId}/
    {executionId}/
      input.json               ← 非公開: ウィットネス
      public-input.json        ← 公開可能
      election-manifest.json   ← 公開可能
      close-statement.json     ← 公開可能
      journal.json             ← 公開可能
      receipt.json             ← 公開可能
      metadata.json            ← 公開可能
      included-bitmap.json     ← 非公開: 厳密 counted bitmap artifact
      seen-bitmap.json         ← 非公開: 厳密 presented bitmap artifact
      verification.json        ← 非公開: 検証レポート
      bundle.zip               ← 配布対象: 許可リストファイルのアーカイブ

非同期モード（S3）

s3://{BUCKET}/sessions/{sessionId}/{executionId}/
  input.json                 ← 非公開: ワーク入力
  {inputBase}-receipt.json   ← ホストの生出力
  {inputBase}-output.json    ← ホストの生出力
  {inputBase}-journal.json   ← ホストが生成した場合のみ
  public-input.json          ← 公開可能
  election-manifest.json     ← 公開可能
  close-statement.json       ← 公開可能
  included-bitmap.json       ← 非公開: 厳密 counted bitmap artifact
  seen-bitmap.json           ← 非公開: 厳密 presented bitmap artifact
  bundle.zip                 ← 配布対象: 内部は receipt.json / journal.json / public-input.json / election-manifest.json / close-statement.json
  verification.json          ← `/api/verification/run` 後に参照可能になる場合あり（非公開）

補足

• 非同期モードの S3 オブジェクト名は固定の receipt.json / journal.json になりません。inputBase がコンテナ実行時に生成される一時入力ファイル名に依存するためです。
• 非同期モードの verification.json は bundle.zip の構成要素ではなく、report エンドポイントから参照する別アーティファクトです。S3 上の report がこのセッションの配信対象として記録されていれば短命な presigned URL にリダイレクトされ、未記録ならローカル report を探し、いずれもなければ 404 を返します。

バンドルのアクセス方法

ダウンロードエンドポイント

両エンドポイントとも X-Session-Capability ヘッダーが必須です。つまり、ダウンロードは capability 保護 API から開始されます。

加えて、executionId はそのセッションで現在許可されている verificationExecutionId と一致しなければなりません。不一致や未設定の場合、API は 404 を返します。

S3 バンドルは capability 保護済みのダウンロードエンドポイント経由でのみ配布されます。エンドポイントは現在の verificationExecutionId と S3 key を確認したうえで、そのつど短命な presigned URL にリダイレクトします。

アーカイブの再現性

同期モード（verification-bundle.ts）の bundle.zip は再現性を確保するため、以下の措置を講じています。

• エントリのタイムスタンプをゼロに固定
• 許可リストに一致するファイルのみを含める
• ファイル名のアルファベット順でエントリを追加

非同期モード（docker/entrypoint.sh）は zip -r で作成され、上記の再現性制御とは実装が異なります。

セキュリティ上の制約

パストラバーサル防止

バンドルのパスセグメント（セッション ID、実行 ID）は英数字とハイフンのみに制限されています。.. を含むパスや許可されていない文字を含むパスは拒否されます。

非公開ファイルの保護

input.json、verification.json、included-bitmap.json、seen-bitmap.json は bundle.zip には含まれません。

ゲーティングロジック

「Verified」を表示してよい条件と、表示を必ず阻止する不変条件を厳密に並べる章です。

「必要な検証が未実行または失敗なら Verified を表示しない」という原則のもと、各チェックの結果がどう最終判定に集約されるかを定式化します。

最終判定の種類

検証パイプラインの結果は、主経路では deriveVerificationSummary によって集約され、UI 上は以下の 3 トーンに整理されます。なお /verify ページには STARK タイムアウト時の失敗表示など、集約結果に対する限定的な上書きもあります。

ステータスの判定順序

この表は deriveVerificationSummary の集約結果です。チェックが空、または未知チェックだけで既知チェックが 1 件も解決できない場合、summary は null になり、Verified ではなく最終サマリー未表示として扱われます。

現行 /verify ページでは、pending / running のチェックが残っている間は最終サマリー自体を表示せず、ステップ表示が完了したあとに summary を表示します。UI レベルの最終表示は (1) 明示的なサーバー失敗、(2) hard-failure fallback、(3) summary、(4) pending warning の順で解決されます。

補助判定のゲーティング（validateVotingIntegrity）

現行 /verify の最終判定では使われない内部 helper ですが、整合性証明・完全性・第三者 STH 合意・ユーザーインデックス範囲を順に評価し、いずれかが失敗すれば canShowVerified = false を返します。意味論は チェック一覧 の recorded_consistency_proof / counted_missing_indices_zero / counted_expected_vs_tree_size / recorded_sth_third_party に対応します。

STARK 検証のゲーティング

STARK 検証は整合性検証とは独立に評価されます。

STARK が not_run のまま最終判定が Verified になる経路はありません（整合性チェックだけでは Verified に到達できません）。

zkGate: STARK 結果に基づく Counted チェックの制御

STARK 検証の結果は、Counted-as-Recorded 段階のチェック評価にも影響します。これを zkGate と呼びます。

core evaluator では、dev_mode は事前に success または not_run に正規化されてから zkGate に入力されます。一方、現行 /api/verify の表示用ステータス組み立てでは、dev mode が許可されていない場合は fail-closed の failed として反映されます。

ステップとチェックの対応関係

UI に表示される 4 つのステップは、現行実装では 22 個のチェック定義から派生します。

ただし、verificationSteps[].status は「その stage で required 扱いになるチェック群」から導出され、verificationSteps[].inputs は stage 内の 全チェック定義 から集約されます。

補足:

• recorded_commitment_in_bulletin は recorded_inclusion_proof から、recorded_root_at_cast_consistent は recorded_consistency_proof から導出される表示用チェックです。チェック一覧には現れますが、単独では step status を決定しません。
• recorded_sth_third_party は通常は optional ですが、STH source が設定されている場合だけ required に昇格し、Recorded-as-Cast の step status と最終判定をブロックし得ます。

ステップのステータスは、required 扱いになったチェックのステータスから次の順序で集約されます。

さらに現行実装には、単純集約だけではない 3 つの補正があります。

• counted_as_recorded は journal が存在しない場合、required チェックに failed がない限り not_run に補正されます。
• recorded_as_cast は userVote.proof.treeSize がない場合、not_run に補正されます。
• /api/verify は castSource='client' で verificationSteps / verificationChecks を組み立てるため、API 応答上の Cast-as-Intended はいったん not_run です。その後ブラウザ側で保存済みセッション情報から Cast チェックを再評価して上書きし、最終的な UI 表示と summary にはそのローカル結果が反映されます。

UI シーケンスとポーリング

検証ページでは、4 つのステップが順次アニメーション表示されます。

sequenceDiagram
  participant U as ブラウザ
  participant S as サーバー

  Note over U: ページロード時
  U->>S: GET /api/verify
  S-->>U: 検証ペイロード

  Note over U: STARK 完了まで待機

  alt verificationStatus = not_run
    U->>S: POST /api/verification/run
    S-->>U: 実行受付
  end

  loop STARK ポーリング
    U->>S: GET /api/verify
    S-->>U: verificationStatus 確認
  end

  Note over U: STARK 解決後に<br/>ステップを順次表示

  Note over U: Step 1: Cast-as-Intended
  Note over U: Step 2: Recorded-as-Cast
  Note over U: Step 3: Counted-as-Recorded
  Note over U: Step 4: STARK Verification

  Note over U: 最終判定を表示

不変条件のまとめ

以下の不変条件は、コードの変更によっても決して緩和してはなりません。

これらの不変条件は、改ざんシナリオ（S0〜S5）の検出を保証する基盤です。各シナリオがどの不変条件によって検出されるかは、改ざんシナリオ を参照してください。

この fail-closed モデルは、単体・結合・E2E テスト で「Verified を誤表示しない」ケースを継続的に検査しています。形式化側では Lean による形式化 の verification summary / display vectors を通じて、モデルと実装の対応を確認します。

改ざんシナリオ

STARK Ballot Simulator は、E2E 検証可能投票の教育的デモとして、正常系 S0 と改ざんシナリオ S1〜S5 を提供します。S1〜S5 は投票システムに対する特定の攻撃を模擬し、検証パイプラインがどのチェックで異常を検出するかを実演します。

この部に含まれる章

• シナリオ一覧 — S0〜S5 の定義、データフロー、実装上の扱い
• 検出メカニズム — シナリオ別に失敗するチェックと最終判定

想定読者と前提

• 想定読者: 検証パイプラインの教育的デモを試したい技術者
• 前提: 検証パイプライン の 4 段階モデルを把握していること

本章で扱わないもの

• 実世界の投票システムに対する攻撃手法の一般論
• 本番投票システム向けの脅威モデリングや対策ガイド
• S2/S4 を proof-tampering に変更するなど PoC スコープを超える攻撃シナリオ

関連する章

• 検証パイプライン — 各シナリオに対応するチェックの一覧
• 第三者検証ガイド — シナリオごとに生成された bundle.zip を監査する手順
• 用語集 — シナリオ・改ざんに関する用語定義

シナリオ一覧

改ざんシナリオ S0〜S5 の定義と、実装上どこを改変するかを整理します。ここでは「zkVM 入力」「主張集計（claimed tally）」「ジャーナル統計（missing/invalid/excluded）」の関係を中心に説明します。

教育モードの目的

改ざんシナリオは、暗号的検証が実際に機能することを確認するために設計されています。

• 正常ケース（S0）を基準として、検証パイプラインが通過する状態を確認する
• 攻撃シナリオ（S1〜S5）を適用して、どの不変条件が破れると検証が失敗するかを確認する

攻撃の 2 類型

• 入力改ざん (tamperMode=input): S1 / S3 / S5
• 主張改ざん (tamperMode=claim): S2 / S4

この図は「改ざんがどこに入るか」の分類のみを示します。どのチェックで失敗するかの詳細は 検出メカニズム を参照してください。

実装上の共通前提

• 1 回の finalize で選択されるシナリオは 1 つ（S0〜S5）
  • UI: /aggregate は single-select（S0〜S5 のラジオボタン）
  • API: POST /api/finalize は scenarioId を 1 つ受け取る
• totalExpected は 64（ユーザー 1 + ボット 63）
• 掲示板（CT Merkle）は追記専用で、シナリオ適用で既存エントリは削除しない
• tamperMode は none / input / claim の 3 種

注意事項:

• 本章は実 API 経路（/api/finalize → finalize-session → finalize-sync|async）を基準に説明する
• finalize 実行モードは FINALIZE_ASYNC_MODE で切り替わる（false: 同期, true: 非同期）。AWS 運用では通常 true
• mock mode の差分:
  • NEXT_PUBLIC_USE_MOCK_API=true の mock API fixture は本章と異なるチェック結果を返すことがある
  • USE_MOCK_ZKVM=true の mock zkVM executor は CT inclusion proof を簡略化するため、特に S5 再集計分岐の journal 統計は real zkVM と異なることがある
• 本章の「主な失敗点」は STARK 検証が success の局面を前提とする（zkGate の詳細は検出メカニズムを参照）

tamperMode により、zkVM 入力へ反映されるかどうかが決まります。

flowchart TD
  A[シナリオ選択] --> B{tamperMode}
  B -->|none / claim| C[元の votes を zkVM 入力へ]
  B -->|input| D[modifiedVotes を zkVM 入力へ]
  C --> E[zkVM 実行]
  D --> E

S0: 正常（改ざんなし）

改ざんを適用しない基準シナリオです。

S1: ユーザー票の除外

ユーザー票（インデックス 0）を modifiedVotes から削除し、63 票を zkVM に渡します。

ポイント:

• 掲示板上のユーザー票エントリは残る
• 検出は主に完全性チェック（excludedSlots > 0）
• ビットマップ証明が利用可能なら counted_my_vote_included でも検出可能

S2: ユーザー票に関する主張集計の改ざん

ユーザー票に対する「主張集計（表示する tally）」のみ改ざんします。zkVM には元の 64 票を渡します。

ポイント:

• 「票の中身を zkVM 入力で差し替える」実装ではない
• レシートや STARK 証明は通常どおり有効
• 検出の主因は counted_tally_consistent の失敗

S3: ボット票の除外

現行実装ではボット票インデックス 1（targetBotId 初期値）を削除し、63 票を zkVM に渡します。

S1 との違い:

• S1: ユーザー自身の未集計をビットマップで直接示せる
• S3: ユーザー票は含まれるが、集計全体の完全性違反で検出される

S4: ボット票に関する主張集計の改ざん

1 票のボット票に関する「主張集計」だけを改ざんします。zkVM 入力は元の 64 票のままです。

ポイント:

• S2 と同様に、改ざん対象は tally.counts 側
• 検出の主因は counted_tally_consistent の失敗

S5: ランダムエラー注入

64 票からランダムに 1 票を選び、50% で「除外」または「再集計（別候補化）」を行います。

実装上の重要点:

• tamperMode は常に input
• そのため zkVM 入力は常に modifiedVotes が使われる
• 除外パスでは missingSlots が増え、real zkVM の再集計パスでは CT inclusion proof の不整合により invalidPresentedSlots が増えるため、いずれも excludedSlots > 0 になる
• 再集計パスでは counted_tally_consistent も失敗する（claimedCounts は 64 票ベース、verifiedTally は inclusion proof 不整合の票を除外した 63 票ベース）

シナリオ一覧表

ジャーナル統計の扱い（sync / async 共通）

現行実装では、missingSlots / invalidPresentedSlots / excludedSlots / validVotes などのジャーナル統計は、sync / async いずれも zkVM が返した proof-derived な値をそのまま使います。

• sync / async いずれも、finalize 後にジャーナル統計を上書きしない
• async finalize はコールバックで bundle.zip から復元した journal をそのまま使う

シナリオ由来の ignoredCount / recountedCount / claimedCounts は presentation 用であり、journal の統計値を書き換えません。

• ignoredCount / recountedCount → tamperSummary や tamperedCount に反映
• claimedCounts → S2/S4 や S5 再集計分岐での表示用 tally

tamperMode=claim（S2/S4）でも同様に、journal 統計は zkVM の値のままです。

集計フローへの挿入点

flowchart TB
  A[セッション votes 読み込み] --> B[シナリオ適用]
  B --> C{tamperMode}
  C -- input --> D[modifiedVotes で zkVM 入力生成]
  C -- claim --> E[元の votes で zkVM 入力生成]
  D --> F[zkVM 実行]
  E --> F
  F --> G[finalizationResult 保存]
  B --> H[claimedCounts 計算]
  H --> G

検出メカニズム

各改ざんシナリオに対して、検証パイプラインがどのチェックで失敗するかを整理します。本章は実 API の判定ロジックを基準にしており、STARK 検証が success になった後の挙動を前提とします。

前提

• NEXT_PUBLIC_USE_MOCK_API=true の mock API fixture は本章と異なるチェック結果を返すことがある。
• USE_MOCK_ZKVM=true の mock zkVM executor は CT inclusion proof を簡略化するため、S5 再集計分岐の journal 統計は real zkVM と異なることがある。以降、再集計分岐の挙動は real zkVM を前提に記述する。
• 現行 API は castSource=client のため、cast_* チェックはシナリオに関係なく not_run。

検出の 2 つの原理

• 原理1: 完全性違反 (excludedSlots > 0) → counted_missing_indices_zero が失敗（主に S1/S3/S5）
• 原理2: 主張集計の不整合 (claimed ≠ verified) → counted_tally_consistent が失敗（主に S2/S4）

シナリオ別の主な失敗チェック（STARK 解決後）

補足:

• S1 では、ビットマップ証明が利用可能な場合 counted_my_vote_included も失敗し得ます
• S2/S4 では、counted_input_commitment_match は通常成功します（zkVM 入力を改変していないため）
• S5 の再集計分岐では counted_tally_consistent も失敗します（詳細は下記「S5 の実装依存ポイント」参照）

4 段階検証モデルとの対応（/api/verify 応答）

この表は「シナリオ適用による典型挙動」を示します。running や追加の not_run は運用状態や証拠不足により別途発生します。 なお、ここでの STARK Verification は段階別の表示ステータスです。全体の verificationStatus は fail-closed ルールにより failed になることがあります。

チェックID（主要項目）マトリクス（STARK 解決後）

• S5 の counted_my_vote_included は、ランダム対象がユーザー票（除外または再集計）なら失敗し得ます。証拠不足時は not_run になります
• S5 の counted_tally_consistent は、除外パスでは成功、再集計パスでは失敗します（詳細は下記「S5 の実装依存ポイント」参照）
• いずれの分岐でも主な失敗は counted_missing_indices_zero です

S2/S4 で何が起きるか

S2/S4 は「入力改ざん」ではなく「主張集計改ざん」です。

flowchart TD
  A["tamperMode=claim (S2/S4)"]
  A --> V1["元の votes を zkVM 入力へ"]
  V1 --> V2["verifiedTally"]
  A --> C1["claimedCounts を改変"]
  C1 --> C2["API の tally.counts"]
  V2 --> X{"claimed と verified は一致?"}
  C2 --> X
  X -->|不一致| F["counted_tally_consistent = failed"]

このため counted_input_commitment_match の失敗は通常発生しません（zkVM 入力は元票）。

S5 の実装依存ポイント

S5 はランダムに除外または再集計を選びますが、実装上は常に tamperMode=input です。つまり claim tamper ではなく、改変後の votes が zkVM 入力に入ります。ジャーナル統計は sync / async どちらでも zkVM が返した値をそのまま使います（詳細はシナリオ一覧 > ジャーナル統計の扱いを参照）。

• 除外分岐: missingSlots=1 となり、counted_missing_indices_zero が失敗
• 再集計分岐: invalidPresentedSlots=1 となり、counted_missing_indices_zero が失敗
• 再集計分岐では counted_tally_consistent も失敗します。claimedCounts は改変後の 64 票から算出されますが、zkVM は元の CT 掲示板 proof/root と新しい commitment が整合しない票を除外するため verifiedTally は 63 票ベースになります

ビットマップ証明の役割

counted_my_vote_included は、チェック定義上 required のユーザー包含チェックです。

• S1（ユーザー票除外）では、証明が利用可能なら失敗して「自分の票が未集計」であることを直接示せる
• 証拠不足で not_run になる場合でも、最終判定は Verified になりません:
  • 完全性違反が同時にある場合 → votes_excluded_unknown
  • 完全性違反が無く required evidence が欠ける場合 → missing_evidence

最終判定（Verified 表示）

最終表示は verification-summary のルールで決定されます。

flowchart TB
  A[検証チェック集合] --> B{必須チェック failed?}
  B -- yes --> F[failed 系ステータス]
  B -- no --> C{必須チェック not_run / running?}
  C -- yes --> W[in_progress / missing_evidence]
  C -- no --> D{任意チェックに劣化あり?}
  D -- yes --> L[verified_with_limitations]
  D -- no --> V[fully_verified]

代表的な失敗ステータス:

• user_vote_excluded / votes_excluded / votes_excluded_unknown: 完全性違反（S1/S3/S5）
• published_tally_mismatch: claimed と verified の不一致（S2/S4）
• counted_integrity_failed: Counted 系必須チェック失敗の一般ケース

これらの検出経路は、単体・結合・E2E テスト の CLI / E2E フローと、Property-based Testing の Merkle / journal 不変条件で補強しています。

品質保証と形式手法

この部では、STARK Ballot Simulator の検証ロジックをどの品質境界で支えているかを説明します。

本プロジェクトは AI コーディングエージェントと協業して実装を進めました。実装速度を上げるだけでなく、AI 協業で混入しやすい次のような乖離を検出できる境界が必要です。

• 仕様と実装のドリフト
• 暗黙の fallback
• 公開してはいけないアーティファクトの混入
• Verified 判定ロジックの分散

この部に含まれる章

• 単体・結合・E2E テスト — example-based テストでの局所退行検出と CLI / E2E 経路
• Property-based Testing — fast-check と Rust proptest による入力空間探索
• Lean による形式化 — 抽象モデルでの不変条件証明と CI 連携

想定読者と前提

• 想定読者: 実装に追従するテストや形式化の設計判断を確認したい開発者・監査者
• 前提: 単体テスト・結合テスト・E2E テストの一般的な区分、および Property-based Testing の基本概念を把握していること

品質保証のレイヤー

本書では、example-based tests、property-based testing、Lean による形式化、それらを CI に接続する仕組みを次のレイヤーで使い分けます。

中心に置く不変条件

最も重要な品質目標は、ユーザーに Verified と表示してよい条件を緩めないことです。

• required check が失敗・未実行・実行中なら Verified にしない
• excludedSlots > 0 を成功状態にしない
• STARK receipt verification だけを根拠に全体成功としない
• input.json、verification.json、included-bitmap.json、seen-bitmap.json を公開配布対象に含めない
• mock / dev receipt / production STARK proof の違いをテスト階層で明示する

これらは ゲーティングロジック と バンドル構造 で説明した安全境界を、テストと形式化の側から支えるものです。

本章で扱わないもの

この部は、システム全体の完全な形式検証を主張するものではありません。SHA-256 や RISC Zero の暗号学的健全性、各種ランタイムや AWS の正しさ、本番選挙システムとしての安全性は対象外です。Lean が扱う射程と扱わない射程の詳細は Lean による形式化 > 証明していないこと を参照してください。

関連する章

• 検証パイプライン — テストと形式化が守る Verified 判定の本体
• ゲーティングロジック — 不変条件として品質保証が支える側のロジック
• バンドル構造 — 公開境界の判定に関わる安全境界

単体・結合・E2E テスト

このページでは、example-based tests がどのリスクを守っているかを整理します。ここでの中心はテスト数ではなく、検証アプリとして失敗してはいけない境界に、どの層のテストを置いているかです。

テストピラミッド

単体テスト

単体テストは、純粋関数や小さな UI component、schema、環境変数 guard、エラー整形の退行検出に使います。

主な対象:

• 検証チェック定義と summary logic
• Lean 生成 vector と照合する verification summary / display / check definition
• zkVM journal / input commitment / bitmap helper
• session capability token と Turnstile bypass guard
• UI component と hooks
• i18n translation consistency

結合テスト

結合テストは、境界をまたいだ契約が崩れていないかを検査します。

主な対象:

• Next / Hono で共有する API route registry
• store 実装と finalization state transition
• verification bundle の public allowlist
• verifier-service client と STARK receipt status の扱い
• Lean 生成 vector と照合する input commitment / bitmap Merkle / Rust guest model
• bitmap proof、bulletin proof、verification run などの session-scoped API

CLI / E2E テスト

CLI と Playwright は、単一関数ではなく利用者フローとしての正しさを見ます。

• CLI flow: session 作成、投票、集計、検証をブラウザなしで実行する
• Playwright mock flow: production-mode の Next test server 上で主要画面を通す
• axe smoke: 主要ページの重大な accessibility violation を検出する
• real zkVM dev / prod flow: proof contract 変更時に mock だけで完了扱いにしないための重い確認経路

主なコマンド

RISC0_DEV_MODE=1 の receipt は production STARK proof ではありません。UI/API の回帰検出には有用ですが、proof soundness を確認したことにはなりません。

重要な検査観点

Verified を誤表示しない

このアプリの最重要 invariant は、必要な暗号・整合性チェックが通っていない状態で Verified を表示しないことです。

テストでは次のような状態を fail-closed に扱います。

• required check が failed
• required check が not_run / pending / running
• STARK receipt verification が失敗または未解決
• unknown check や空の check set
• excludedSlots > 0
• public tally と verified tally の不一致

この観点は ゲーティングロジック の実装側の安全網です。

公開 artifact 境界

bundle.zip は第三者検証に必要な公開可能 artifact だけを含みます。

公開してよいものは allowlist で管理し、次の artifact は配布対象に含めません。

• input.json
• verification.json
• included-bitmap.json
• seen-bitmap.json

この境界は sync 生成、async container、bundle/report delivery の複数箇所にまたがるため、テストで契約として固定します。

mock / real zkVM 境界

mock zkVM は UI や API flow の高速な退行検出に使います。一方で、journal format、input commitment、Image ID、receipt verification contract に触れる変更では、Rust 側や real zkVM 経路を使って TypeScript と Rust の対応を確認します。

コストの違いを前提に、普段は軽い gate を使い、proof contract に触れる変更では重い gate へ進む設計です。

UI と accessibility

Playwright は、ユーザーが実際に触る投票・集計・検証の流れを production-mode server 上で確認します。テスト ID は翻訳文ではなく安定した data-testid を使い、i18n やレイアウト変更に引きずられにくくしています。

CI での位置づけ

CI では、TypeScript の core checks、UI mock E2E、Rust tests、formal checks、public snapshot checks が役割を分けて動きます。

すべてを常に最重構成で走らせるのではなく、変更領域に応じて必要な gate を選ぶ構成にしています。特に production STARK proof は高コストなので、proof 入力や journal contract に関わる変更で使う確認経路として扱います。

Property-based Testing

Property-based Testing (PBT) は、少数の fixture では見落としやすい境界条件を、生成入力と「常に成り立つべき性質」で検査するために使います。

本プロジェクトでは、Merkle tree、bitmap packing、input commitment、journal count のように、順序・境界・改ざん耐性が重要なロジックに PBT を置いています。

PBT を導入した理由

example-based tests は既知のシナリオを守ります。PBT はそれに加えて、次のような仕様レベルの性質を入力空間全体に近い形で探索します。

• 同じ vote multiset なら入力順序を変えても input commitment が変わらない
• root、leaf、index、proof node を改ざんすると Merkle proof が失敗する
• LSB-first bitmap packing の bit address が境界で崩れない
• journal count の分解式が常に成立する

PBT は証明ではありませんが、実装に対して広い入力空間を継続的に探索できるため、暗号周辺の encoding drift や境界条件の退行を早期に検出できます。

TypeScript 側の PBT

RFC 6962 Merkle tree

対象:

• src/lib/merkle/rfc6962-merkle-tree.property.test.ts

検査する性質:

• 任意の leaf set について inclusion proof が round-trip する
• root、leaf、index、proof node を改ざんすると検証に失敗する
• append-only consistency proof が old size / new size の組み合わせで検証できる
• 奇数サイズ tree の代表ケースを固定 regression として保持する

Bitmap Merkle

対象:

• src/lib/merkle/bitmap-merkle-tree.property.test.ts

検査する性質:

• 生成した bitmap の任意 index について proof が round-trip する
• proof から抽出した included が元の bit と一致する
• leaf chunk や audit path の改ざんを拒否する
• 0, 1, 7, 8, 255, 256, 257, 511, 512 bit などの境界を固定ケースで検査する

Input commitment

対象:

• src/lib/zkvm/__tests__/input-commitment.property.test.ts

検査する性質:

• 同じ vote multiset の順序を入れ替えても input commitment が変わらない
• duplicate index がある異常入力でも deterministic tie-break により順序が安定する
• election ID、bulletin root、tree size、total expected を変えると commitment が変わる
• vote の index、commitment、Merkle path を変えると commitment が変わる

Journal invariants

対象:

• src/lib/zkvm/__tests__/journal-invariants.property.test.ts

検査する性質:

• totalVotes = validVotes + rejectedRecords
• invalidVotes = rejectedRecords
• seenIndicesCount = validVotes + invalidPresentedSlots
• validVotes + invalidPresentedSlots + missingSlots = treeSize
• excludedSlots = missingSlots + invalidPresentedSlots
• included bitmap の true は seen bitmap の true を含意する

Rust 側の PBT

対象:

• zkvm/methods/guest/src/property_tests.rs

検査する性質:

• input commitment が vote order に対して permutation invariant
• duplicate index の tie-break を含めても permutation invariant
• RFC 6962 inclusion proof が reference tree と一致する
• root / leaf / path 改ざんを拒否する
• bitmap root が reference oracle と一致する
• bit flip で bitmap root が変わる

Rust 側の PBT は、zkVM guest / contract-core で使う低レベル実装に近い場所で、TypeScript 側と同じ性質を別実装として検査します。

Lean との関係

PBT は実装に対して広い入力空間を探索し、Lean は同種の不変条件を抽象モデル上で証明します。両者の役割分担と、Lean から出力した generated vectors を介して実装テストに接続する仕組みは Lean による形式化 > 実装との接続 に整理しています。

限界

• PBT は数学的証明ではない
• 生成範囲は CI 実行時間とのバランスで制限する
• SHA-256 の衝突困難性は PBT では証明しない
• RISC Zero receipt soundness も PBT の対象ではない
• 生成器に含めていない入力領域は探索されない

そのため、PBT は example-based tests や Lean formalization を置き換えるものではなく、境界条件と実装 drift を検出する追加レイヤーとして扱います。

Lean による形式化

本プロジェクトでは Lean 4 を使い、Verified 表示の fail-closed 条件、journal count の整合性、input commitment の canonical encoding、LSB-first bitmap packing、抽象 guest tally model の不変条件を形式化しています。

Lean は実装を直接証明するのではなく、抽象モデル上で不変条件を証明し、そこから生成した generated vectors / formal report / formal audit を TypeScript・Rust のテストと CI に接続することで、モデルと実装の対応付けを継続的に検査します。Lean が扱わない範囲は末尾の 証明していないこと を参照してください。

Lean で定義しているもの

GuestModel.lean は zkvm/methods/guest/src/main.rs を行単位で翻訳したものではありません。外部的に重要な処理順序、つまりインデックス範囲、重複 index、選択肢、コミットメント、重複 commitment、包含証明、集計反映の順序を抽象 state machine として表します。

Lean で証明していること

これらは抽象モデル上の主張です。実装との対応は、次の generated vectors とテストで検査します。

実装との接続

flowchart LR
  L["Lean models<br/>formal/StarkBallotFormal/*.lean"]
  T["Theorems<br/>形式的な不変条件"]
  R["formal-report.json<br/>主張と前提"]
  V["generated-vectors/*.json<br/>実装対応付けケース"]
  A["formal-audit.json<br/>theorem hash / dependency / hygiene"]
  TS["TypeScript tests<br/>Vitest"]
  RS["Rust vector tests<br/>cargo test"]
  FCI["formal CI<br/>pnpm formal:verify"]
  RCI["Rust tests workflow<br/>cargo test"]

  L --> T
  T --> R
  L --> V
  T --> A
  V --> TS
  V --> RS
  R --> FCI
  V --> FCI
  A --> FCI
  TS --> FCI
  RS --> RCI

pnpm formal:verify は Lean build、formal report / generated vectors / audit の freshness、TypeScript の vector-consuming tests、生成 JSON の format check をまとめて実行します。Rust 側の vector-consuming tests は docs/current/formal/generated-vectors/** の変更で起動する Rust tests workflow の cargo test によって検査します。

この接続により、Lean model が変わったのに実装テストが追従していない場合、または実装側の encoding / summary / guest behavior が model から外れた場合に、CI 上で drift を検出できます。

対応付けを支える成果物

Lean の成果物を public documentation と実装テストに接続するため、次を組み込んでいます。

• guest-model generated vectors
• check-definition drift vector
• theorem statement hash
• generated-vector hash
• #print axioms に基づく theorem dependency audit
• proof hygiene scan
• explicit guest bounds
• TypeScript / Rust 側の vector-consuming tests
• pnpm formal:verify による freshness gate

実行コマンド

証明していないこと

Lean は次を証明しません。

• SHA-256 の衝突困難性
• RISC Zero receipt soundness
• Rust compiler / TypeScript runtime / browser runtime の完全な正しさ
• AWS runtime behavior
• React rendering 全体の正しさ
• 本番選挙システムとしての安全性
• zkVM guest Rust 実装全体の line-by-line verification

したがって、正確な主張は「投票システム全体を形式検証した」ではありません。正確には、選択した安全モデルを Lean で証明し、generated vectors と CI drift guard によって TypeScript / Rust 実装との対応を検査している、というものです。

AWS アーキテクチャ

現行の AWS 構成は、Amplify Gen 2 が担うアプリ層と、Terraform で管理する非同期プローバー層に分かれています。この部では、その構成、成立経緯、連携点、運用上の制約を扱います。

この部に含まれる章

• 現行構成とサービス一覧 — 現行構成の成立経緯、環境分離、サービス構成
• トポロジー — レイヤ別のサービス構成と通信フロー
• 非同期プローバー — SQS → Step Functions → ECS による証明パイプライン
• イメージ署名 — AWS Signer によるコンテナイメージ検証
• Terraform — IaC による構成管理とワークスペース運用

想定読者と前提

• 想定読者: 非同期プローバーや IaC の構成を把握したい運用者
• 前提: AWS の基本サービス（S3 / SQS / Step Functions / ECS）と Terraform の概念を把握していること

本章で扱わないもの

• Amplify Gen 2 の Auth / Data 機能の詳細
• Terraform 文法・モジュール設計の一般論
• CloudWatch アラート設計やコスト最適化ガイド

関連する章

• zkVM 設計 — ECS 上で実行されるホストとレシート生成
• 第三者検証ガイド — 検証ページで取得した bundle.zip を使うローカル監査
• 用語集 — インフラ用語の定義

現行構成とサービス一覧

現行の AWS 構成（管理境界・環境分離・利用サービス）を整理する章です。ハイブリッド構成に至った経緯と改善候補は 設計ふりかえり § 6 を参照してください。

現行の管理境界

Amplify Gen 2 がアプリ層、Terraform が非同期プローバー基盤を担う 2 系統管理になっています。

環境分離

develop と main の 2 環境を運用し、主要なアプリケーション実行系リソースは Terraform ワークスペースと Amplify ブランチデプロイで分離しています。両環境とも証明モードは実 STARK 証明（代表実測はECS Fargate タスク仕様参照）で、RISC0_DEV_MODE=1 / USE_MOCK_ZKVM=true はローカル同期実行用の設定です。

ただし全リソースが環境ごとに二重化されているわけではなく、RISC Zero ツールチェーン用の ECR リポジトリと CodeBuild プロジェクトは aws.shared provider で共有されます。環境別に分かれるのは prover 用 ECR、証明バンドル S3、prover image metadata S3、SSM current metadata parameter、SQS、Step Functions、ECS、CloudTrail などの実行系リソースです。

全体構成図

図: STARK Ballot Simulator の AWS 全体構成。現行では Amplify 管理領域（上）と Terraform 管理領域（下）に分かれている。

サービス一覧

本システムで使用する主要な AWS サービスと、その役割の概要です。

Amplify 管理

Terraform 管理

これらのサービスに紐づく IAM ロール / ポリシーも同じ Terraform 管理下にあります。詳細は Terraform > IAM 設計 を参照してください。

Amplify と Terraform の境界

2 つのインフラ管理ツール間の連携は、ARN と環境変数によって行われます。

flowchart TB
  subgraph TF["Terraform 管理"]
    OUT["Amplify 同期出力<br/>SFN ARN / SQS ARN / SQS URL / 証明バンドル S3 名"]
    OPS["運用出力<br/>metadata S3 名 / SSM parameter 名"]
    IN["入力変数<br/>finalize_callback_lambda_arn"]
  end

  subgraph AMP["Amplify Gen 2 管理"]
    ENV["環境変数"]
    CB["finalize-callback-runner<br/>Lambda ARN"]
  end

  OUT -.対応する値.-> ENV
  CB -.ARN を入力変数へ設定.-> IN

Terraform の出力値（Step Functions ARN、SQS ARN、SQS URL、S3 バケット名など）は Amplify の環境変数に手動で反映する運用で、PROVER_STATE_MACHINE_ARN と PROVER_WORK_QUEUE_ARN は Amplify backend のデプロイ時にも必須（未設定で fail-closed）です。同期手順と一覧は Terraform > Amplify との連携ポイント を参照してください。

なお、prover image metadata bucket 名と current metadata SSM parameter 名は CodeBuild / 運用確認向けの Terraform 出力であり、Amplify 環境変数へ同期する実行時契約ではありません。

関連する章

• トポロジー — リクエスト経路とコンポーネント間の通信フロー
• 非同期プローバー — SQS → Step Functions → ECS の実行時フロー
• Terraform — Amplify との連携ポイント（ARN / 環境変数名）
• 設計ふりかえり § Amplify 単独構成からハイブリッド構成への移行 — 現行構成に至った設計判断

トポロジー

AWS 上のサービス配置と、コンポーネント間の通信経路を俯瞰する章です。

本システムは 5 つの論理レイヤ（Web、API、Data、Prover、Storage）で構成され、各レイヤは明確な責務を持ちます。

レイヤ別トポロジー

Web レイヤ

Amplify Hosting が Next.js アプリケーションのビルドとホスティングを担当します。GitHub リポジトリのブランチ（develop / main）と Amplify の環境が 1 対 1 で対応し、プッシュをトリガーとする自動デプロイが行われます。

API レイヤ

API Gateway（HTTP API）が /api/* パスパターンのリクエストを受け取り、単一の Lambda 関数（hono-api）にプロキシします。hono-api は Hono フレームワーク上に構築されており、ルーティング、セッション管理、Turnstile 検証、レート制限を処理します。下図の「主なリクエスト制御」は、hono-api がルートごとに適用有無と順序を切り替える代表的な要素を示します（固定順のパイプラインではありません）。

flowchart LR
  Client["クライアント"] --> APIGW["API Gateway<br/>(HTTP API)"]
  APIGW --> HONO["hono-api<br/>Lambda"]
  HONO --> APPSYNC["AppSync<br/>(Data)"]
  HONO --> SQS["SQS<br/>(非同期証明)"]
  HONO --> S3["S3<br/>(バンドル取得)"]

  subgraph "主なリクエスト制御（ルートごとに適用）"
    direction TB
    RATE["IP / zkVM レート制限"]
    SESS["セッション / capability 検証"]
    TURN["Turnstile 検証"]
    BODY["入力検証"]
    HAND["ハンドラー実行"]
    RATE -.-> HAND
    SESS -.-> HAND
    TURN -.-> HAND
    BODY -.-> HAND
  end

CORS 設定では X-Session-ID と X-Session-Capability ヘッダーを許可し、セッションスコープと capability トークンによるリクエスト制御を実現しています。なお POST /api/verification/run だけは、hono-api から専用の verifier-service-runner Lambda を同期起動する構成です（後述のエンドツーエンドのデータフローを参照）。

Data レイヤ

AppSync（GraphQL API）と DynamoDB が、セッション・投票・集計結果のデータ永続化を担当します。データプレーンは allow.resource(...) により hono-api / prover-dispatch-proxy / finalize-callback-runner からの SigV4 呼び出しに限定され、未認証アクセスは無効です（Amplify Data の検証要件として fallback group は定義していますが、エンドユーザーには割り当てていません）。

主要なデータモデルは以下の 2 つです（集計結果は VotingSession.finalizationResultJson に格納）。

レート制限用に 2 つの追加テーブル（RateLimitEvents、RateLimitCounters）が PAY_PER_REQUEST モードで運用されています。

Prover レイヤ

STARK 証明の生成を担当するレイヤです。SQS キュー、Step Functions ステートマシン、ECS Fargate タスクで構成されます。詳細は 非同期プローバー を参照してください。

flowchart LR
  CODEBUILD["CodeBuild<br/>プローバーイメージ"] --> META["S3<br/>イメージメタデータ"]
  CODEBUILD --> SSM["SSM Parameter<br/>current metadata"]
  SQS["SQS<br/>ワークキュー"] --> DP["prover-dispatch-proxy<br/>Lambda"]
  DP --> SFN["Step Functions<br/>ディスパッチャー"]
  SFN --> SIG["check-image-signature<br/>Lambda"]
  SFN --> ECS["ECS Fargate<br/>16 vCPU / 32 GB"]
  SFN --> CALLBACK["finalize-callback-runner<br/>Lambda"]
  ECS --> S3["S3<br/>証明バンドル"]

ECS タスクは ARM64 アーキテクチャの Fargate で実行され、専用の VPC（10.0.0.0/16）内のパブリックサブネットに配置されます。セキュリティグループは HTTPS エグレスのみを許可し、インバウンドトラフィックは一切受け付けません。

Storage レイヤ

S3 バケットが、証明バンドルに含まれる配布対象アーティファクトと非公開ワーク入力の保存を担当します。 Terraform はこれに加えて、プローバーイメージのビルドメタデータを保存する S3 バケットと、現在候補を指す SSM Parameter も管理します。

プローバーイメージメタデータ用バケット（{project}-prover-metadata-{環境名}）も Terraform 管理下にあり、AES256 暗号化・パブリックアクセス全ブロック・バージョニング Enabled で運用されます。CodeBuild からの publish 仕様と SSM current pointer の関係は イメージ署名 > ビルドと署名 を参照してください。

証明バンドル側のオブジェクトパスは既定で sessions/{sessionId}/{executionId}/ 配下です。先頭プレフィックスは s3_proof_prefix で変更可能ですが Amplify 側に sessions/ を前提とする箇所があり、変更時の影響範囲は 非同期プローバー > フェーズ 2: ディスパッチ を参照してください。

S3 バケット自体はパブリックアクセス全ブロックです。「区分」は機密性の扱いを示すもので、実際の配布経路（presigned URL 等）は バンドル構造 を参照してください。

エンドツーエンドのデータフロー

投票から検証までの全データフローを、レイヤ間の通信として示します。

sequenceDiagram
  participant C as クライアント
  participant W as Web レイヤ<br/>(Amplify Hosting)
  participant A as API レイヤ<br/>(API GW + Lambda)
  participant V as 検証レイヤ<br/>(verifier-service-runner)
  participant D as Data レイヤ<br/>(AppSync + DDB)
  participant P as Prover レイヤ<br/>(SQS → SFN → ECS)
  participant S as Storage レイヤ<br/>(S3)

  Note over C,D: 投票フェーズ
  C->>W: ページ読み込み
  C->>A: POST /api/session
  A->>D: セッション作成
  C->>A: POST /api/vote
  A->>D: 投票 + コミットメント保存
  A-->>C: 投票レシート返却
  Note over A,D: ボット投票を自動追加

  Note over C,P: 集計フェーズ
  C->>A: POST /api/finalize
  alt FINALIZE_ASYNC_MODE=true
    A->>P: SQS メッセージ送信
    A-->>C: 202 Accepted
    P->>S: input.json 保存（SFN 起動前）
    P->>P: イメージ署名検証
    P->>P: ECS タスクで証明生成
    P->>S: 実行成果物 + 公開監査アーティファクト + bundle.zip 保存
    P->>D: コールバックで結果書き込み
  else FINALIZE_ASYNC_MODE=false
    A->>A: 同期で zkVM 実行
    A-->>C: 200 OK（集計結果）
  end

  Note over C,S: 検証フェーズ
  C->>A: GET /api/verify
  A->>D: セッション + 集計結果取得
  A-->>C: 検証ペイロード返却
  C->>A: POST /api/verification/run
  A->>V: verifier-service-runner を同期起動
  V->>S: bundle.zip 取得
  V->>V: verifier-service 実行
  opt USE_S3=true
    V->>S: verification.json / bundle.zip の書き戻しを試行
  end
  V-->>A: 検証結果返却
  A-->>C: 検証結果返却

verifier-service-runner は S3 書き戻しが有効な構成で verification.json と更新済み bundle.zip の保存を試み、成功した場合のみ新しい key を finalization state に反映します。失敗時はもとの s3BundleKey を維持するため配信元は失われません（書き戻し挙動の詳細と bitmap sibling object の扱いは バンドル構造 を参照）。

ネットワーク構成

VPC

Terraform が管理する VPC は、ECS Fargate タスク専用です。Amplify 管理のリソース（Lambda、AppSync）は VPC 外で動作します。

flowchart TD
  subgraph VPC["VPC (10.0.0.0/16)"]
    subgraph AZ1["ap-northeast-1a"]
      S1["パブリックサブネット<br/>10.0.1.0/24"]
    end
    subgraph AZ2["ap-northeast-1c"]
      S2["パブリックサブネット<br/>10.0.2.0/24"]
    end
    SG["セキュリティグループ<br/>Egress: 443 のみ"]
  end

  IGW["インターネット<br/>ゲートウェイ"]
  ECR["ECR<br/>(イメージ取得)"]
  S3["S3<br/>(バンドル保存)"]

  VPC --> IGW
  IGW --> ECR
  IGW --> S3

ECS タスクはパブリック IP を持ちますが、セキュリティグループがインバウンドを全拒否するため、外部からのアクセスはできません。アウトバウンドは HTTPS（ポート 443）のみ許可され、ECR からのイメージ取得、S3 へのアップロード、CloudWatch Logs などの AWS API 通信に使用されます。

監視とロギング

主な CloudWatch ログ群

Amplify 管理 Lambda と AppSync の実際のロググループ名には app / branch / API 由来の識別子が入るため、運用時は runbook の discovery クエリで特定します。

CloudTrail（main 環境のみ）

main 環境では CloudTrail による全リージョン監査ログが有効です。

非同期プローバー

SQS → Step Functions → ECS Fargate で証明を非同期生成する経路と、各段階の責務を扱う章です。

STARK 証明の生成は 64 票で約 6 分を要するため、同期的な HTTP リクエスト内では完了できません。非同期パイプラインにより、Web リクエストのタイムアウトを回避しつつ、高負荷な証明生成を安全に実行します。

この章は FINALIZE_ASYNC_MODE=true で動作する非同期経路を対象としています。

パイプライン全体像

flowchart TB
  API["POST /api/finalize"] --> SQS["SQS<br/>ワークキュー"]
  SQS --> DP["prover-dispatch-proxy<br/>Lambda"]
  DP --> S3U["S3<br/>input.json 保存"]
  DP --> SFN["Step Functions<br/>StartExecution"]
  SFN --> SIG["check-image-signature<br/>Lambda"]
  SIG --> CHK{"署名 COMPLETE?"}
  CHK -->|Yes| ECS["ECS Fargate<br/>RunTask"]
  CHK -->|No| SFNFAIL["Step Functions<br/>署名失敗分岐"]
  ECS --> S3W["S3<br/>bundle / sibling artifacts 保存"]
  ECS --> SFNRET["Step Functions<br/>成功/失敗を判定"]
  SFNFAIL --> CB["finalize-callback-runner<br/>Lambda"]
  SFNRET --> CB
  CB --> DDB["AppSync/DynamoDB<br/>セッション更新"]

詳細な失敗分岐（署名検証 NG、プローバー実行失敗）は、後続のステートマシン図で示します。

各フェーズの詳細

フェーズ 1: リクエスト受付

クライアントが POST /api/finalize を呼び出すと、API ハンドラーは以下の処理を行います。

以下は FINALIZE_ASYNC_MODE=true の場合です。

1. セッションの状態を検証（全投票が完了していること）
2. zkVM 入力を構築（入力ビルダーが投票データ + Merkle パスを組み立て）
3. セッションの finalizationState を「pending」に更新
4. SQS キューにメッセージを送信
5. クライアントに 202 Accepted を返却

クライアントはその後、GET /api/sessions/:id/status を X-Session-Capability 付きでポーリングして進捗を確認します。

フェーズ 2: ディスパッチ

prover-dispatch-proxy Lambda が SQS メッセージを受信し、以下を実行します。

1. SQS メッセージと現在のセッション状態を検証
2. zkVM 入力 JSON を S3 にアップロード（sessions/{sessionId}/{executionId}/input.json）
3. Step Functions のステートマシンを StartExecution で起動
4. セッションの finalizationState を「running」に更新し、executionId と Step Functions execution ARN を記録

フェーズ 2 の補足事項

前提条件チェック: dispatch 前に、セッションが存在し、finalizationState.status が pending、finalizationState.executionId が SQS メッセージの executionId と一致することを確認します。揃わない場合は高コストな証明実行に進まず中断し、伝播遅延など再試行で回復し得る状態は SQS の受信回数に応じて retry / DLQ に委ねます。

contract generation の互換性: SQS メッセージに付いている contract generation が保存済みの finalization contract と互換でない場合、unsupported_current_artifact として既存の session state を fail-closed に確定させます（再試行対象外）。

同時実行制御: Amplify 側の SQS trigger は batchSize=1 で、PROVER_LAMBDA_CONCURRENCY により予約同時実行数を制御します（既定 2）。Step Functions 起動時の throttle 系エラーは Lambda が例外として返し、SQS retry の対象にします。

s3_proof_prefix と Amplify 側の連動: S3 パスプレフィックスは Terraform 変数 s3_proof_prefix で変更可能ですが、Amplify 側に sessions/* を前提とする以下の箇所があるため、変更時は同時に更新が必要です。

• verifier-service-runner Lambda の S3 アクセスポリシー（sessions/* のみに Get/Put/List を許可）
• CLI / verifier-service の管理ポリシー（同様に sessions/* 限定）
• 関連 Amplify 環境変数

フェーズ 3: 証明生成

Step Functions ステートマシンが 3 つのステップを順次実行します。

stateDiagram-v2
  [*] --> VerifyImageSignature
  VerifyImageSignature --> CheckImageSignature
  VerifyImageSignature --> FinalizeFailed: Lambda 呼び出し失敗
  CheckImageSignature --> RunProver: 署名 COMPLETE
  CheckImageSignature --> FinalizeSignatureFailed: 署名 NG
  RunProver --> FinalizeSucceeded: 成功
  RunProver --> FinalizeFailed: 失敗
  FinalizeSignatureFailed --> [*]
  FinalizeSucceeded --> [*]
  FinalizeFailed --> [*]

VerifyImageSignature

check-image-signature Lambda を呼び出し、ECR イメージのダイジェストに対する AWS Signer 署名のステータスを確認します。詳細は イメージ署名 を参照してください。

CheckImageSignature

Choice ステートで署名ステータスを判定します。COMPLETE であれば RunProver に進み、それ以外は FinalizeSignatureFailed に遷移してコールバック Lambda に失敗を通知します。

RunProver

ECS Fargate タスクを ecs:runTask.sync（同期モード）で起動します。Step Functions はタスクの完了を待機し、成功/失敗に応じて対応するコールバックステートに遷移します。終端ステートの一覧と意味はクライアント側のポーリングの表にまとめています。

ECS タスクのコンテナには、Step Functions の入力からセッション固有の環境変数が注入されます。

フェーズ 4: 結果通知

Step Functions が finalize-callback-runner Lambda を呼び出し、以下の情報をセッションに書き戻します。

• 成功時: bundle メタデータ（s3BundleKey、s3UploadedAt）と、bundle.zip / bitmap artifact から復元した finalizationResult
• 失敗時: 失敗状態とエラー情報（イメージ署名失敗、プローバーエラーなど）

bundle / report の配信は、capability 検証付きの短命 presigned URL 経由で行います。詳細は バンドル構造 を参照してください。

ECS タスクの実行フロー

ECS Fargate タスク内のコンテナは、エントリポイントスクリプトにより以下の処理を順次実行します。

1. S3 から入力 JSON をダウンロード
2. 入力の構造を検証（必須フィールド確認）
3. zkVM ホストバイナリを実行（タイムアウト: 900 秒）
4. ジャーナルを JSON に変換
5. public-input.json、election-manifest.json、close-statement.json を構築
6. journal.json と公開監査アーティファクトの整合性を検証
7. bundle.zip を作成（receipt.json + journal.json + public-input.json + election-manifest.json + close-statement.json）
8. 生成物と private sibling artifacts を S3 にアップロード（リトライ付き）

入力の検証

エントリポイントは、zkVM 入力 JSON に必要なフィールドが存在することを確認します。欠落があればタスクは即座に失敗し、Step Functions が失敗コールバックを実行します。

zkVM ホストバイナリの実行

コンテナ内の /opt/zkvm/bin/host がプローバーとして起動されます。タイムアウトと代表実測値は ECS Fargate タスク仕様 を参照してください。本番モード（RISC0_DEV_MODE 未設定）では実際の STARK 証明が生成されます。

S3 アップロード

生成されたアーティファクトは、指数バックオフ付きのリトライ（最大 3 回、基底 2 秒）で S3 にアップロードされます。主にアップロードされるファイルは以下です。

配布と callback 復元の主経路は bundle.zip 内の receipt.json / journal.json / 公開監査アーティファクトです。bitmap artifact は利用可能な場合に sibling object として callback から追加復元されます。配布経路の詳細は バンドル構造 を参照してください。

SQS キュー設計

ワークキュー

デッドレターキュー（DLQ）

3 回の受信失敗後、メッセージは DLQ に移動されます。DLQ のメッセージ保持期間は 14 日で、手動での障害調査と再処理に使用されます。

ECS Fargate タスク仕様

ARM64 アーキテクチャの選択は、RISC Zero の STARK 証明生成における Graviton プロセッサのコスト効率に基づいています。非 GPU 前提のこの構成は PoC の意図的な制約です。詳細は PoC の意図的な制約 > 非 GPU 前提の証明実行 を参照してください。

クライアント側のポーリング

非同期証明の進捗は、クライアントが GET /api/sessions/:id/status を X-Session-Capability 付きでポーリングして確認します。

stateDiagram-v2
  [*] --> pending: POST /api/finalize → 202
  pending --> running: dispatch-proxy が SFN を起動
  running --> succeeded: callback-runner が結果を書き込み
  running --> failed: エラー発生
  succeeded --> [*]
  failed --> [*]

注: prover-dispatch-proxy が Step Functions 起動前に失敗した場合、コールバックが走らないため pending のまま再試行/DLQ 待ちになることがあります。dispatch 前提条件や contract generation の互換チェックで非再試行扱いになる条件はフェーズ 2を参照してください。

障害時の調査導線

非同期証明がスタックした場合の最小調査パスです。

flowchart TD
  START["finalize がスタック"] --> Q1{"SQS に<br/>メッセージあり?"}
  Q1 -->|No| A1["API → SQS の送信を確認<br/>環境変数 PROVER_WORK_QUEUE_URL"]
  Q1 -->|Yes| Q2{"dispatch-proxy<br/>ログに成功あり?"}
  Q2 -->|No| A2["Lambda ログを確認<br/>SQS → Lambda のトリガー設定"]
  Q2 -->|Yes| Q3{"SFN の<br/>実行状態は?"}
  Q3 -->|署名失敗| A3["ECR イメージ署名を確認<br/>Signer プロファイル設定"]
  Q3 -->|ECS 失敗| Q4{"ECS タスク<br/>ログに出力あり?"}
  Q4 -->|No| A4["タスク起動失敗<br/>IAM / サブネット / イメージ URI"]
  Q4 -->|Yes| A5["エントリポイントエラーを確認<br/>入力検証 / プローバー実行"]
  Q3 -->|コールバック失敗| A6["callback-runner ログを確認<br/>AppSync 書き込み権限"]

関連する章

• バンドル構造 — bundle.zip と隣接オブジェクトの公開境界
• イメージ署名 — Step Functions 内の署名検証ステップの詳細
• Image ID — プローバーイメージと Image ID の対応関係

イメージ署名

AWS Signer でプローバーイメージを署名し、ECS 実行前にゲートとして検証する仕組みを扱う章です。

STARK 証明は「特定のゲストプログラムが正しく実行された」ことを保証しますが、そもそもそのゲストプログラムを含むコンテナイメージ自体が改ざんされていないことも保証する必要があります。イメージ署名は、信頼されたビルドパイプラインが生成したイメージのみが証明生成に使用されることを担保するセキュリティゲートです。

脅威モデル

署名なしの場合、未承認イメージへの差し替えは検証段階の Image ID 照合や STARK レシート検証で拒否され得るものの、証明生成インフラ上で未承認イメージが実行されること自体は起動前に止められません。署名ありの場合は、Step Functions が起動前に署名ステータスを確認し、署名なし/未完了であればタスク起動を拒否します。

STARK 証明は Image ID（ゲストバイナリの暗号的識別子）に紐づきますが、イメージ署名はそれとは別レイヤで「未承認コンテナイメージの実行」を起動前に抑止します。両者は相補的な防御です。

署名フロー

ビルドと署名

CodeBuild がプローバーコンテナイメージをビルドし、ビルド済み ARM64 コンテナから host --print-image-id --json を実行して guest ImageID と methodVersion を抽出します。その後 ECR に push し、ECR 上で解決されたイメージ digest、digest 固定 URI、ImageID、methodVersion、Git SHA、RISC Zero toolchain image を image-metadata.json として出力します。その digest を運用手順で Terraform の ecs_image_uri に反映し、Step Functions は digest 固定のイメージ参照に対して署名ステータスを確認します。 ECR マネージド署名が有効な環境では、push 後に AWS Signer プロファイルに基づく署名ステータスが対象 digest に付与されます。

sequenceDiagram
  participant GH as GitHub
  participant CB as CodeBuild
  participant ECR as ECR
  participant SGN as AWS Signer

  GH->>CB: ソースコード取得
  CB->>CB: Docker イメージビルド<br/>(ARM64)
  CB->>CB: ImageID / methodVersion 抽出
  CB->>ECR: イメージをプッシュ<br/>(タグ付き)
  ECR-->>CB: digest を解決<br/>metadata 出力
  CB->>CB: image-metadata.json 生成
  ECR->>SGN: （ECR managed signing 有効時）署名処理
  SGN->>ECR: 署名ステータス更新
  Note over ECR: deploy/runtime では<br/>Terraform に反映した digest 固定で参照

注: このリポジトリでコード化されているのは署名ステータス確認（DescribeImageSigningStatus）です。
署名付与そのもの（ECR managed signing の有効化）は、ECR 側の設定・運用が前提です。

CodeBuild の build/push では運用上のタグを使用できますが、Terraform に渡す ecs_image_uri と Step Functions が署名確認する対象は常にダイジェスト固定（@sha256:<64-hex>）です。これにより、タグの上書きによるイメージのすり替えを防止します。ベースとなる RISC Zero ツールチェーンイメージも同様に、ECR 上のタグから digest を解決した RISC0_TOOLCHAIN_IMAGE として Docker build に渡され、非 digest 形式は buildspec 側で拒否されます。

生成された image-metadata.json は、S3 metadata bucket の prover-images/<env>/latest.json、prover-images/<env>/by-digest/sha256-<digest>.json、prover-images/<env>/by-git-sha/<sha>.json に保存されます。さらに SSM Parameter Store の current pointer に同じ候補 metadata JSON を書き込み、ImageID と digest 固定 URI が別々にずれないようにします。これらは昇格前の候補であり、運用では ECR 署名ステータスと必要な proof smoke を確認してから imageId-mapping.json と Terraform の ecs_image_uri に反映します。

実行前確認

Step Functions ステートマシンの最初のステートで、check-image-signature Lambda がイメージの署名ステータスを確認します。

stateDiagram-v2
  [*] --> VerifyImageSignature: Step Functions 開始
  VerifyImageSignature --> CheckImageSignature

  state CheckImageSignature <<choice>>
  CheckImageSignature --> RunProver: status = COMPLETE
  CheckImageSignature --> FinalizeSignatureFailed: status ≠ COMPLETE

  state FinalizeSignatureFailed {
    [*] --> CallbackFailed: エラー情報を通知
  }

  state RunProver {
    [*] --> ECSTask: 署名ステータス確認済みイメージで実行
  }

check-image-signature Lambda は以下の処理を行います。

1. ECR の DescribeImageSigningStatus API を呼び出す
2. 指定されたリポジトリ名とイメージダイジェストに対する署名ステータスを取得
3. 取得した status（COMPLETE / それ以外）を Step Functions に返す

署名ステータスが COMPLETE でない場合、Step Functions の Choice ステートが FinalizeSignatureFailed に遷移し、コールバック Lambda に ImageSignatureVerificationFailed エラーを通知します。ECS タスクは一切起動されません。

ステータス確認と暗号学的検証の違い 本システムの実行前チェックは ECR の DescribeImageSigningStatus が返すステータス参照であり、署名値そのものの暗号学的検証（証明書チェーン検証など）は行いません。独立検証が必要な場合は Notation などの外部ツールを併用してください。

ECR リポジトリとイメージ管理

リポジトリ構成

両リポジトリとも、プッシュ時の脆弱性スキャン（Scan on Push）が有効です。

ダイジェスト固定

Terraform の ecs_image_uri 変数には、ダイジェスト固定の URI のみが許可されます。バリデーションルールにより @sha256:<64-hex> 形式が強制されます。

Step Functions の定義に含まれるイメージダイジェストは、Terraform の変数から以下のように抽出されます。

• リポジトリ名: URI の @ より前の部分からレジストリホストを除去
• ダイジェスト: URI の @ より後の部分（sha256:...）

この分解により、check-image-signature Lambda は正確なリポジトリとダイジェストの組み合わせで署名ステータスを確認できます。

ビルドパイプライン

CodeBuild プロジェクト

2 つの CodeBuild プロジェクトがイメージのビルドを担当します。

RISC Zero ツールチェーンのビルドは低頻度（ツールチェーンバージョン更新時のみ）ですが、ビルドに時間を要するため Large インスタンスと長いタイムアウトが設定されています。

CodeBuild の IAM 権限

CodeBuild ロールには以下の権限が付与されています。

Image ID との関係

イメージ署名と Image ID は異なるレイヤのセキュリティメカニズムですが、共に「正しいプログラムが実行されたこと」の信頼チェーンを構成します。

flowchart TD
  subgraph "ビルド時"
    BUILD["コンテナイメージ<br/>ビルド"] --> SIGN["ECR managed signing<br/>(運用設定)"]
    BUILD --> IMGID["ARM64 ImageID / methodVersion 抽出"]
    IMGID --> META["candidate metadata<br/>(S3 + SSM current)"]
    META --> PROMOTE["mapping / Terraform 値へ昇格"]
    PROMOTE --> MAP["imageId-mapping.json<br/>と ecs_image_uri に反映"]
  end

  subgraph "実行時"
    VERIFY_SIG["イメージ署名ステータス確認<br/>(Step Functions)"] --> RUN["プローバー実行"]
    RUN --> RECEIPT["レシート生成<br/>(Image ID を含む)"]
  end

  subgraph "検証時"
    RECEIPT --> VERIFY_RECEIPT["レシート検証<br/>(verifier-service)"]
    MAP --> VERIFY_RECEIPT
    VERIFY_RECEIPT --> MATCH{"Image ID<br/>一致?"}
  end

  SIGN --> VERIFY_SIG

候補 metadata から imageId-mapping.json / ecs_image_uri への昇格手順はビルドと署名に記載しています。

Terraform

Terraform で非同期プローバーインフラを宣言的に管理する構成、ワークスペース運用、Amplify 管理領域との連携点を扱う章です。

Terraform は、証明生成パイプラインに関わる AWS リソース（ECS、Step Functions、SQS、S3、ECR、CodeBuild、VPC、Lambda、IAM、CloudWatch、CloudTrail、SSM Parameter）を宣言的に管理します。Amplify Gen 2 管理領域との連携点は本章末の Amplify との連携ポイント を参照してください。

ディレクトリ構成

Terraform の構成ファイルは terraform/ ディレクトリに配置され、機能別に分割されています。

環境分離

ワークスペース戦略

develop と main の 2 環境を、Terraform ワークスペースと git 管理外の *.local.tfvars ファイルの組み合わせで管理します。

flowchart LR
  subgraph "Terraform State"
    S3["S3 バケット<br/>terraform-state"]
    S3 --> DEV["develop<br/>workspace"]
    S3 --> MAIN["main<br/>workspace"]
  end

  subgraph "local tfvars"
    DEVF["develop.local.tfvars"]
    MAINF["main.local.tfvars"]
  end

  DEVF --> DEV
  MAINF --> MAIN

environment 変数はバリデーションにより develop または main のみが許可されます。環境ごとの差分は locals で定義された設定マップにより解決されます。

ワークスペースの確認

環境の取り違えを防ぐため、操作前にワークスペースの確認が推奨されます。

ステート管理

S3 バックエンド

Terraform ステートは S3 バケットに保存され、use_lockfile = true による S3 lockfile でステートの同時変更を防止します。tracked の backend.tf は partial backend として backend "s3" {} だけを持ち、bucket や region は backend.local.hcl から terraform init に渡します。

named workspace ごとに state path と lockfile path は分かれますが、同じ backend bucket と root module を共有し、bootstrap・共有リソース・環境別 prover runtime が同居しています。長期運用では state と lifecycle の粒度に課題が残ります。経緯と改善候補は 設計ふりかえり § 7 を参照してください。

認証方式

Terraform の実行は STS AssumeRole を前提とし、現行の標準フローでは terraform-admin assumed role で実行します。aws_account_id は AWS provider の allowed_account_ids に渡され、principal_guard.tf は実行 principal が assumed-role/terraform-admin/* に一致しない場合に fail-fast します。

flowchart LR
  EXEC["実行環境<br/>(ローカル/CI)"] --> STS["AWS STS<br/>AssumeRole"]
  STS --> ROLE["Terraform 実行ロール<br/>IAM ロール"]
  ROLE --> TF["Terraform 実行"]

plan / apply は scripts/terraform/terraform-guarded.sh 経由で実行します。この wrapper は AWS caller、account ID、Terraform workspace、*.local.tfvars の environment を確認してから Terraform を起動します。

主要な入力変数

Terraform の実行に必要な変数と、そのバリデーションルールの概要です。

必須変数

*_arn / *_location の各変数は、sanitized placeholder を弾くバリデーションが入っているため、実値の注入が前提です。現行の CodeBuild source は GITHUB タイプ（location 指定）で構成されています。

オプション変数

tracked の develop.tfvars / main.tfvars は値の形を示す placeholder です。実運用では .env.local または shell 環境から pnpm terraform:backend / pnpm terraform:tfvars:develop / pnpm terraform:tfvars:main で backend.local.hcl と *.local.tfvars を生成します。

出力値

Terraform の出力値は、Amplify 環境変数や運用ツールから参照されます。

IAM 設計

最小権限の原則に基づき、各コンポーネントに専用の IAM ロールが割り当てられています。

flowchart TD
  subgraph "信頼されるサービス (Service Principal)"
    ECSSVC["ecs-tasks.amazonaws.com"]
    STATESVC["states.${aws_region}.amazonaws.com"]
    CBSVC["codebuild.amazonaws.com"]
    LAMSVC["lambda.amazonaws.com"]
  end

  subgraph "IAM ロール"
    ETE["ecs_task_execution"]
    ET["ecs_task"]
    SFN["step_functions"]
    CB["codebuild"]
    CBT["codebuild_risc0_toolchain"]
    CIS["check_image_signature"]
    CTL["cloudtrail_logs<br/>(main only)"]
  end

  ECSSVC --> ETE
  ECSSVC --> ET
  STATESVC --> SFN
  CBSVC --> CB
  CBSVC --> CBT
  LAMSVC --> CIS
  CTSVC["cloudtrail.amazonaws.com"] --> CTL

スコープの制限

• ECS タスクロールの S3 権限は var.s3_proof_prefix 配下に制限（既定: sessions/*）
• Step Functions ロールの ECS 権限は特定クラスター ARN に制限
• Step Functions ロールの iam:PassRole は ECS 関連ロールのみに制限
• Step Functions ロールの EventBridge 権限は ecs:runTask.sync の managed rule 操作用
• CodeBuild ロールの metadata 書き込みは prover image metadata バケット配下と現行 metadata SSM Parameter に制限

Amplify との連携ポイント

Terraform と Amplify は別系統で管理され、以下のポイントで手動同期を含む連携が残っています。

flowchart TB
  subgraph TF["Terraform"]
    SFN_ARN["Step Functions ARN"]
    SQS_ARN["SQS キュー ARN"]
    SQS_URL["SQS キュー URL"]
    S3_NAME["S3 バケット名"]
    CB_INPUT["入力変数<br/>finalize_callback_lambda_arn"]
  end

  subgraph AMP["Amplify"]
    ENV["環境変数"]
    CB_ARN["finalize-callback-runner<br/>Lambda ARN"]
  end

  SFN_ARN --> ENV
  SQS_ARN --> ENV
  SQS_URL --> ENV
  S3_NAME --> ENV
  CB_ARN -. "IaC input" .-> CB_INPUT

この双方向の参照により、Amplify が管理する Lambda を Terraform が管理する Step Functions から呼び出します。Terraform 出力 → Amplify 環境変数は手動同期のため、出力を変更した場合は Amplify 側の app-level / branch override の実効値も合わせて確認してください。

バージョン制約

API リファレンス

この章では、公開ドキュメントとして扱うべき API（ブラウザクライアントと第三者検証で利用するエンドポイント）を、現行実装ベースで説明します。

この部に含まれる章

• エンドポイント一覧 — 外部クライアント向け API のリクエスト/レスポンス仕様
• セッションライフサイクル — クライアントとサーバーのセッション管理実装

想定読者と前提

• 想定読者: ブラウザクライアントや第三者検証ツールから API を呼び出す実装者
• 前提: HTTP / セッションヘッダーの基本と、本書 全体像 のフローを把握していること

本章で扱わないもの

• 内部運用/デバッグ向け API（/api/debug/*、/api/finalize/callback）の詳細
• レート制限・Turnstile・capability TTL などの環境変数チューニング
• Amplify / Hono / Lambda 側の認可・ルーティング実装

関連する章

• 検証パイプライン — /api/verify が返す検証ペイロードの内訳
• 第三者検証ガイド — bundle.zip の取得とローカル監査
• 用語集 — capability トークン・session-scoped API の用語定義

エンドポイント一覧

この文書は、外部クライアント向け API のレスポンス形状・要件を現行実装ベースで記載します。session-scoped / capability 保護 API も含むため、無認証公開 API ではありません。

対象外（内部向け）

以下は内部運用/デバッグ用途のため、この文書の詳細対象外です。

• GET /api/debug/enable
• POST /api/finalize/callback

デュアルランタイム構成