はじめに

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

目的

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

想定読者

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

本書の読み方

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

全体像

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

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

コアコンセプト

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

各章への案内

暗号プロトコル

STARK Ballot Simulator で使用する暗号プリミティブとプロトコルの設計を解説します。

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

この部に含まれる章

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

コミットメントスキーム

投票者の選択を秘匿しつつ束縛するコミットメントスキームの設計を解説します。

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

概要

投票コミットメントは、投票者が選んだ選択肢を秘密にしたまま、その選択に束縛されることを可能にする暗号プリミティブです。投票時にはコミットメント値のみが掲示板に公開され、選択肢自体は検証段階まで秘匿されます。

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" は、このコミットメントが他のプロトコルで使用されるハッシュ値と偶発的に衝突することを防ぐための仕組みです。

ドメイン分離は本システムの全暗号プリミティブに一貫して適用されています。

安全性

Hiding（秘匿性）

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

前提条件:

• 乱数は暗号学的に安全な乱数生成器（CSPRNG）から生成される
• 同じ乱数は決して再利用しない

乱数の再利用は hiding 性を破壊します。同一選挙で同一乱数を使用した場合、同じ選択肢であればコミットメント値が一致してしまい、情報が漏洩します。

Binding（束縛性）

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

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

TypeScript と Rust の実装同期

コミットメントは TypeScript（クライアント・サーバー）と Rust（zkVM ゲスト）の双方で計算されます。これら 2 つの実装は、バイトレベルで完全に同一の出力を生成する必要があります。

同期が必要な要素:

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

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

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

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

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

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

CT Merkle ツリー

RFC 6962（Certificate Transparency）を参照した CT スタイルの追記専用 Merkle ツリーの設計を解説します。

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

概要

本システムの掲示板（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 のべき乗サイズのツリーが出現するため、MTH アルゴリズムの一般的な対応が必要です。

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

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

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

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

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

包含証明（Inclusion 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. 計算されたルートが期待するルートハッシュと一致するか確認

監査パスのサイズは 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）の前方互換的なプレフィックスであること、つまり追記専用性を暗号学的に証明するものです。

構造

SUBPROOF アルゴリズム

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

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

検証の意味

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

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

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

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

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

zkVM ゲストプログラムも同じハッシュ規則（0x00 リーフ、0x01 ノード、使用タグ）を用いて包含証明を検証します。ハッシュ規則の不一致は、ゲスト内での検証失敗として即座に検出されます。

RFC 6962 参照範囲

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

入力コミットメント

zkVM に渡す入力データ全体に対する正準エンコーディングとコミットメントの設計を解説します。

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

概要

入力コミットメントは、zkVM ゲストプログラムに渡されるすべての投票データ（コミットメント値と Merkle パス）を単一のハッシュ値に集約するプロトコルです。

このハッシュ値は zkVM のジャーナル（公開出力）にコミットされるため、第三者はジャーナルに記録された入力コミットメントと、公開されている投票データから再計算した値を照合することで、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 バイト

フィールド一覧

正準化規則

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

ソート規則

投票はインデックスの昇順にソートしてからエンコードする必要があります。

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

前提となる不変条件:

• 各投票の index は一意である（重複インデックスは不正入力）

重複インデックスが存在する入力はプロトコル違反であり、正常系の正準化対象ではありません。したがって、正準順序の主キーは index の昇順として定義されます。

実装上は、重複インデックスという異常入力に対して Rust 側で追加の tie-break（commitment と merklePath）を行いますが、これはあくまで異常系の決定性補助であり、正常系仕様を変更するものではありません。

エンディアン規則

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

16 進数正規化

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

TypeScript と Rust の同期

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

flowchart LR
  subgraph TypeScript
    TS_IN[公開入力データ] --> 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 が処理した入力データと公開されている入力データが異なることを意味し、結果の信頼性が根本的に損なわれます。

注意事項

入力コミットメントには投票者の秘密データ（選択肢や乱数）は含まれません。含まれるのはコミットメント値と Merkle パスのみであり、これらはすべて掲示板上で公開されているデータです。したがって、入力コミットメントの公開は投票の秘密性に影響しません。

STH ダイジェスト

Signed Tree Head (STH) ダイジェストによる分割ビュー攻撃の緩和メカニズムを解説します。

ログ 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 --> TP[第三者ソースに公開]

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

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

現行実装は第三者ソースへの照会（fetch）を行うものであり、アプリケーションが第三者ソースへ STH を自動公開する機能は含みません。

合意ロジック

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

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

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

zkVM との連携

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

この仕組みにより、STARK 証明が特定のツリー状態に対して生成されたことが保証されます。第三者はジャーナルの STH ダイジェストを独立ソースの値と照合することで、サーバーが証明と異なるツリー状態を提示していないかを確認できます。

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

STH ダイジェストの第三者検証は、Recorded-as-Cast 段階のチェックとして実行されます。

このチェックが有効化されている場合（STH ソースが設定されている場合）、合意が得られなければ「Verified」ステータスはブロックされます。

設定

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

STH ソースが未設定の場合、recorded_sth_third_party は not_run（未実行）となり、第三者照合は行いません。セキュリティ上は少なくとも 2 つ以上の独立ソースを設定することが推奨されます。

相対パス（例: /api/sth）はリクエスト元のオリジンに対して解決されます。

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

• NEXT_PUBLIC_STH_SOURCES=/api/sth
• NEXT_PUBLIC_STH_MIN_MATCHES=1

この設定は PoC の動作確認を優先したものです。本番運用では、独立した複数ソースと NEXT_PUBLIC_STH_MIN_MATCHES >= 2 を推奨します。

PoC における制約

本 PoC の開発用テンプレート（.env.local.example）では、STH ソースとして同一サーバー上の API エンドポイント（/api/sth）を使用します。実運用環境では、独立した組織が運営する複数のソースを使用する必要があります。同一サーバー上のソースのみでは、分割ビュー攻撃に対する防御力が限定的です。

ビットマップ Merkle

投票カウント証明のためのビットマップ Merkle ツリーの設計を解説します。

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

概要

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

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

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]
  end

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

ビットマップの構造

ビットマップの定義

ビットマップは、ツリーサイズ（投票数）と同じ長さのブール配列です。

• bitmap[i] = true: インデックス i の投票が正常に検証され、集計に含まれた
• bitmap[i] = false: インデックス i の投票が除外された（無効、欠損、または検証失敗）

本 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> の公開レスポンスは、以下の要素で構成されます:

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

ビット抽出

投票者は受け取ったチャンクから、自分が指定した 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

included = true であれば、自分の投票がカウントされたことを意味します。

検証手順

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

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

zkVM ゲストとの連携

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

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

1. 各投票に対してコミットメントの再計算と包含証明の検証を実施
2. 検証に成功した投票のインデックスに対応するビットを true に設定
3. ビットマップを LSB-first でパッキングし、32 バイトチャンクに分割
4. CT スタイルのハッシュ規則で Merkle ルートを計算
5. ルートをジャーナルにコミット

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

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

サーバーはビットマップ Merkle 証明を提供するために、最終化時に includedBitmap データを保持します。

現行 PoC 実装では、USE_MOCK_ZKVM=true かつ mock executor が実ビットマップを保持している場合に限り、その実ビットマップを使用します。これが利用できない場合は検証統計（validVotes など）から簡易ビットマップを再構成します。その後、どの経路で得たデータでもルート照合を行い、整合性を確認します。

安全性ゲート

サーバーが保持するビットマップデータから計算したルートと、ジャーナルの includedBitmapRoot が一致しない場合、ビットマップ証明の提供は無効化されます。これにより、サーバーが不正なビットマップデータを使って偽の証明を生成することを防止します。

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

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

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

チャンクレベルの情報漏洩

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

本 PoC では 64 票が 1 チャンクに収まるため、チャンクを受け取った投票者は全 64 票のカウント状態を知ることができます。

PoC における許容性

本システムでは 63 票がボット（自動投票）であり、ボットのカウント状態が開示されても実質的なプライバシー侵害は生じません。実運用環境で人間の投票者が多数参加する場合は、以下の対策を検討する必要があります:

• チャンクサイズの縮小（より多くのリーフ、より深いツリー）
• ゼロ知識証明を用いたビット開示の最小化
• 投票者の明示的な同意に基づく開示

zkVM 設計

RISC Zero zkVM を用いた集計証明パイプラインの全体設計を解説します。

ゲストプログラムが投票データを検証・集計し、ホストが STARK 証明を生成し、検証サービスがレシートを検証する一連のアーキテクチャにより、集計結果の正当性を暗号学的に保証します。

アーキテクチャ概要

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 秒で要点

RISC Zero zkVM 実装の要点（簡潔版）

RISC Zero の一次情報（zkVM specification / recursion docs）に沿って、実装上重要な点だけを抜粋すると次のとおりです。

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

ジャーナルとレシート

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

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

ジャーナルの各項目は、対応する STARK 証明（レシート検証）により「ゲストプログラムが計算した出力」であることが保証されます。項目ごとの意味と確認ポイントは次のとおりです。

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

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) の成功は強い保証ですが、それ単体で「全票が提示された」ことまでは保証しません。本 PoC では以下を組み合わせて最終判定します。

1. STARK 検証成功（正しいゲスト実行）
2. excludedCount == 0（除外票なし）
3. 一貫性証明・STH 整合の成功（設定時）
4. 必須チェックが not_run / running のままでは不合格

このため、Verified 表示は「証明 + 完全性チェック」がそろった場合にのみ成立します。

参考資料（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: 掲示板に追記
  B-->>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: レシート + 期待 Image ID
  VS->>VS: Receipt::verify(image_id)
  VS-->>S: 検証レポート
  S-->>V: 検証結果を提供

同期モードと非同期モード

ホストプログラムの実行には 2 つのモードがあります。

詳細は ホストと証明生成 を参照してください。

開発モードと本番モード

RISC Zero は RISC0_DEV_MODE 環境変数により、開発モードと本番モードを切り替えます。

開発モードで生成されたレシートは InnerReceipt::Fake 型となります。検証サービスでは通常 DevMode として扱いますが、image_id 不一致などの事前条件違反があれば Failed になります。本番環境でフェイクレシートが混入した場合は検証失敗です。

この部に含まれる章

• ゲストプログラム — zkVM 内で実行される検証・集計ロジック
• ホストと証明生成 — ホストプログラムと同期/非同期の証明パス
• 検証サービス — Rust ベースのレシート検証
• Image ID — ゲストバイナリの暗号的識別子と管理

ゲストプログラム

zkVM 内で実行されるゲストプログラムの設計を解説します。

ゲストプログラムは、投票コミットメントの再計算、RFC 6962 包含証明の検証、集計の実行、ビットマップルートの計算を行い、結果をジャーナルにコミットします。ゲスト内の全処理は STARK 証明により正当性が保証されるため、このプログラムが信頼の根幹となります。

概要

ゲストプログラムは 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{投票数 ≤<br/>ツリーサイズ?}
    I3 -->|No| FAIL
    I4 -->|Yes| NEXT[フェーズ 2 へ]
    I4 -->|No| FAIL
  end

  subgraph "フェーズ 2: 投票検証と集計"
    NEXT --> LOOP[各投票に対して]
    LOOP --> V1[6 段階検証]
    V1 -->|有効| TALLY[集計に加算]
    V1 -->|無効| EXCL[除外リストに追加]
    TALLY --> BIT[ビットマップ更新]
  end

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

投票の 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. 包含証明検証}
  C6 -->|失敗| INV
  C6 -->|成功| VALID[有効: 集計に加算]

1. インデックス範囲チェック

投票のインデックスが 0 以上 tree_size 未満であることを確認します。範囲外のインデックスは掲示板上に存在し得ないため、不正入力として検出されます。

2. インデックス重複チェック

同一インデックスの投票が既に処理されていないことを確認します。重複するインデックスは二重カウント攻撃を意味するため、2 番目以降の同一インデックスは除外されます。

3. 選択肢範囲チェック

選択肢の値が 0 から 4（A から E）の範囲内であることを確認します。

4. コミットメント再計算と照合

ゲスト内で投票者の（選択肢, 乱数, 選挙 ID）からコミットメントを再計算し、入力として渡されたコミットメント値と照合します。

この検証により、投票者が主張する選択肢が掲示板上のコミットメントと一致することが保証されます。コミットメントの計算規則は コミットメントスキーム を参照してください。

5. コミットメント重複チェック

同一コミットメントが既に処理されていないことを確認します。コミットメント値が重複した場合は、入力の異常または二重投入の兆候として無効化されます。

6. RFC 6962 包含証明検証

投票のコミットメントが掲示板 Merkle ツリーに含まれることを、RFC 6962 PATH 関数ベースの CT スタイル包含証明で検証します。投票のインデックスと Merkle パスから掲示板ルートを再計算し、入力の bulletin_root と一致するかを確認します。

ハッシュ規則は CT Merkle ツリー の RFC 6962 参照規則に合わせます:

• リーフ: SHA-256(0x00 || "stark-ballot:leaf|v1" || data)
• ノード: SHA-256(0x01 || left || right)

集計ロジック

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

• 集計は選択肢ごとの配列（5 要素）で管理
• 有効投票のインデックスに対応するビットマップのビットを true に設定
• 無効投票はカウントされず、ビットマップのビットも false のまま

三分類の除外モデル

ゲストプログラムは、ツリーサイズ分の全スロットを以下の 3 カテゴリに分類します。

flowchart LR
  TS["ツリーサイズ<br/>(全スロット)"]
  TS --> CNT["カウント済み<br/>countedIndices"]
  TS --> INV["無効<br/>invalidIndices"]
  TS --> MIS["欠損<br/>missingIndices"]

通常のファイナライズ経路（buildZkVMInputFromSession が生成する正規入力）では、これら 3 つの合計はツリーサイズと一致します:

countedIndices + invalidIndices + missingIndices = treeSize

実装上は、範囲外インデックスや重複インデックスを含む非正規入力が直接渡された場合、この恒等式が崩れる余地があります。公開検証では、通常フローで生成された入力を前提に扱います。

後方互換フィールドとして excludedCount も出力されます:

excludedCount = invalidIndices + missingIndices

excludedCount > 0 は検証失敗の決定的な指標です。1 票でも除外された場合、集計結果の完全性が損なわれていることを意味します。

ジャーナル出力

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

ジャーナルの信頼モデル

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

第三者はレシートの STARK 検証を行うだけで、上記の保証を取得できます。ゲストプログラムのロジックを信頼する必要はありますが、ホストやサーバーの正直性を信頼する必要はありません。

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

ゲストプログラムは投票検証と並行して、各インデックスのカウント状態を記録するビットマップを構築します。

1. ツリーサイズと同じ長さのブール配列を初期化（全 false）
2. 有効と判定された投票のインデックスに対応するビットを true に設定
3. ビットマップを LSB-first でバイト列にパッキング
4. 32 バイトチャンクに分割し、CT スタイルの Merkle ツリーを構築
5. ルート値（includedBitmapRoot）をジャーナルにコミット

ビットマップの詳細な構造とハッシュ規則は ビットマップ Merkle を参照してください。

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

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

入力コミットメント

ゲストに渡されたすべての投票データ（コミットメント値と Merkle パス）を正準エンコーディングで連結し、SHA-256 で圧縮します。第三者は公開された入力データから同じ値を再計算し、ジャーナルの値と照合することで、zkVM が処理した入力の同一性を検証できます。

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

STH ダイジェスト

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

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

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

ゲストプログラムにはバージョン番号が割り当てられ、ジャーナルの methodVersion フィールドに記録されます。現在のバージョンは 10（v1.0）です。

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

ホストと証明生成

ホストプログラムによる 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]
    VOTES["投票データ<br/>(選択肢, 乱数, コミットメント)"]
    BULL["掲示板<br/>(ルート履歴, 包含証明)"]
    LID[ログ ID]
  end

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

  EID --> EID2
  BULL --> BR
  BULL --> TS
  VOTES --> VWP
  LID --> LID2

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

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

Merkle パスの解決戦略

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

flowchart TD
  START[Merkle パス解決] --> P1{掲示板から<br/>包含証明を取得可能?}
  P1 -->|Yes| USE1[掲示板の証明を使用]
  P1 -->|No| P2{投票データに<br/>事前計算パスが存在?}
  P2 -->|Yes| CHK{proofMode = rfc6962<br/>かつ 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/ハッシュ文字列をバイト配列へ変換）。

出力ファイル

ホストバイナリは 2 つの JSON ファイルを出力します。

レシート JSON には image_id フィールドが含まれ、このゲストプログラムの Image ID が記録されます。検証サービスはこのフィールドを使用して、期待される Image ID との照合を行います。

同期モード

同期モードでは、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 を構築します。

非同期モード

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

sequenceDiagram
  participant S as サーバー
  participant SQS as SQS
  participant SFN as Step Functions
  participant ECS as ECS Fargate
  participant S3 as S3
  participant CB as コールバック Lambda

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

非同期モードの処理フロー

1. 入力の準備: ディスパッチ Lambda が入力 JSON を S3 にアップロードし、Step Functions 実行を開始
2. イメージ署名チェック: プローバーコンテナイメージの署名を検証し、承認されたイメージのみ実行を許可
3. プローバータスク: ECS Fargate タスクが起動し、S3 から入力をダウンロードしてホストバイナリを実行
4. 出力バンドル: レシート、ジャーナル、公開入力をバンドルし、S3 にアップロード
5. コールバック: 成功/失敗に応じてコールバック Lambda がセッションデータを更新

公開バンドルの構築

非同期モードでは、ホストバイナリの出力から公開バンドル（bundle.zip）を構築します。

input.json は秘密データを含むため、公開バンドルには含まれません。公開バンドルの構成については バンドル構造 を参照してください。

非同期モードの特性

開発モードの動作

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

flowchart TD
  ENV{RISC0_DEV_MODE?}
  ENV -->|"= 1"| DEV["開発モード<br/>フェイクレシート生成<br/>約 100ms"]
  ENV -->|未設定| PROD["本番モード<br/>STARK 証明生成<br/>約 370 秒"]
  DEV --> FAKE["InnerReceipt::Fake"]
  PROD --> REAL["InnerReceipt::Composite<br/>+ seal データ"]

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

• ローカル開発での高速フィードバック
• E2E テストの高速実行
• UI 開発時のモック

開発モードのレシートは 検証サービス で Fake として検出され、通常は DevMode 扱いになります（image_id 不一致などの事前条件違反時は Failed）。いずれにせよ本番モードの検証基準は満たしません。

検証サービス

Rust ベースの STARK レシート検証サービスの設計を解説します。

Receipt::verify(expected_image_id) により、レシートが期待されるゲストプログラムの実行結果であることをサーバー側で検証します。検証結果はレポートとして永続化され、クライアントに提供されます。

概要

検証サービスは、ホストプログラムが生成したレシートの STARK 検証をサーバー側で行う Rust ベースのコンポーネントです。

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

flowchart LR
  subgraph 入力
    RCP[レシート JSON]
    EID["期待 Image ID"]
  end

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

検証フロー

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

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

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

1. レシートの読み込みとパース

検証サービスは複数のレシート形式に対応しています。

2. 開発モードの検出

レシートの内部構造（InnerReceipt）がフェイク（Fake）型の場合、開発モードで生成されたレシートとして扱います。開発モードのレシートは本物の STARK 証明としては成立しません。

ただし、Fake 検出だけで即 dev_mode にはなりません。Image ID メタデータが不一致の場合は failed となります。照合後の Receipt::verify() で Fake レシートが InvalidProof を返したケースは dev_mode として分類します。

補足として、image_id メタデータが欠落している場合は、非 Fake レシートでは failed、Fake レシートでは Receipt::verify() の結果（通常 InvalidProof）に基づいて dev_mode になる経路があります。

3. Image ID の照合

レシート JSON のメタデータ image_id を期待値と照合します。不一致は failed として即時拒否され、Receipt::verify() には進みません。

この事前チェックにより、異なるゲストプログラムで生成されたレシートを早期に拒否できます。Image ID の管理については Image ID を参照してください。

4. STARK 検証の実行

Image ID の照合に成功した後、RISC Zero SDK の Receipt::verify() メソッドを使用して STARK 証明の暗号学的検証を行います。

この検証は以下のことを証明します:

• レシートに含まれる seal（証明データ）が有効である
• ジャーナルの内容が、指定された Image ID のゲストプログラムの正当な実行結果である
• 証明の生成時にデータの改ざんが行われていない

検証レポート

検証サービスは検証結果を構造化されたレポートとして出力します。

ステータスの判定基準

flowchart TD
  S{検証結果}
  S -->|"metadata image_id 不一致"| F1["failed<br/>errors: image_id_mismatch"]
  S -->|"Receipt::verify 成功 + 非 Fake"| OK["success"]
  S -->|"Receipt::verify 成功 + Fake"| DM["dev_mode"]
  S -->|"Receipt::verify 失敗 + Fake + InvalidProof"| DM2["dev_mode"]
  S -->|"Receipt::verify 失敗（その他）"| F2["failed<br/>errors: verification_failed"]

デプロイメントモデル

検証サービス（Rust バイナリ verifier-service）は、呼び出し経路ごとに実行場所が異なります。

• 同期ファイナライズ（POST /api/finalize）: real executor 利用時のみ API サーバープロセスがローカルに配置されたバイナリを直接実行（mock executor 利用時は verifier-service を呼ばず dev_mode 扱い）
• 明示的検証（POST /api/verification/run）: verifier-service-runner Lambda が S3 バンドルを展開してバイナリを実行

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->>RUNNER: 実行要求（sessionId, executionId, expectedImageId）
  RUNNER->>S3: レシートバンドルを取得・展開
  RUNNER->>VS: レシート + 期待 Image ID
  VS->>VS: STARK 検証実行
  VS-->>RUNNER: 検証レポート
  RUNNER-->>API: 検証レポート
  API->>API: verification.json として保存
  API-->>C: 検証結果

呼び出しパターン

検証サービスの呼び出しには 2 つのパターンがあります。

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

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

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

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

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

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

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

• STARK 証明自体は公開データ: レシートと Image ID が公開されていれば、第三者が独立に検証可能
• 検証サービスは利便性のための委任: ブラウザでの STARK 検証が実用的になれば、クライアント側検証に移行可能
• 公開バンドル: レシートと公開入力は ZIP ローカル検証（Ubuntu） の手順で独立検証できる

verification.json の非公開性

verification.json は公開バンドル（bundle.zip）には含まれません。必要に応じてレポート用エンドポイント経由で配布されますが、第三者検証ではレシートファイルを直接使った独立検証が推奨されます。

Image ID

zkVM ゲストバイナリの暗号的識別子（Image ID）の管理と検証を解説します。

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

概要

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

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

本システムでは、同一バージョンのゲストに対して ARM64 用 (expectedImageID) と x86_64 用 (expectedImageID_x86_64) の 2 つの Image ID をマッピング上で管理できます。

ただし、実行時の自動解決は「WSL 環境なら expectedImageID_x86_64 を優先する」というルールです。WSL 以外では expectedImageID が選ばれます。WSL 以外の x86_64 環境で x86_64 用 Image ID を使う場合は、EXPECTED_IMAGE_ID で明示オーバーライドします。

Image ID マッピング

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

マッピングの構造

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

バージョン履歴の管理

マッピングファイルはバージョンの履歴を保持します。current フィールドが現在有効なバージョンを指し、deprecated フィールドが過去のバージョンを列挙します。

flowchart LR
  subgraph マッピングファイル
    V8["v8<br/>(deprecated)"]
    V9["v9<br/>(deprecated)"]
    V10["v10<br/>(current)"]
  end

  V10 --> ARM["ARM64 Image ID"]
  V10 --> X86["x86_64 Image ID"]

Image ID の解決

検証時に使用する期待 Image ID は、以下の優先順位で解決されます。

flowchart TD
  START[Image ID 解決] --> P1{環境変数<br/>EXPECTED_IMAGE_ID<br/>が設定されている?}
  P1 -->|Yes| USE1[環境変数の値を使用]
  P1 -->|No| LOAD[マッピングファイルを読み込み]
  LOAD --> P2{読み込み成功?}
  P2 -->|No| ERR[既定値へフォールバック]
  P2 -->|Yes| P3{WSL 実行環境かつ<br/>expectedImageID_x86_64 が存在?}
  P3 -->|Yes| X86[expectedImageID_x86_64 を使用]
  P3 -->|No| ARM[expectedImageID を使用]

1. 環境変数: EXPECTED_IMAGE_ID が設定されている場合、その値を使用
2. マッピングファイル: current バージョンの Image ID を取得し、WSL 実行環境かつ expectedImageID_x86_64 が存在する場合のみその値を使用（それ以外は expectedImageID）
3. フォールバック: マッピングの読み込みに失敗した場合は、実装内の既定値にフォールバック

環境変数によるオーバーライドは、デプロイパイプラインでの柔軟な制御や、テスト時の特定バージョン指定に使用されます。

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

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

stark_image_id_match チェック

このチェックは、レシートに記録された Image ID と期待値を照合します。

flowchart TD
  RID["レシートの Image ID"] --> CMP{一致?}
  EID["期待 Image ID<br/>(マッピングから取得)"] --> CMP
  CMP -->|一致| NEXT["stark_receipt_verify へ進む"]
  CMP -->|不一致| FAIL["検証失敗"]

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

Image ID の更新手順

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

1. ゲストコードを変更する
2. zkVM ゲストをビルドし、新しい Image ID を取得する
3. imageId-mapping.json を更新する（必要に応じて expectedImageID_x86_64 も更新）
4. プローバーイメージとマッピングを同時にデプロイする

更新の同期要件

Image ID の更新は、プローバーイメージのデプロイとマッピングファイルの更新を同時に行う必要があります。

非同期プローバーの場合、デプロイのローリングアップデート中に旧イメージのタスクが残存する可能性があるため、一時的に旧バージョンの Image ID も受け入れる遷移期間が必要になる場合があります。

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

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

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

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

検証パイプライン

STARK Ballot Simulator の検証パイプラインは、投票の完全性を 4 段階で検証するシステムです。各段階は独立した暗号的保証を提供し、いずれかの段階が失敗した場合でも、どの段階で何が問題かを特定可能にします。

設計原則

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

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

検証チェックが not_run（未実行）または running（実行中）の状態にある場合、システムは「Verified」を表示しません。証拠の不在を成功として扱わないという姿勢です。

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

excludedCount > 0（除外された投票が存在する）、整合性証明の失敗、第三者 STH 合意の不成立など、いずれかの必須チェックが失敗すれば、「Verified」表示は即座にブロックされます。

原則 3: チェック評価はサーバー中心、最終集約はクライアント

20 個の検証チェック（verificationChecks）は主にサーバー側（GET /api/verify）で評価されます。一方、最終的な Verified/Warning/Failed のサマリー集約はクライアント側（deriveVerificationSummary）で実行されます。STARK レシート検証はサーバー側の専用サービスで実行されます。validateVotingIntegrity は補助判定として実装されていますが、journal が取得できる場合にのみ実行されます（通常の /verify フローでは journal は省略）。

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

1. 段階の依存関係

flowchart TD
  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"]
  UI["結果表示"]

  S1 --> S2
  S2 --> S3
  S3 --> S4
  S4 --> UI

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

flowchart TD
  subgraph SERVER["サーバー側"]
    VFY["GET /api/verify<br/>Stage 1-3 を評価"]
    RUN["POST /api/verification/run<br/>Stage 4 を検証"]
  end

  subgraph CLIENT["クライアント（UI）"]
    UI["結果表示と最終サマリー集約<br/>（必要時に補助判定）"]
  end

  VFY --> UI
  RUN --> UI

検証の実行フロー

検証導線では、/result で STARK 検証を起動し、/verify で結果をポーリング表示します。

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

  U->>R: 「検証へ進む」をクリック
  R->>A: POST /api/verification/run（必要時）
  A->>VS: レシート + Image ID
  VS->>VS: Receipt::verify(imageId)
  VS-->>A: 検証レポート保存
  R-->>V: /verify へ遷移

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

  Note over V: クライアントは表示とシーケンス制御を実行

4 段階の概要

クライアントは verificationSteps / verificationChecks の表示と、verificationChecks からの最終サマリー集約を担当します。validateVotingIntegrity は journal が利用可能な場合にのみ実行できる補助判定です。

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

検証チェック数

パイプライン全体で 20 個の検証チェックが定義されており、各チェックには一意の ID が割り当てられています。

チェックの詳細は チェック一覧 を参照してください。

この部に含まれる章

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

4 段階検証モデル

E2E 検証可能投票の 4 段階検証モデルの設計と各段階の保証を解説します。

各段階は独立した暗号的保証を提供し、いずれかが失敗した場合でも、どの段階で何が問題かを特定可能にします。

段階間の依存関係

概念モデルとしては 4 段階を順に評価しますが、実装では GET /api/verify がチェック群をまとめて計算します。STARK ステータスによって Counted チェックが pending / not_run / failed にゲートされる（zkGate）ため、後段の評価可否に影響します。また、UI は STARK 解決後に段階表示を順次進めます。

現行実装では、各段階のチェック判定そのものは主に GET /api/verify 側で計算され、クライアントは結果の表示とシーケンス制御を担当します。validateVotingIntegrity は補助判定として存在しますが、通常の /verify 応答では journal が省略されるため常時実行される経路ではありません。

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

目的

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

検証する内容

現行実装では、GET /api/verify が投票時にセッションへ保存された 3 つの値（選挙 ID、選択肢、乱数）からコミットメントを再計算し、投票時のレシートに含まれるコミットメント値と照合します。暗号式自体は、投票者がローカルで再計算する Cast-as-Intended と同一です。

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

必要な証拠

失敗モード

限界

現行の /api/verify 経路では Cast-as-Intended はセッション保存済み証拠に依存します。セッション証拠を復元できない場合、この段階は not_run になり最終判定は Verified になりません。

Stage 2: Recorded-as-Cast

目的

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

検証する内容

この段階では 3 種類の検証を行います。

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

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

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

  IP --> RESULT{"全て成功?"}
  CP --> RESULT
  STH --> RESULT

2a: 包含証明（Inclusion Proof）

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

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

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

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

複数の独立した STH（Signed Tree Head）ソースに問い合わせ、比較可能な応答間で合意が成立しているかを確認します。照合の必須項目は STH ダイジェストで、bulletinRoot と treeSize は各ソースが返した場合に追加照合されます。これにより、サーバーが検証者ごとに異なるツリー状態を提示するスプリットビュー攻撃を検出します。

必要な証拠

失敗モード

Stage 3: Counted-as-Recorded

目的

掲示板に記録された全投票が、zkVM の集計処理に正しく含まれたことを確認します。投票の除外、欠落、重複がないことを検証し、集計結果の完全性を保証します。

検証する内容

flowchart TD
  START["Stage 3 開始"]
  G1["counted_missing_indices_zero<br/>excludedCount == 0"]
  G2["counted_expected_vs_tree_size<br/>totalExpected == treeSize"]
  G3["counted_input_commitment_match<br/>公開入力とジャーナルが一致"]
  G4["counted_my_vote_included<br/>ビットマップ証明で自票を確認"]
  OTHERS["残り required チェック<br/>counted_input_sanity<br/>counted_unique_indices<br/>counted_unique_commitments<br/>counted_tally_consistent"]
  PASS["Counted-as-Recorded: success"]
  FAIL["Counted-as-Recorded: failed"]

  START --> G1
  G1 -->|NG| FAIL
  G1 -->|OK| G2
  G2 -->|NG| FAIL
  G2 -->|OK| G3
  G3 -->|NG| FAIL
  G3 -->|OK| G4
  G4 -->|NG| FAIL
  G4 -->|OK| OTHERS
  OTHERS -->|all success| PASS
  OTHERS -->|any failed| FAIL

flowchart TD
  PUB["公開系チェック (4)<br/>counted_input_sanity<br/>counted_unique_indices<br/>counted_unique_commitments<br/>counted_input_commitment_match"]
  ZK["zk 系チェック (4)<br/>counted_tally_consistent<br/>counted_missing_indices_zero<br/>counted_expected_vs_tree_size<br/>counted_my_vote_included"]
  RESULT{"全 8 required チェックが success?"}
  PASS["Stage 3 を通過"]
  FAIL["Verified をブロック"]

  PUB --> RESULT
  ZK --> RESULT
  RESULT -->|Yes| PASS
  RESULT -->|No| FAIL

必要な証拠

通常の UI フローでは includeJournal=1 を付けないため、Counted チェックは上位フィールドと publicInputSummary を主に使用します。

重要な判定: excludedCount

excludedCount（除外された投票の数）は、本システムにおいて最も重要な不変条件の一つです。

• excludedCount == 0: 全投票が集計に含まれた（正常）
• excludedCount > 0: 一部の投票が集計から除外された（即座に検証失敗）

この値が 0 でない場合、counted_missing_indices_zero が failed になり、最終サマリー判定は「Verified」を表示しません。

失敗モード

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 照合: レシートに記録された Image ID が、デプロイ済みの期待 Image ID と一致するかを確認します。Image ID はゲストプログラムのバイナリから導出される暗号的識別子であり、ゲストプログラムが改変されていないことを保証します。

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

必要な証拠

開発モードの検出

RISC0_DEV_MODE=1 で生成されたレシートは InnerReceipt::Fake 型であり、暗号学的な保証を持ちません。検証サービスはこれを dev_mode ステータスとして報告します。チェック評価では、設定に応じて dev_mode は success または not_run に正規化されます（既定では not_run 側）。

失敗モード

段階ステータスの集約

各段階のステータスは、その段階に属するチェックの結果から導出されます。

最終的な「Verified」表示の判定は、4 段階の結果に加えて追加のゲーティング条件を適用します。詳細は ゲーティングロジック を参照してください。

チェック一覧

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

各チェックは一意の ID を持ち、success / failed / not_run / running / pending のステータスで管理されます。not_run のチェックが残っている場合、「Verified」は表示されません。

チェックの属性

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

証拠種別

重要度

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

投票者の意図通りにコミットメントが生成されたかを検証するチェック群です。 現行実装では、このカテゴリの入力は /api/verify が返す voteReceipt / userVote（セッション復元データ）を起点に評価されます。

判定ロジックの詳細

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

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

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

cast_commitment_match: 投票時データ（選挙 ID、選択肢、乱数）からコミットメントを再計算し、レシートのコミットメント値と照合します。ドメインタグ "stark-ballot:commit|v1.0" を含む正準フォーマットに従います。

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

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

判定ロジックの詳細

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 包含証明（監査パス）を検証します。リーフハッシュと監査パスからルートを再計算し、期待するルートハッシュと照合します。

recorded_consistency_proof: 投票時のツリー（oldSize, oldRoot）から最終ツリー（newSize, newRoot）への RFC 6962 整合性証明を検証します。この証明は、古いツリーが新しいツリーの追記専用プレフィックスであることを保証します。

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

このチェック定義の criticality は optional ですが、サマリー判定では STH ソースが設定されている場合に実質的な必須条件として扱われます。

派生チェックについて

recorded_commitment_in_bulletin と recorded_root_at_cast_consistent は、それぞれ recorded_inclusion_proof と recorded_consistency_proof から結果を派生します。これは、包含証明の検証成功がそのまま「コミットメントの存在」の証明となり、整合性証明の検証成功がそのまま「ルートの一貫性」の証明となるためです。

派生チェックの重要度が optional であるのは、派生元の required チェックが既にカバーしているためです。

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

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

判定ロジックの詳細

counted_input_sanity: 公開入力サマリー（publicInputSummary）が存在し、必要なフィールド（選挙 ID、掲示板ルート、ツリーサイズ、投票数等）を含んでいることを確認します。

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: zkVM ジャーナルの excludedCount が 0 であることを確認します。このチェックは本システムの最重要不変条件であり、0 でない場合は即座に検証を失敗とします。

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

counted_my_vote_included: ビットマップ Merkle 証明を検証し、投票者のインデックスに対応するビットが 1（集計に含まれた）であることを確認します。サーバーから取得した leafChunk と auditPath を使用し、ビットマップルートまでの Merkle パスを検証します。

counted_input_commitment_match: 公開入力から入力コミットメント（全投票 + Merkle パスの正準ハッシュ）を計算し、zkVM ジャーナルに記録された入力コミットメント値と照合します。一致すれば、zkVM が公開入力と同一のデータを処理したことが保証されます。

STARK Verification（2 チェック）

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

判定ロジックの詳細

stark_image_id_match: レシートに記録された Image ID が、imageId-mapping.json で定義された期待 Image ID と一致することを確認します。不一致は、異なるゲストプログラムで生成された証明であることを示します。

stark_receipt_verify: サーバー側の Rust 検証サービスが Receipt::verify(image_id) を実行し、Seal（STARK 証明）が暗号学的に正当であることを確認します。チェック結果としては success / failed / not_run / running が使われ、dev_mode は許可設定に応じて success または not_run に正規化されます。

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

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

全チェック早見表

バンドル構造

証明バンドル（proof bundle）の構成と公開・非公開アーティファクトの区分を解説します。

同期モードと非同期モードで生成されるバンドルの構成、公開許可リスト、および非公開アーティファクト（input.json, verification.json）の保護について説明します。

概要

証明バンドルは、zkVM の実行結果を検証可能な形で保存・配布するためのアーティファクト群です。バンドルには公開可能なファイルと非公開ファイルが含まれ、厳格な許可リストによって第三者に公開するファイルが制御されます。

flowchart TB
  subgraph "バンドルディレクトリ"
    subgraph "公開アーティファクト"
      PI["public-input.json<br/>公開入力"]
      RC["receipt.json<br/>STARK レシート"]
      JN["journal.json<br/>zkVM ジャーナル"]
      MT["metadata.json<br/>メタデータ"]
      STH["sth.json<br/>STH スナップショット"]
      CP["consistency-proof.json<br/>整合性証明"]
    end

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

    BZ["bundle.zip<br/>公開アーカイブ"]
  end

  PI --> BZ
  RC --> BZ
  JN --> BZ
  MT --> BZ
  STH -.-> BZ
  CP -.-> BZ
  IN -.-x BZ
  VR -.-x BZ

公開許可リスト

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

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

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

非公開アーティファクト

input.json は zkVM ゲストへの完全な入力であり、個々の投票者の選択肢と乱数が含まれます。これが公開されると、投票の秘匿性が失われます。verification.json は bundle.zip の公開配布対象ではなく、必要時のみ専用エンドポイント経由で扱います。

公開入力の構造

public-input.json は、input.json（秘匿入力）から秘密情報を除外した公開版です。

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

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

証明生成には同期モード（ローカル実行）と非同期モード（ECS Fargate）の 2 つのパスがあり、生成されるバンドルの構成が異なります。

flowchart LR
  subgraph "同期モード"
    S1["ローカルプロセスで<br/>ホストバイナリ実行"]
    S2["TypeScript で<br/>全アーティファクト生成"]
    S3["検証サービスを呼び出し<br/>verification.json を保存"]
    S4["許可リストで<br/>bundle.zip を作成"]
    S1 --> S2 --> S3 --> S4
  end

  subgraph "非同期モード"
    A1["ECS Fargate で<br/>ホストバイナリ実行"]
    A2["entrypoint.sh で<br/>公開アーティファクト生成"]
    A3["bundle.zip を<br/>S3 にアップロード"]
    A4["コールバック Lambda で<br/>結果をセッションに保存"]
    A1 --> A2 --> A3 --> A4
  end

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

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

1. S3 から入力 JSON をダウンロード
2. ホストバイナリを実行し、レシートと出力を生成
3. 出力から journal.json を変換生成
4. 入力と出力から public-input.json を構築
5. receipt.json、journal.json、public-input.json を bundle.zip にアーカイブ
6. *-receipt.json / *-output.json / public-input.json / bundle.zip などを S3 にアップロード

コールバック Lambda は S3 のバンドルからジャーナルとレシートを取得し、presigned URL を生成してセッションデータに保存します。 非同期モードでは、journal.json は *-output.json から変換され、receipt.json は *-receipt.json をコピーしたものを bundle.zip に格納します。

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

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

{VERIFIER_WORK_DIR}/
  {sessionId}/
    {executionId}/
      input.json               ← 非公開: ウィットネス
      public-input.json        ← 公開
      journal.json             ← 公開
      receipt.json             ← 公開
      metadata.json            ← 公開
      verification.json        ← 非公開: 検証レポート
      bundle.zip               ← 公開: 許可リストファイルのアーカイブ

非同期モード（S3）

s3://{BUCKET}/sessions/{sessionId}/{executionId}/
  input.json                 ← 非公開: ワーク入力
  {inputBase}-receipt.json   ← ホストの生出力
  {inputBase}-output.json    ← ホストの生出力
  {inputBase}-journal.json   ← ホストが生成した場合のみ
  public-input.json          ← 公開
  bundle.zip                 ← 公開: 内部は receipt.json / journal.json / public-input.json
  verification.json          ← `/api/verification/run` 後に追加される場合がある

inputBase はコンテナ実行時に生成される一時入力ファイル名に依存するため、非同期モードの S3 オブジェクト名は固定の receipt.json / journal.json になりません。

バンドルのアクセス方法

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

S3 にアップロードされたバンドルは presigned URL 経由でアクセスされます。presigned URL は有効期限付きであり、期限切れの場合はクライアントが /api/verify?refreshS3=1 で新しい URL を取得できます。

アーカイブの再現性

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

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

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

セキュリティ上の制約

パストラバーサル防止

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

非公開ファイルの保護

input.json と verification.json は、bundle.zip には含まれません。これらのファイルがバンドルディレクトリに存在していても、許可リストに含まれていないため、アーカイブ作成時に除外されます。

ゲーティングロジック

「Verified」表示の条件と、表示を阻止する不変条件を解説します。

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

最終判定の種類

検証パイプラインの結果は、verificationChecks の集約結果として以下に分類されます。

ステータスの判定順序

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

validateVotingIntegrity はクライアント側の補助判定として実装されています。この関数は 5 つのゲートを順に評価し、いずれかが失敗した時点で canShowVerified = false を返します。

ただし通常の /verify 取得では journal が省略されるため（includeJournal=1 未指定）、この補助判定は標準フローで常時実行されるわけではありません。最終サマリ表示は verificationChecks の集約（deriveVerificationSummary）が優先されます。

ゲート 1: 整合性証明

RFC 6962 の整合性証明により、掲示板が追記専用であることを検証します。

ゲート 2: 完全性（Completeness）

zkVM の集計に全投票が含まれたことを検証します。

excludedCount > 0 は、投票が意図的に集計から除外されたことを意味します。これは投票システムにおいて最も深刻な不正であり、いかなる場合も「Verified」を表示してはなりません。

ゲート 3: 警告の収集

validateVotingIntegrity では totalExpected != treeSize や invalidIndices > 0 を警告として収集します（excludedCount == 0 の場合）。

ただし、verificationChecks 側では counted_expected_vs_tree_size が必須チェックであり、totalExpected != treeSize は failed として最終的に Verified をブロックします。

ゲート 4: 第三者 STH 検証（有効時のみ）

STH ソースが設定されている場合のみ評価されます。

STH 合意の検証では、STH ダイジェストは必須照合です。bulletinRoot と treeSize は各ソースが値を返した場合にのみ照合対象になります。

• STH ダイジェスト（logId || treeSize || timestamp || bulletinRoot の SHA-256）
• 掲示板ルート（返却時）
• ツリーサイズ（返却時）

ゲート 5: ユーザーインデックスの範囲検証

投票者のインデックスがツリーサイズの範囲内であることを確認します。

STARK 検証のゲーティング

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

現在の実装では、STARK not_run の状態で「Verified（整合性）」を緑表示する経路はありません。

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

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

dev_mode は事前に success または not_run に正規化されてから zkGate に入力されます。

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

UI に表示される 4 つのステップは、20 個のチェックのサブセットから派生します。

ステップのステータスは、対応するチェックのステータスから集約されます。

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

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

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

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

  Note over U: STARK 完了まで待機

  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: 最終判定を表示

重要な制約として、STARK 検証が完了するまで、ステップの表示シーケンスは開始されません。これは、STARK の結果が Counted チェックの評価（zkGate）に影響するためです。

不変条件のまとめ

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

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

改ざんシナリオ

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

本章の前提（実 API 基準）

本章は、src/server/api / src/lib/finalize / src/lib/verification の実 API 実装を基準に説明します。

• NEXT_PUBLIC_USE_MOCK_API=true で mock API を使う場合は fixture ベースの応答になるため、チェック結果やステップ表示が本章と異なることがあります
• 特にローカル開発既定値（.env.local.example）では mock API が有効化されるため、実 API での再現時は mock API を無効化して確認します

教育モードの目的

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

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

攻撃の 2 類型

flowchart TD
  A["攻撃類型"]
  I["入力改ざん (tamperMode=input)<br/>S1 / S3 / S5"]
  C["主張改ざん (tamperMode=claim)<br/>S2 / S4"]

  A --> I
  A --> C

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

• 入力改ざん（S1/S3/S5）: 典型的には counted_missing_indices_zero（excludedCount > 0）で検出。S5 の再集計分岐では counted_tally_consistent が併発する場合があります
• 主張改ざん（S2/S4）: 典型的には counted_tally_consistent（claimed と verified の不一致）で検出

実装上、/api/verify の counted_* は STARK 状態でゲートされるため、verificationStatus=not_run では not_run、verificationStatus=running では pending が返り得ます。

シナリオ適用単位

現行実装では 1 回の finalize で選べるシナリオは 1 つです。

• UI: /aggregate は single-select（S0〜S5 のラジオボタン）
• API: POST /api/finalize は scenarioId を 1 つ受け取る
• finalize 実行モードは FINALIZE_ASYNC_MODE で切り替わる（false: 同期, true: 非同期）
• .env.local.example の既定値は FINALIZE_ASYNC_MODE=false（同期）
• AWS 運用では通常 FINALIZE_ASYNC_MODE=true（非同期）を使う

この部に含まれる章

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

シナリオ一覧

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

実装上の共通前提

• 1 回の finalize で選択されるシナリオは 1 つ（S0〜S5）
• 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: 非同期）
• .env.local.example の既定値は FINALIZE_ASYNC_MODE=false（同期）
• AWS 運用では通常 FINALIZE_ASYNC_MODE=true（非同期）を使う
• NEXT_PUBLIC_USE_MOCK_API=true の mock API fixture は本章と異なるチェック結果を返すことがある
• /api/verify の counted_* チェックは STARK 状態でゲートされる（verificationStatus=not_run では not_run、running では pending）
• 本章の「主な失敗点」は、STARK 検証が解決済み（success/failed）で counted_* が評価可能な局面を前提とする

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 に渡します。

ポイント:

• 掲示板上のユーザー票エントリは残る
• 検出は主に完全性チェック（excludedCount > 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 が使われる
• 除外パスでは missingIndices が増え、再集計パスでは不正票化により invalidIndices が増えるため、いずれも excludedCount > 0 になる
• 再集計パスでは counted_tally_consistent も失敗し得る（claimed は再集計後、verified は不正票除外後）

再集計パスでも excludedCount が 0 にならないのは、zkVM 側で不正票として除外されるためです。

シナリオ一覧表

ジャーナル統計オーバーライド（同期 finalize のみ）

同期 finalize（ローカル実行）では、tamperMode=input の場合（S1/S3/S5）に zkVM 実行後の統計を次で上書きします。

• missingIndices = max(existingMissing, ignoredCount)
• invalidIndices = max(existingInvalid, recountedCount)
• excludedCount = missingIndices + invalidIndices
• countedIndices = totalExpected - excludedCount

一方、FINALIZE_ASYNC_MODE=true の非同期 finalize ではこのオーバーライドは適用せず、コールバックで復元した zkVM ジャーナル値をそのまま用います。

tamperMode=claim（S2/S4）ではこのオーバーライドは行いません。

集計フローへの挿入点

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

検出メカニズム

各改ざんシナリオに対して、検証パイプラインがどのチェックで失敗するかを整理します。ここでは実装上の実際の判定ロジック（verification-checks と verification-summary）に合わせて説明します。

本章は実 API（src/server/api/handlers/verify.ts と src/lib/verification/*）の判定ロジックを基準にしています。NEXT_PUBLIC_USE_MOCK_API=true の mock API fixture では、本章と異なるチェック結果を返すことがあります。

/api/verify の counted_* チェックは STARK 状態でゲートされます。

• verificationStatus=not_run の間、counted_* は not_run になり得る
• verificationStatus=running の間、counted_* は pending になり得る
• 本章で「失敗するチェック」と書く箇所は、STARK 検証が解決済み（success/failed）で counted_* が評価可能な局面を前提とする

検出の 2 つの原理

flowchart TB
  P1[原理1: 完全性違反\nexcludedCount > 0] --> C1[counted_missing_indices_zero が失敗]
  P2[原理2: 主張集計の不整合\nclaimed ≠ verified] --> C2[counted_tally_consistent が失敗]

• 原理1（完全性違反）: 主に S1/S3/S5
• 原理2（主張集計の不整合）: 主に S2/S4

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

補足:

• S1 では、ビットマップ証明が利用可能な場合 counted_my_vote_included も失敗し得ます
• S2/S4 では、cast_commitment_match と counted_input_commitment_match は通常成功します（zkVM 入力を改変していないため）
• STARK 未解決（not_run/running）の間は、上表の counted_* 失敗は not_run/pending として観測され得ます

4 段階検証モデルとの対応

この表は「シナリオ適用による典型挙動」を示します。not_run（証拠不足）や running（検証実行中）は運用状態により別途発生します。

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

S5 の counted_my_vote_included は、ランダム対象がユーザー票（除外または再集計）なら失敗し得ます。証拠不足時は not_run になります。

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"]

このため以下は通常発生しません。

• cast_commitment_match の失敗（ローカル証拠は改変されない）
• counted_input_commitment_match の失敗（zkVM 入力は元票）

S5 の実装依存ポイント

S5 はランダムに除外または再集計を選びますが、実装上は常に tamperMode=input です。FINALIZE_ASYNC_MODE=true の非同期 finalize では、実行後オーバーライドは行わず zkVM ジャーナル値をそのまま使います。

• 除外分岐: missingIndices=1 系になり、counted_missing_indices_zero が失敗
• 再集計分岐: invalidIndices=1 系になり、counted_missing_indices_zero が失敗
• 再集計分岐では counted_tally_consistent も併発して失敗し得る

ビットマップ証明の役割

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

• S1（ユーザー票除外）では、証明が利用可能なら失敗して「自分の票が未集計」であることを直接示せる
• 証拠不足で not_run になる場合でも、最終判定は Verified にならない（missing_evidence もしくは excludedCount による失敗）

最終判定（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: 完全性違反（S1/S3/S5）
• published_tally_mismatch: claimed と verified の不一致（S2/S4）
• counted_integrity_failed: Counted 系必須チェック失敗の一般ケース

AWS アーキテクチャ

STARK Ballot Simulator の AWS インフラストラクチャ設計を解説します。

本システムは Amplify Gen 2（Web ホスティング + AppSync + DynamoDB + Lambda）と Terraform 管理のプローバーインフラ（SQS + Step Functions + ECS Fargate + S3）を組み合わせたハイブリッド構成を採用しています。Amplify がアプリケーション層を、Terraform が計算集約的な証明生成パイプラインをそれぞれ管理します。

設計思想

なぜハイブリッド構成か

STARK 証明の生成には 16 vCPU / 32 GB メモリで約 6 分を要します。この特性は、API Gateway + Lambda の 15 分タイムアウト制約と相性が悪く、また通常の Web リクエストの処理パターンとも大きく異なります。

そこで本システムでは、責務に応じてインフラ管理を分離しています。

環境分離

develop と main の 2 環境を運用し、Terraform ワークスペースと Amplify ブランチデプロイによって完全に分離しています。

注: RISC0_DEV_MODE=1 / USE_MOCK_ZKVM=true は主にローカル同期実行向けの設定です。Terraform 管理の非同期プローバーパス（SQS → Step Functions → ECS）では、実 STARK 証明を前提にしています。

全体構成図

図: STARK Ballot Simulator の AWS 全体構成。Amplify 管理領域（上）と Terraform 管理領域（下）のハイブリッド構成。

サービス一覧

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

Amplify 管理

Terraform 管理

Amplify と Terraform の境界

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

flowchart TB
  subgraph TF["Terraform 管理"]
    OUT["出力値<br/>SFN ARN / SQS URL / S3 バケット名"]
    IN["入力変数<br/>finalize_callback_lambda_arn"]
  end

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

  OUT --> ENV
  CB --> IN

Terraform の出力値（Step Functions ARN、SQS URL、S3 バケット名など）は、Amplify の環境変数として設定され、Lambda 関数から参照されます。 実行時フロー（SQS → Step Functions → ECS など）の詳細は トポロジー と 非同期プローバー を参照してください。

この部に含まれる章

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

トポロジー

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 検証、レート制限を処理します。

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
    SESS["セッション検証"]
    TURN["Turnstile 検証"]
    RATE["レート制限"]
    HAND["ハンドラー実行"]
    SESS --> TURN --> RATE --> HAND
  end

CORS 設定では X-Session-ID ヘッダーを許可し、セッションスコープのリクエスト制御を実現しています。

Data レイヤ

AppSync（GraphQL API）と DynamoDB が、セッション・投票・集計結果のデータ永続化を担当します。認証は Cognito Identity Pool によるゲスト認証（IAM SigV4）で行われます。

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

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

Prover レイヤ

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

flowchart LR
  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 --> CB["finalize-callback-runner<br/>Lambda"]
  ECS --> S3["S3<br/>証明バンドル"]

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

Storage レイヤ

S3 バケットが証明バンドル（レシート、ジャーナル、公開入力）の保存を担当します。

オブジェクトのパスは sessions/{sessionId}/{executionId}/ 配下に構造化されています。

receipt.json と journal.json は S3 直下には保存されず、bundle.zip の内部エントリとして配布されます。

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

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

sequenceDiagram
  participant C as クライアント
  participant W as Web レイヤ<br/>(Amplify Hosting)
  participant A as API レイヤ<br/>(API GW + Lambda)
  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->>P: イメージ署名検証
    P->>P: ECS タスクで証明生成
    P->>S: input.json + 実行成果物 + 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->>S: バンドル取得
  A->>A: STARK レシート検証
  A-->>C: 検証結果返却

ネットワーク構成

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 ログ群

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| SIGFAIL["署名検証失敗"]
  ECS --> S3W["S3<br/>bundle.zip 保存"]
  ECS --> CB["finalize-callback-runner<br/>Lambda"]
  SIGFAIL --> 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 を返却（FINALIZE_ASYNC_MODE=false の場合は同期処理のレスポンスを返却）

クライアントはその後、GET /api/sessions/:id/status をポーリングして進捗を確認します。

ステージ 2: ディスパッチ

prover-dispatch-proxy Lambda が SQS メッセージを受信し、以下を実行します。

1. zkVM 入力 JSON を S3 にアップロード（sessions/{sessionId}/{executionId}/input.json）
2. Step Functions のステートマシンを StartExecution で起動
3. セッションの finalizationState を「running」に更新し、executionId を記録

ステージ 3: 証明生成

Step Functions ステートマシンが 3 つのステップを順次実行します。

stateDiagram-v2
  [*] --> VerifyImageSignature
  VerifyImageSignature --> CheckImageSignature
  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 を呼び出し、以下の情報をセッションに書き戻します。

• 成功時: S3 上のバンドルメタデータ（バケット、キー）、証明結果
• 失敗時: エラー情報（イメージ署名失敗、プローバーエラーなど）

ECS タスクの実行フロー

ECS Fargate タスク内のコンテナは、エントリポイントスクリプトにより以下の処理を順次実行します。

flowchart TD
  A["S3 から入力 JSON を<br/>ダウンロード"] --> B["入力の構造を検証<br/>(必須フィールド確認)"]
  B --> C["zkVM ホストバイナリを実行<br/>(タイムアウト: 900 秒)"]
  C --> D["ジャーナルを JSON に変換"]
  D --> E["public-input.json を構築"]
  E --> F["bundle.zip を作成<br/>(receipt + journal + public-input)"]
  F --> G["S3 にアップロード<br/>(リトライ付き)"]

入力の検証

エントリポイントは、zkVM 入力 JSON に必要なフィールドが存在することを確認します。欠落があればタスクは即座に失敗し、Step Functions が失敗コールバックを実行します。

zkVM ホストバイナリの実行

コンテナ内の /opt/zkvm/bin/host がプローバーとして起動されます。タイムアウトは 900 秒（15 分）です。本番モード（RISC0_DEV_MODE 未設定）では実際の STARK 証明が生成され、64 票で約 370 秒を要します。

S3 アップロード

生成されたアーティファクトは、指数バックオフ付きのリトライ（最大 3 回、基底 2 秒）で S3 にアップロードされます。実際にアップロードされるファイルは以下です。

journal.json は *-output.json からエントリポイント内で再構成され、bundle.zip の中に receipt.json とともに格納されます。

SQS キュー設計

ワークキュー

デッドレターキュー（DLQ）

3 回の受信失敗後、メッセージは DLQ に移動されます。DLQ のメッセージ保持期間は 14 日で、手動での障害調査と再処理に使用されます。

ECS Fargate タスク仕様

ARM64 アーキテクチャの選択は、RISC Zero の STARK 証明生成における Graviton プロセッサのコスト効率に基づいています。

クライアント側のポーリング

非同期証明の進捗は、クライアントが GET /api/sessions/:id/status をポーリングして確認します。

stateDiagram-v2
  [*] --> pending: POST /api/finalize → 202
  pending --> running: dispatch-proxy が SFN を起動
  running --> succeeded: callback-runner が結果を書き込み
  running --> failed: エラー発生
  succeeded --> [*]
  failed --> [*]

障害時の調査導線

非同期証明がスタックした場合の最小調査パスです。

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 書き込み権限"]

イメージ署名

AWS Signer によるプローバーコンテナイメージの署名と実行前検証を解説します。

STARK 証明は「特定のゲストプログラムが正しく実行された」ことを保証しますが、そもそもそのゲストプログラムを含むコンテナイメージ自体が改ざんされていないことも保証する必要があります。イメージ署名は、信頼されたビルドパイプラインが生成したイメージのみが証明生成に使用されることを担保するセキュリティゲートです。

脅威モデル

イメージ署名が防止する攻撃シナリオを示します。

flowchart TD
  subgraph "署名なしの場合"
    A1["攻撃者が ECR イメージを<br/>改ざんしたものに置換"] --> B1["改ざんされたプローバーが<br/>不正な集計結果を生成"]
    B1 --> C1["不正な結果に対して<br/>有効な STARK 証明が存在"]
  end

  subgraph "署名ありの場合"
    A2["攻撃者が ECR イメージを<br/>改ざんしたものに置換"] --> B2["Step Functions が<br/>署名検証を実行"]
    B2 --> C2["署名不一致を検出<br/>タスク起動を拒否"]
  end

STARK 証明は Image ID（ゲストバイナリの暗号的識別子）に紐づきますが、イメージ署名はそれとは別のレイヤで「コンテナイメージ全体の完全性」を保証します。両者は相補的な防御を形成します。

署名フロー

ビルドと署名

CodeBuild がプローバーコンテナイメージをビルドして ECR に push し、Step Functions 実行時に署名ステータスを検証します。 ECR マネージド署名が有効な環境では、push 後に AWS Signer プロファイルに基づく署名ステータスが付与されます。

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->>ECR: イメージをプッシュ<br/>(ダイジェスト付き)
  ECR->>SGN: （ECR managed signing 有効時）署名処理
  SGN->>ECR: 署名ステータス更新
  Note over ECR: イメージ + 署名が<br/>一体で保存される

注: このリポジトリでコード化されているのは署名ステータス検証（DescribeImageSigningStatus）です。
署名付与そのもの（ECR managed signing の有効化）は、ECR 側の設定・運用が前提です。

ECR のイメージ URI は常にダイジェスト固定（@sha256:<64-hex>）で参照されます。タグベースの参照は使用しません。これにより、タグの上書きによるイメージのすり替えを防止します。

実行前検証

Step Functions ステートマシンの最初のステートで、check-image-signature Lambda がイメージの署名ステータスを検証します。

stateDiagram-v2
  [*] --> VerifyImageSignature: Step Functions 開始
  VerifyImageSignature --> CheckSignatureResult

  state CheckSignatureResult <<choice>>
  CheckSignatureResult --> RunProver: status = COMPLETE
  CheckSignatureResult --> SignatureFailed: status ≠ COMPLETE

  state SignatureFailed {
    [*] --> 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 リポジトリとイメージ管理

リポジトリ構成

両リポジトリとも、プッシュ時の脆弱性スキャン（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 ロールには以下の権限が付与されています。

DS-202 準拠

本システムのイメージ署名アーキテクチャは、デジタル署名に関する DS-202 ガイドラインの以下の原則に準拠しています。

Image ID との関係

イメージ署名と Image ID は異なるレイヤのセキュリティメカニズムですが、共に「正しいプログラムが実行されたこと」の信頼チェーンを構成します。

flowchart TD
  subgraph "ビルド時"
    BUILD["コンテナイメージ<br/>ビルド"] --> SIGN["AWS Signer で<br/>イメージ署名"]
    BUILD --> IMGID["Image ID 計算<br/>(ゲストバイナリから導出)"]
    IMGID --> MAP["imageId-mapping.json<br/>に記録"]
  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

Terraform

IaC（Infrastructure as Code）による AWS リソース管理の設計を解説します。

Terraform は、証明生成パイプラインに関わる AWS リソース（ECS、Step Functions、SQS、S3、ECR、CodeBuild、VPC、Lambda）を宣言的に管理します。Amplify Gen 2 が管理するリソース（Web ホスティング、AppSync、hono-api Lambda 等）とは明確に分離されています。

ディレクトリ構成

Terraform の構成ファイルは terraform/ ディレクトリに配置され、機能別に分割されています。

環境分離

ワークスペース戦略

develop と main の 2 環境を、Terraform ワークスペースと tfvars ファイルの組み合わせで管理します。

flowchart LR
  subgraph "Terraform State"
    S3["S3 バケット<br/>terraform-state"]
    S3 --> DEV["develop<br/>workspace"]
    S3 --> MAIN["main<br/>workspace"]
  end

  subgraph "tfvars"
    DEVF["develop.tfvars"]
    MAINF["main.tfvars"]
  end

  DEVF --> DEV
  MAINF --> MAIN

environment 変数はバリデーションにより develop または main のみが許可されます。環境ごとの差分は locals で定義された設定マップにより解決されます。

ワークスペースの確認

環境の取り違えを防ぐため、操作前にワークスペースの確認が推奨されます。

ステート管理

S3 バックエンド

Terraform ステートは S3 バケットに保存され、DynamoDB テーブルによるロック機構でステートの同時変更を防止します。

認証方式

Terraform の実行は STS AssumeRole を前提としています。
具体的な認証ツール（AWS IAM Identity Center / aws-vault など）は運用環境に依存し、Terraform コードの責務外です。

flowchart LR
  EXEC["実行環境<br/>(ローカル/CI)"] --> STS["AWS STS<br/>AssumeRole"]
  STS --> ROLE["Terraform 実行ロール<br/>IAM ロール"]
  ROLE --> TF["Terraform 実行"]

主要な入力変数

Terraform の実行に必要な変数と、そのバリデーションルールの概要です。

必須変数

注: 現行の CodeBuild source は GITHUB タイプ（location 指定）で構成されています。

オプション変数

出力値

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"]
    CIS["check_image_signature"]
  end

  ECSSVC --> ETE
  ECSSVC --> ET
  STATESVC --> SFN
  CBSVC --> CB
  LAMSVC --> CIS

スコープの制限

• ECS タスクロールの S3 権限は sessions/* プレフィックスに制限
• Step Functions ロールの ECS 権限は特定クラスター ARN に制限
• Step Functions ロールの iam:PassRole は ECS 関連ロールのみに制限

Amplify との連携ポイント

Terraform と Amplify は相互に独立して管理されますが、以下のポイントで連携します。

flowchart TB
  subgraph TF["Terraform"]
    SFN_ARN["Step Functions 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_URL --> ENV
  S3_NAME --> ENV
  CB_ARN -. "IaC input" .-> CB_INPUT

この双方向の参照により、Amplify が管理する Lambda を Terraform が管理する Step Functions から呼び出すことが可能になります。

バージョン制約

API リファレンス

この章では、公開ドキュメントとして扱うべき API（ブラウザクライアントと第三者検証で利用するエンドポイント）を、現行実装ベースで説明します。

この章の対象範囲

対象:

• 投票・集計フロー（/api/session, /api/vote, /api/progress, /api/finalize, /api/finalize/cancel, /api/sessions/:sessionId/status）
• 検証フロー（/api/verify, /api/verification/run, バンドル取得）
• 監査補助（/api/bulletin/*, /api/bitmap-proof, /api/sth, /api/zkvm-input-hash, /api/botdata/:id）

対象外（内部運用 / デバッグ向け）:

• GET /api/debug/enable
• POST /api/finalize/callback

デュアルランタイム構成

API ハンドラはフレームワーク非依存の共通実装で、Next.js と Hono(Lambda) の両方から利用されます。

リクエスト処理の実装上の注意

ミドルウェアは「全リクエスト共通の固定チェーン」ではなく、エンドポイント実装ごとに必要な検証を呼び出す方式です。

補足:

• GET /api/bitmap-proof の X-Session-ID はストア実装依存です（Mock/File は省略可、Amplify は実質必須）。

エラーレスポンスの実装差分

多くのエンドポイントは errorResponse(...) を通して以下の形式を返します。

• error（エラーコード）
• message（メッセージ）
• statusCode（HTTP ステータス）
• 必要に応じて details など

ただし、いくつかのエンドポイント（例: GET /api/sessions/:sessionId/status, GET /api/verification/bundles/...）は、{ error: "..." } のような独自形式を返します。詳細は エンドポイント一覧 を参照してください。

この部に含まれる章

• エンドポイント一覧 — 公開対象 API のリクエスト/レスポンス仕様
• セッションライフサイクル — クライアントとサーバーのセッション管理実装

エンドポイント一覧

この文書は、公開ドキュメントとして扱う API を対象に、現行実装のレスポンス形状・要件を記載します。

対象外（内部向け）

以下は内部運用/デバッグ用途のため、この文書の詳細対象外です。

• GET /api/debug/enable
• POST /api/finalize/callback

公開対象 API 一覧

共通の実装上の注意

• POST /api/vote と POST /api/finalize は Turnstile 検証を実行します。
• POST /api/verification/run は Turnstile なしで、/api/finalize と同じ zkVM レート制限を使用します。
• エラー形式はエンドポイントにより異なります（標準化 payload と独自 payload が混在）。

基本フロー API

POST /api/session

新規セッションを作成します。

レスポンス（200）:

• data.sessionId
• data.electionId
• data.electionConfigHash
• data.logId

備考:

• このハンドラでは X-Session-ID は不要です。

POST /api/vote

ユーザー投票を保存し、ボット投票を非同期開始します。

要件:

• ヘッダー: X-Session-ID 必須
• ボディ: commitment, vote, rand（turnstileToken は開発設定により省略可）
• Turnstile 検証あり
• 投票用レート制限あり

レスポンス（200）:

• data.voteId
• data.commitment
• data.bulletinIndex
• data.bulletinRootAtCast
• data.timestamp

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)
• CAPTCHA_FAILED (403)
• GLOBAL_LIMIT_EXCEEDED (503)
• ALREADY_VOTED (400)
• SESSION_FINALIZED (400)
• INVALID_VOTE_CHOICE (400)
• INVALID_COMMITMENT (400)
• DUPLICATE_VOTE (409)

GET /api/progress

投票進捗を取得します。

要件:

• ヘッダー: X-Session-ID 必須

レスポンス（200）:

• data.count
• data.total
• data.completed
• data.userVoted
• data.finalized

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)

POST /api/finalize

集計と証明生成を開始します。同期/非同期の 2 形態があります。

要件:

• ヘッダー: X-Session-ID 必須
• ボディ: scenarioId（S0-S5）, turnstileToken（環境により必須）
• Turnstile 検証あり
• zkVM レート制限あり

レスポンス（200, 同期）:

• data.sessionId
• data.tally
• data.bulletinRoot
• data.verifiedTally
• data.voteReceipt
• data.receipt（同期成功レスポンスで返却）
• data.receiptPublication（保存時）
• data.imageId
• data.userVote
• data.missingIndices
• data.invalidIndices
• data.countedIndices
• data.totalExpected
• data.treeSize
• data.sthDigest
• data.includedBitmapRoot
• data.inputCommitment
• data.verificationStatus
• data.verificationBundleUrl / data.verificationReportUrl / data.verificationReport（条件付き）
• data.verificationExecutionId（条件付き）
• data.s3BundleUrl / data.s3BundleKey / data.s3UploadedAt / data.s3BundleExpiresAt（条件付き）
• data.tamperSummary（条件付き）

レスポンス（202, 非同期）:

• executionId
• statusUrl
• state
• queue（null の場合あり）

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)
• CAPTCHA_FAILED (403)
• INVALID_REQUEST (400)
• VERIFICATION_FAILED (400, CT proof unavailable)
• USER_NOT_VOTED (400)
• VOTING_NOT_COMPLETE (400)
• SESSION_ALREADY_FINALIZED (400)
• ZKVM_RATE_LIMIT_EXCEEDED (429)
• GLOBAL_LIMIT_EXCEEDED (503)
• Invalid ImageID (400, 独自形式 { error: "Invalid ImageID", details: { expected, actual } })

POST /api/finalize/cancel

進行中の非同期集計をキャンセルします。

要件:

• FINALIZE_ASYNC_MODE=true のときのみ有効
• ヘッダー: X-Session-ID（x-session-id も受理）
• ボディ: executionId 必須、reason 任意

レスポンス（200）:

• state

主なエラー（このエンドポイントは独自形式）:

• 404: Async finalization disabled / Session not found
• 400: ヘッダー欠落、JSON 不正、payload 不正
• 409: 現在状態ではキャンセル不可
• 500: Session store unavailable
• 501: ストアが cancellation 非対応

GET /api/sessions/:sessionId/status

非同期集計の状態を返します。

要件:

• パスパラメータ sessionId 必須

レスポンス（200）:

• sessionId
• finalizationState（null の場合あり）
• queue（null の場合あり）
• progress（条件付き）
• finalizationResult（null の場合あり）
• stepFunctions（条件付き）
• asyncFinalizationMode（enabled / disabled）

主なエラー（独自形式）:

• 400: Session ID is required
• 404: Session not found

検証 API

GET /api/verify

検証画面向けの統合ペイロードを返します。

要件:

• ヘッダー: X-Session-ID 必須
• クエリ: refreshS3=1, includeJournal=1（任意）

レスポンス（200）:

• data.electionId
• data.electionConfigHash
• data.logId
• data.tally
• data.bulletinRoot
• data.scenarioId
• data.verificationStatus
• data.verificationBundleUrl / data.verificationReportUrl / data.verificationReport（条件付き）
• data.verificationSteps / data.verificationChecks
• data.s3BundleUrl / data.s3BundleKey / data.s3UploadedAt / data.s3BundleExpiresAt（条件付き）
• data.imageId
• data.tamperDetected
• data.verifiedTally
• data.missingIndices
• data.invalidIndices
• data.countedIndices
• data.totalExpected
• data.treeSize
• data.excludedCount
• data.sthDigest
• data.includedBitmapRoot
• data.inputCommitment
• data.seenIndicesCount（条件付き）
• data.journalStatus
• data.journal（includeJournal=1 のとき）
• data.voteReceipt（条件付き）
• data.userVote（条件付き）
• data.botVotesSummary（条件付き）
• data.verificationExecutionId（条件付き）
• data.tamperSummary（条件付き）

特殊レスポンス:

• verificationStatus が許容セット外の場合、400 VERIFICATION_FAILED を返しつつ、data.verificationSteps / data.verificationChecks を返します。

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)
• SESSION_NOT_FINALIZED (400)
• USER_NOT_VOTED (400)

POST /api/verification/run

サーバー側で STARK レシート検証を実行します。

要件:

• ヘッダー: X-Session-ID 必須
• ボディ: JSON オブジェクト（通常は空オブジェクト {}）
• zkVM レート制限あり

レスポンス（200）:

• data.verificationStatus（success / failed / dev_mode / not_run / running）
• data.verificationExecutionId
• data.estimatedDurationMs
• data.idempotent

挙動:

• 既存結果がある場合や実行中の場合は、再実行せず idempotent: true を返します。

バンドル取得 API

GET /api/verification/bundles/:sessionId/:executionId

証明バンドル bundle.zip を返します。

レスポンス:

• 200: ZIP バイナリ
• 302: S3 presigned URL へリダイレクト
• 400: パラメータ不正
• 404: バンドル未検出
• 500: ダウンロード URL 生成失敗 / 読み込み失敗

GET /api/verification/bundles/:sessionId/:executionId/report

検証レポート verification.json を返します。

レスポンス:

• 200: JSON
• 302: S3 presigned URL へリダイレクト
• 400: パラメータ不正
• 404: レポート未検出
• 500: ダウンロード URL 生成失敗 / 読み込み失敗

掲示板 API

GET /api/bulletin

掲示板一覧を返します。

要件:

• ヘッダー: X-Session-ID 必須
• クエリ: offset, limit（任意）

レスポンス（200）:

• commitments
• bulletinRoot
• treeSize
• timestamp
• rootHistory（条件付き）
• nextOffset / hasMore（ページング時）

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)
• INVALID_OFFSET (400)
• INVALID_LIMIT (400)

GET /api/bulletin/:voteId

投票単位の包含証明を返します。

要件:

• ヘッダー: X-Session-ID 必須
• パス: voteId（UUID v4 形式）

レスポンス（200）:

• voteId
• commitment
• bulletinIndex
• merklePath
• bulletinRootAtCast
• treeSize
• proofMode（rfc6962）

主なエラー:

• INVALID_VOTE_ID (400)
• VOTE_NOT_FOUND (404)
• VERIFICATION_FAILED (400, CT proof unavailable)

GET /api/bulletin/:voteId/proof

最小形式の包含証明を返します。

要件:

• ヘッダー: X-Session-ID 必須
• セッションは finalized 必須
• パス: voteId

アクセス制御:

• 原則は「そのセッションのユーザー投票」のみ
• 例外としてシナリオ S3/S4 では対象ボット票を許可

レスポンス（200）:

• voteId
• proof.leafIndex
• proof.merklePath
• proof.treeSize
• proof.bulletinRootAtCast
• proof.proofMode

キャッシュ:

• ETag 対応
• If-None-Match 一致時は 304

GET /api/bulletin/consistency-proof

RFC6962 整合性証明を返します。

要件:

• ヘッダー: X-Session-ID 必須
• クエリ: oldSize, newSize 必須

レスポンス（200）:

• oldSize
• newSize
• rootAtOldSize
• rootAtNewSize
• proofNodes
• oldSubtreeHashes / appendSubtreeHashes（条件付き）
• timestamp

備考:

• このエンドポイントは独自のエラー JSON を返します。

GET /api/botdata/:id

ボット投票（1..63）のデータと証明を返します。

要件:

• ヘッダー: X-Session-ID 必須
• セッション finalized 必須

レスポンス（200）:

• data.id
• data.vote
• data.random
• data.commitment
• data.voteId
• data.timestamp
• data.proof（leafIndex, merklePath, treeSize, bulletinRootAtCast, proofMode）

主なエラー:

• INVALID_BOT_ID (400)
• SESSION_NOT_FINALIZED (400)
• BOT_DATA_NOT_FOUND (404)

補助 API

GET /api/bitmap-proof

ビットマップ包含証明の材料を返します。

要件:

• クエリ: i（0 以上整数）必須
• X-Session-ID はストア実装依存（Mock/File は省略可、Amplify は実質必須）
• 互換性のため X-Session-ID の指定を推奨

レスポンス（200）:

• leafChunk
• auditPath

キャッシュ:

• ETag 対応
• If-None-Match 一致時 304
• Cache-Control: private ... immutable

エラー（独自コード）:

• INVALID_INDEX (400)
• BITMAP_NOT_FOUND (404)
• INTERNAL_ERROR (500)

GET /api/sth

STH スナップショットを返します。

要件:

• ヘッダー: X-Session-ID 必須
• finalized セッションのみ

レスポンス（200）:

• sth.sthDigest
• sth.bulletinRoot
• sth.treeSize
• sth.timestamp
• sth.logId

備考:

• 現行実装の sth.timestamp はジャーナル内時刻ではなく、session.lastActivity を返します。

主なエラー:

• SESSION_ID_REQUIRED (400)
• SESSION_NOT_FOUND (404)
• SESSION_NOT_FINALIZED (404, このエンドポイント固有の扱い)

GET /api/zkvm-input-hash

セッション由来の zkVM 入力コミットメントを返します。

要件:

• クエリ: sessionId 必須
• クエリ: includeData 任意（true / 1 / yes で有効）

レスポンス（200）:

• inputCommitment
• data（includeData 有効時のみ）

主なエラー（独自形式）:

• INVALID_REQUEST (400)
• SESSION_NOT_FOUND (404)
• SESSION_NOT_FINALIZED (400)
• CT_PROOF_UNAVAILABLE (400)
• INTERNAL_ERROR (500)

セッションライフサイクル

この文書は、セッション管理の実装を クライアント側とサーバー側に分けて説明します。

1. 管理責務の分離

クライアントとサーバーは X-Session-ID で紐づきます（ただし全エンドポイントで必須ではありません）。

2. クライアント側フェーズ

クライアントセッション（src/lib/session/client.ts）のフェーズは以下の 3 つです。

• voting
• finalizing
• verifying

主な遷移トリガー:

• POST /api/session 後に generateSessionId(...) で voting 開始
• aggregate 画面で非同期集計の pending/running を検知すると saveSessionData({ phase: 'finalizing' })
• 集計結果を保存すると saveSessionData({ finalizeResult, phase: 'verifying' })

3. クライアント TTL 実装

SESSION_PHASE_TIMEOUTS_MS:

• voting: 30 分
• finalizing: 30 分
• verifying: 24 時間

TTL 更新の実装ポイント:

• generateSessionId(...): 新規作成
• saveSessionData(...): フェーズを加味して expiresAt を再計算
• updateLastActivity(...): 現在フェーズで expiresAt を再延長

期限切れ判定:

• checkTimeout() または getSessionData() が有効期限超過を検出すると clearSession() を実行

補足:

• 専用 heartbeat API はありません。
• 60 秒間隔の updateLastActivity() は現行実装では verify 画面で実行されています。

4. サーバー側セッション状態

サーバーは SessionData に以下を保持します。

• 投票（votes, userVoteIndex, botCount）
• 集計状態（finalizationState）
• 集計結果（finalizationResult）
• 最終活動時刻（lastActivity）

finalizationState.status は以下を取り得ます。

• pending
• running
• succeeded
• failed
• timeout

5. サーバー側 TTL / 失効の実装差分

サーバー側の失効挙動はストア実装で異なります。

重要事項:

• 「同時セッション上限 100」を強制するロジックは、現行の /api/session 実装には入っていません。

6. X-Session-ID スコープ

X-Session-ID の要否はエンドポイントごとに異なります。

ヘッダー必須の代表例:

• /api/vote, /api/progress, /api/finalize, /api/finalize/cancel
• /api/verify, /api/verification/run
• /api/bulletin, /api/bulletin/:voteId, /api/bulletin/:voteId/proof, /api/bulletin/consistency-proof
• /api/botdata/:id, /api/sth

ヘッダー不要の代表例:

• /api/sessions/:sessionId/status（パスパラメータ）
• /api/verification/bundles/:sessionId/:executionId（パスパラメータ）
• /api/zkvm-input-hash（クエリ sessionId）

実装依存:

• /api/bitmap-proof（Mock/File は省略可、Amplify は実質必須）

7. マルチタブ時の実務上の注意

localStorage は同一オリジンで共有されるため、タブ間でセッション情報が競合します。

代表的な結果:

• 片方のタブで投票済み後、別タブで再投票すると ALREADY_VOTED
• 片方のタブで集計完了後、別タブで再集計すると SESSION_ALREADY_FINALIZED
• セッション作成を並行すると、最後に保存した starkBallotSession が有効になる

第三者検証ガイド

この章は、アプリの検証ページでダウンロードした bundle.zip を使って、第三者がローカルで独立検証するための最小手順をまとめたものです。

この章で扱う範囲

• 検証ページから取得した bundle.zip のローカル検証
• Ubuntu 環境での Rust セットアップ
• verifier-service を使った STARK レシート検証
• journal.json の完全性チェック（excludedCount など）

この章で扱わない範囲

• アプリケーション本体のビルド・デプロイ
• AWS インフラや非同期 finalize の運用トラブル対応
• アプリを一から複製して再現実行するための手順

上記の調査が必要な場合は、次のページを参照してください。

• チェック一覧（チェック ID と判定ロジック）
• API エンドポイント一覧（手動検証に使う API 契約）
• 検出メカニズム（改ざんシナリオごとの失敗パターン）
• 非同期プローバー（非同期 finalize の処理と障害調査導線）

最低限確認する不変条件

手順

• ZIP ローカル検証（Ubuntu）

ZIP ローカル検証（Ubuntu）

この手順は、検証ページでダウンロードした bundle.zip を対象に、Ubuntu 上で第三者検証を行うためのガイドです。

0. 前提

• 検証ページから bundle.zip をダウンロード済みであること
• Ubuntu 22.04 / 24.04
• このリポジトリ（stark-ballot-simulator）のソースを取得済みであること
• （Step 7 を実行する場合）Node.js 22+ と pnpm が利用可能であること
• （Step 7 を実行する場合）$REPO_ROOT で pnpm i を実行済みであること

検証ページのダウンロードは、s3BundleUrl と verificationBundleUrl の候補から実行されます。S3 URL が期限切れの場合は refreshS3=1 で再取得されます。

以降の手順では、リポジトリルートを REPO_ROOT として扱います。実際のクローン先に合わせて先に設定してください。

export REPO_ROOT="$HOME/stark-ballot-simulator"
cd "$REPO_ROOT"

1. Ubuntu セットアップ（Rust）

sudo apt update
sudo apt install -y build-essential pkg-config libssl-dev unzip jq curl ca-certificates

curl https://sh.rustup.rs -sSf | sh -s -- -y
source "$HOME/.cargo/env"

RUST_CHANNEL="$(awk -F'\"' '/^channel *=/ {print $2}' "$REPO_ROOT/rust-toolchain.toml")"
rustup toolchain install "$RUST_CHANNEL"
rustup default "$RUST_CHANNEL"
echo "rust_channel=$RUST_CHANNEL"

rustc --version
cargo --version

2. verifier-service をビルド

cd "$REPO_ROOT/verifier-service"
cargo build --release

生成物:

• verifier-service/target/release/verifier-service

3. bundle.zip を展開

mkdir -p ~/stark-audit
cp ~/Downloads/stark-ballot-verification-*.zip ~/stark-audit/bundle.zip
cd ~/stark-audit

unzip -o bundle.zip -d bundle
ls -1 bundle

最低限、以下のファイルが必要です。

• bundle/receipt.json
• bundle/journal.json
• bundle/public-input.json

metadata.json は同期モードでのみ含まれる場合があります。

4. 期待 Image ID を決定

journal.json の methodVersion から public/imageId-mapping.json を参照します。

METHOD_VERSION="$(jq -r '.methodVersion' bundle/journal.json)"

EXPECTED_IMAGE_ID="$(jq -r --arg v "$METHOD_VERSION" '.mappings[$v].expectedImageID // empty' "$REPO_ROOT/public/imageId-mapping.json")"

echo "methodVersion=$METHOD_VERSION"
echo "expectedImageId=$EXPECTED_IMAGE_ID"

EXPECTED_IMAGE_ID が空の場合は、マッピングの対象外です。検証を中断してください。

5. STARK レシートを検証

"$REPO_ROOT/verifier-service/target/release/verifier-service" verify \
  --bundle ./bundle.zip \
  --image-id "$EXPECTED_IMAGE_ID" \
  --output ./verification.json

echo "exit_code=$?"
jq '{status, expected_image_id, receipt_image_id, dev_mode_receipt, errors}' ./verification.json

判定:

• exit_code=0 かつ status="success": 合格
• exit_code=2 または status="dev_mode": フェイクレシート（本番検証としては不合格）
• exit_code=3 または status="failed": 不合格

6. journal.json の完全性チェック

jq '{excludedCount, missingIndices, invalidIndices, totalVotes, validVotes, verifiedTally}' bundle/journal.json

jq -e '.excludedCount == 0 and .missingIndices == 0 and .invalidIndices == 0' bundle/journal.json >/dev/null \
  && echo 'integrity_counts=ok' \
  || echo 'integrity_counts=ng'

jq -e '(.verifiedTally | add) == .validVotes' bundle/journal.json >/dev/null \
  && echo 'tally_sum=ok' \
  || echo 'tally_sum=ng'

excludedCount > 0 または missingIndices > 0 または invalidIndices > 0 は、検証失敗として扱います。

7. （任意）inputCommitment 再計算

public-input.json から再計算した値が journal.json の inputCommitment と一致することを確認します。 このステップには Node.js / pnpm と、$REPO_ROOT での pnpm i が必要です。

RECALC="$(cd "$REPO_ROOT" && pnpm tsx -e "import fs from 'node:fs'; import { computeInputCommitmentFromPublicInput } from './src/lib/zkvm/types'; const p = JSON.parse(fs.readFileSync(process.argv[1], 'utf-8')); console.log(computeInputCommitmentFromPublicInput(p));" "$PWD/bundle/public-input.json")"
JOURNAL_COMMITMENT="$(jq -r '.inputCommitment' bundle/journal.json)"

echo "recalculated=$RECALC"
echo "journal=$JOURNAL_COMMITMENT"

[ "${RECALC,,}" = "${JOURNAL_COMMITMENT,,}" ] && echo 'input_commitment=ok' || echo 'input_commitment=ng'

合格条件（最小セット）

• verifier-service の結果が success
• excludedCount == 0 かつ missingIndices == 0 かつ invalidIndices == 0

この2点を満たさない場合、Verified と判定しません。

設計判断

STARK Ballot Simulator の主要な技術選定と、PoC で意図的に受け入れた制約を解説します。

「なぜこの構成を採用したか」「何を PoC 都合で割り切ったか」を明文化し、実装・運用・監査の前提を共有します。

判断の記録方針

各判断は以下の 3 軸で記述します。

この部に含まれる章

• 技術選定 — 主要コンポーネントの選定理由
• PoC の意図的な制約 — 公開版で明示する 3 つの制約

関連する章

• 暗号プロトコル — 各プリミティブの仕様と安全性
• AWS アーキテクチャ — インフラ構成の詳細
• 検証パイプライン — 検証ロジックとゲーティング
• 参考文献 — 設計背景の一次資料一覧

技術選定

主要コンポーネントの技術選定理由を、背景・採用理由・トレードオフに絞って要約します。

1. STARK 証明: RISC Zero zkVM

背景

集計処理の正しさを暗号学的に示すため、ゼロ知識証明システムが必要でした。PoC では Trusted setup 不要の透明性を重視しています。

採用理由

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

トレードオフ

• 64 票で約 370 秒の証明生成時間が必要。
• 証明サイズは小さくないため、クライアント配布よりサーバー検証向き。

詳細: zkVM 設計、Image ID

2. 追記専用掲示板: RFC 6962 CT Merkle

背景

Recorded-as-Cast には、包含証明だけでなく「後から削除・改変されていない」ことの証明が必要です。

採用理由

• RFC 6962 の整合性証明で追記専用性を示せる。
• 包含証明と整合性証明の両方を同一モデルで扱える。
• STH ダイジェストと組み合わせてスプリットビュー攻撃の検出力を上げられる。

トレードオフ

• ドメイン分離（0x00/0x01）を含む実装厳密性が要求される。
• 自前実装ゆえに、検証テストを厚く維持する必要がある。

詳細: CT Merkle ツリー、STH ダイジェスト

3. デュアルランタイム: Next.js + Hono（共通ハンドラー）

背景

開発時は Next.js の統合体験、運用時は API Gateway + Lambda の軽量 API 実行が必要です。どちらか片方に寄せるより、同一ハンドラーを複数アダプタで使う構成を採用しています。

採用理由

• ハンドラー実装は 1 本化し、ランタイム差分はアダプタに限定。
• NEXT_PUBLIC_API_BASE_URL 未設定時は相対 /api を使い、同一フロント実装で両経路に対応。

トレードオフ

• Next/Hono の両アダプタを継続保守する必要がある。
• ランタイム差異の回帰をテストで継続検出する必要がある。

詳細: API リファレンス、トポロジー

4. インフラ分割: Amplify Gen2 + Terraform

背景

Web/API/Data と、重量級の証明パイプラインでは必要な運用粒度が異なります。

採用理由

• Amplify Gen2: フロント/ API / AppSync の開発速度を優先。
• Terraform: ECS / Step Functions / SQS / ECR など、証明基盤の低レイヤ制御を優先。
• 境界を分けることで、アプリ改修と証明基盤改修の干渉を下げる。

トレードオフ

• IaC が 2 系統になるため、運用知識の分散コストがある。
• デプロイ手順は単一ツールより長くなる。

詳細: AWS アーキテクチャ、Terraform

5. 証明実行環境: ECS Fargate（ARM64）

背景

STARK 証明生成は CPU/メモリ負荷が高く、通常の HTTP リクエスト処理と分離が必要です。PoC 設計時点では GPU 版 Lambda を前提にできず、SQS → Step Functions → ECS の非同期経路を標準としています。

採用理由

• 16 vCPU / 32 GB の実行要求を満たせる。
• Step Functions と組み合わせて、署名検証や失敗ハンドリングを実装しやすい。
• ARM64 でビルドと実行を揃え、コスト効率を優先。

トレードオフ

• タスク起動待ち（コールドスタート）がある。
• コンテナビルド/署名/配布の運用が前提になる。

詳細: 非同期プローバー、イメージ署名

6. ビルド戦略: Base Image と App Image の分離

背景

RISC Zero ツールチェーンを毎回アプリイメージに同梱ビルドすると、CI 時間とコストが大きくなります。

採用理由

• ベースを分離することで、日々のアプリビルドを短縮。
• ARM64 でビルドと実行を統一し、x86_64 エミュレーションを避ける。
• 実行基盤（Fargate ARM64）と同一アーキでの再現性を保ちやすい。

詳細: イメージ署名、非同期プローバー

PoC の意図的な制約

本章では、公開版 PoC で意図的に受け入れている制約を 3 点に絞って説明します。

「バグではなく設計上の割り切り」であることを明確化し、本番移行時にどこを解消すべきかを共有します。

制約の全体像

1. 固定票数 64（1 ユーザー + 63 ボット）

PoC の主目的は「検証可能投票の成立条件を end-to-end で示すこと」であり、まずは 64 票固定でパイプライン全体の再現性を優先しています。

2. ビットマップ隣接ビット漏洩

本来はチャンクを小さくし、木を深くすることで漏洩を抑制できます。PoC では zkVM 実行時間とのトレードオフを優先し、現在のチャンク設計を採用しています。

詳細: ビットマップ Merkle

3. 非 GPU 前提の証明実行（ECS Fargate）

この PoC では「GPU 実行を前提にした Lambda 経路を置かない」ことを先に固定し、運用容易性と再現性を優先しています。結果として、証明実行は SQS → Step Functions → ECS Fargate の非同期経路が中心になります。

詳細: AWS アーキテクチャ、非同期プローバー

PoC 制約下でも緩和しない不変条件

上記の制約を受け入れていても、以下は常に維持します。

詳細: ゲーティングロジック

用語集

本書で使用する主要な用語の定義です。暗号・検証の基礎用語と実装・運用の主要用語に分けて掲載しています。

暗号プリミティブ

コミットメント（Vote Commitment）

ドメイン分離タグ、選挙 ID、投票選択肢、乱数を結合して SHA-256 でハッシュした値。投票内容を秘匿しつつ（隠蔽性）、後から変更できないことを保証する（束縛性）。投票の Cast-as-Intended 検証の起点となる。

詳細: コミットメントスキーム

Merkle ルート（Bulletin Root）

掲示板上の全投票コミットメントから RFC 6962 の規則に従って計算されるハッシュ値。掲示板の特定時点における状態を一意に表現する。新しい投票が追加されるたびに更新される。

Merkle パス（Audit Path）

特定のリーフ（投票コミットメント）からルートまでを再構成するために必要な兄弟ノードのハッシュ列。包含証明の構成要素であり、対数オーダーの検証コストを実現する。

包含証明（Inclusion Proof）

特定の投票コミットメントが掲示板に含まれていることを暗号学的に証明するデータ。リーフインデックス、監査パス、ツリーサイズから構成される。RFC 6962 のハッシュ規則に従い、リーフとパスからルートを再計算して期待値と照合する。

詳細: CT Merkle ツリー

整合性証明（Consistency Proof）

RFC 6962 で定義された、2 つの時点のツリーが追記関係にあることを暗号学的に証明するデータ。古いツリーが新しいツリーのプレフィックスであること（投票の削除・並べ替えが行われていないこと）を保証する。

詳細: CT Merkle ツリー

入力コミットメント（Input Commitment）

zkVM に渡される入力全体（全投票のインデックス、コミットメント、Merkle パス）を正準エンコーディングで結合し SHA-256 でハッシュした値。zkVM が公開入力と同一のデータを処理したことを保証するバインディングとして機能する。

詳細: 入力コミットメント

STH ダイジェスト（Signed Tree Head Digest）

掲示板のログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュを結合して SHA-256 でハッシュした値。特定の時点における掲示板の状態を一意に識別し、複数の独立した監視者間で掲示板の一貫性を検証するために使用する。

詳細: STH ダイジェスト

包含ビットマップルート（Included Bitmap Root）

zkVM ゲストが生成するビットマップ（各投票インデックスが集計に含まれたか否か）の Merkle ルート。投票者は自分のインデックスに対応するビットが 1 であることを Merkle 証明で確認できる。

詳細: ビットマップ Merkle

ドメイン分離タグ（Domain Separation Tag）

ハッシュ計算において異なる用途のデータが衝突しないように付与するプレフィックス文字列。本システムでは、コミットメント、入力コミットメント、CT Merkle のリーフ・ノードハッシュにそれぞれ固有のタグを使用する。

STARK 証明

STARK（Scalable Transparent ARgument of Knowledge）

Trusted setup（信頼されたセットアップ）を必要としない暗号証明方式。ハッシュベースの構成により耐量子計算機性に優位がある。本システムでは RISC Zero zkVM によって投票集計の正当性を証明するために使用する。

RISC Zero zkVM

RISC-V アーキテクチャ上で通常の Rust コードを実行し、その実行が正しく行われたことの STARK 証明を生成するゼロ知識仮想マシン。ゲストプログラムとホストプログラムから構成される。

レシート（Receipt）

zkVM が生成する暗号証明オブジェクト。内部に Seal（STARK 証明本体）とジャーナル（公開出力）を含む。Receipt::verify(image_id) によって、特定のゲストプログラムが正しく実行されたことを第三者が検証できる。

ジャーナル（Journal）

zkVM ゲストプログラムの公開出力。検証済み集計結果、除外された投票数、入力コミットメント、包含ビットマップルート等を含む。レシートに暗号学的に束縛されており、改ざんできない。

Image ID

コンパイル済みのゲストプログラムバイナリを一意に識別するハッシュ値。レシート検証時に期待される Image ID と照合することで、意図したゲストプログラムによって生成された証明であることを確認する。プローバーイメージの更新時に同期して更新が必要。

詳細: Image ID

ゲストプログラム（Guest Program）

zkVM 内部で実行される Rust プログラム。投票データの検証と集計を行い、結果をジャーナルとして出力する。ゲストの実行内容は STARK 証明によって保証される。

ホストプログラム（Host Program）

zkVM の外部で動作し、ゲストプログラムの実行と証明生成を制御する Rust プログラム。入力データの読み込み、zkVM の起動、レシートとジャーナルの出力を担う。

検証サービス（Verifier Service）

Rust で実装された独立した STARK レシート検証プログラム。Receipt::verify(expected_image_id) を実行し、レシートの暗号学的正当性を確認する。結果は verification.json として保存される。

詳細: 検証サービス

フェイクレシート（Fake Receipt）

RISC0_DEV_MODE=1 で生成される暗号学的保証のないレシート。開発効率のためのモックであり、検証サービスは InnerReceipt::Fake を自動検出して dev_mode ステータスを返す。本番環境では使用してはならない。

検証パイプライン

E2E 検証可能投票（End-to-End Verifiable Voting）

投票者が自分の投票について「意図通りに投じた」「正しく記録された」「正しく集計された」の 3 段階を独立に検証できる投票方式。システム運営者を信頼せずとも投票の完全性を確認できることが目標。

Cast-as-Intended（意図通りの投票）

検証の第 1 段階。投票者が保持するレシート（選択肢、乱数、コミットメント）を再検証し、投票時に意図した選択が正しくコミットメントに反映されたことを確認する。クライアント側で完結する。

Recorded-as-Cast（記録通りの保存）

検証の第 2 段階。コミットメントが掲示板に正しく記録されたことを、RFC 6962 の包含証明と整合性証明によって確認する。掲示板が追記専用であること（投票が削除・改変されていないこと）を暗号学的に保証する。

Counted-as-Recorded（記録通りの集計）

検証の第 3 段階。掲示板に記録された全投票が zkVM の集計に過不足なく含まれたことを確認する。除外された投票がないこと（excludedCount == 0）は最重要不変条件。

STARK 検証（STARK Verification）

検証の第 4 段階。STARK レシートが暗号学的に正当であること、および期待される Image ID で生成されたことを確認する。ジャーナルの内容が正しい実行結果であることの最終的な保証。

検証チェック（Verification Check）

検証パイプラインを構成する個別の原子的な検証項目。20 個のチェックがあり、それぞれ一意の ID、所属する検証段階、証拠種別、重要度を持つ。

詳細: チェック一覧

ゲーティングロジック（Gating Logic）

検証チェックの結果を集約し、「Verified」「Verification Failed」「Warning」のいずれを表示するかを決定するロジック。必須チェックが 1 つでも failed であれば Verified は表示されない。

詳細: ゲーティングロジック

証拠種別

検証チェックに使用するデータの出所を示す分類。local（投票時に確定したユーザー固有データ）、public（掲示板や公開 API から取得可能なデータ）、zk（zkVM ジャーナルに含まれるデータ）、demo（教育用シミュレーション由来データ）の 4 種別がある。

重要度（Criticality）

検証チェックの必須性を示す分類。required（失敗すれば Verified をブロック）と optional（補助的で、単独では Verified をブロックしない）の 2 段階。

掲示板と透明性

掲示板（Public Bulletin Board）

全投票コミットメントを時系列で記録する追記専用のログ。RFC 6962 の Certificate Transparency モデルに基づき、包含証明と整合性証明によって第三者が監査可能な透明性を実現する。

詳細: CT Merkle ツリー

RFC 6962

Certificate Transparency（証明書の透明性）の標準規格。追記専用の Merkle ツリー、リーフハッシュ（0x00 プレフィックス）とノードハッシュ（0x01 プレフィックス）のドメイン分離、包含証明、整合性証明の仕様を定義する。本システムの掲示板は、この規格のハッシュ規則と証明アルゴリズムを参照した CT スタイル実装を採用している。

STH（Signed Tree Head）

掲示板の特定時点における状態の要約。ログ ID、ツリーサイズ、タイムスタンプ、ルートハッシュを含む。複数の独立したソースからの STH を比較することで、サーバーが異なるクライアントに異なるツリーを提示するスプリットビュー攻撃を検出する。

スプリットビュー攻撃（Split-View Attack）

掲示板サーバーが異なるクライアントに異なるツリー状態を提示する攻撃。特定の投票者に対してのみ投票を除外したツリーを見せることで、不正を隠蔽しようとする。整合性証明と STH の第三者検証によって検出される。

ルート履歴（Root History）

掲示板のルートハッシュ、ツリーサイズ、タイムスタンプの時系列記録。投票時のルートが最終ツリーの有効なプレフィックスであることを、整合性証明で検証する際に参照する。

改ざんシナリオ

改ざんシナリオ（Tamper Scenario）

検証システムが不正をどのように検出するかを教育的に示すシミュレーション。S0（正常）から S5（複合改ざん）まで 6 種類が定義されている。

詳細: 改ざんシナリオ

投票除外（Vote Exclusion）

一部の投票を集計から意図的に除外する攻撃。zkVM ジャーナルの excludedCount > 0 として検出される。本システムの最重要不変条件により、投票除外がある場合は「Verified」を表示しない。

主張集計改ざん（Claimed-Tally Tampering）

公開表示する集計値（claimed tally）を、zkVM が証明した実際の集計値と異なる値に書き換える攻撃の教育的シミュレーション。zkVM の入力・レシート・ジャーナルは正常なまま、公開表示のみを改ざんする。counted_tally_consistent チェックで検出される。

excludedCount

zkVM ジャーナルに含まれる、集計から除外された投票数。0 でなければならない。0 より大きい場合は投票除外が発生しており、いかなる場合も「Verified」を表示してはならない。

インフラストラクチャ

ECS Fargate

AWS のサーバーレスコンテナ実行環境。本システムでは STARK 証明生成に必要な大量のメモリ（32 GB）と CPU（16 vCPU）を提供するために使用する。アイドル時のコストは 0。

詳細: 非同期プローバー

Step Functions

AWS のワークフローオーケストレーションサービス。イメージ署名検証 → ECS プローバー実行 → コールバックの一連のフローを管理する。

非同期証明モード（Async Proving）

SQS → Step Functions → ECS Fargate の経路で STARK 証明を非同期に生成するモード。集計リクエスト（POST /api/finalize）は 202 Accepted を返し、クライアントはステータスポーリングで完了を待つ。

同期証明モード（Sync Proving）

ローカルプロセスで zkVM ホストバイナリを直接実行し、STARK 証明を同期的に生成するモード。開発環境で使用される。

イメージ署名検証（Image Signing）

ECS タスクで使用するプローバーコンテナイメージが、信頼できるビルドパイプラインから生成されたことを検証する仕組み。AWS Signer を使用し、Step Functions のゲートとして機能する。

詳細: イメージ署名

証明バンドル（Proof Bundle）

zkVM の実行結果を検証可能な形で保存・配布するためのアーティファクト群。公開許可リストに基づいて bundle.zip が作成され、非公開ファイルは含まれない。現行実装では、非同期バンドルは public-input.json / receipt.json / journal.json を含み、同期バンドルはこれに加えて metadata.json などの公開補助ファイルを含む場合がある。

詳細: バンドル構造

セッションと API

セッション（Session）

一連の投票フロー（セッション作成 → 投票 → 集計 → 検証）を管理する単位。一意の sessionId（UUID v4）で識別される。投票・集計中は 30 分、検証中は 24 時間の有効期限を持つ。

選挙（Election）

投票の論理的な単位。一意の electionId（UUID v4）で識別され、コミットメントのドメイン分離に使用される。選挙設定ハッシュ（electionConfigHash）が期待投票数などの設定を束縛する。

集計確定（Finalization）

全投票の収集後に zkVM 入力を構築し、STARK 証明を生成するプロセス。同期モード（ローカル実行）と非同期モード（ECS Fargate）の 2 つの実行パスがある。

X-Session-ID

多くの API リクエストで付与される HTTP ヘッダー。セッションスコーピングに使用され、異なるセッション間のデータアクセスを防止する。POST /api/session は新規セッション作成のため不要で、/api/verification/bundles/:sessionId/:executionId 系はパスパラメータで参照対象を指定する。

Turnstile

Cloudflare が提供する CAPTCHA サービス。/api/vote と /api/finalize で Bot による不正アクセスを防止するために使用する。開発環境では TURNSTILE_BYPASS=1 でバイパス可能。

定数

参考文献

本システムの設計に直接関わる文献を掲載しています。

[1] J. Benaloh, R. Rivest, P. Y. A. Ryan, P. Stark, V. Teague, P. Vora. “End-to-end verifiability,” arXiv:1504.03778, 2015. https://arxiv.org/abs/1504.03778

E2E 検証可能投票の基本モデル（Cast-as-Intended / Recorded-as-Cast / Counted-as-Recorded）を定義した文献。本システムの 4 段階検証モデルはこのフレームワークに基づいている。

[2] M. Harrison, T. Haines. “On the Applicability of STARKs to Counted-as-Collected Verification in Existing Homomorphic E-Voting Systems,” in Financial Cryptography and Data Security: FC 2024 International Workshops, LNCS, Springer, 2024. https://doi.org/10.1007/978-3-031-69231-4_4