はじめに

最終更新: 2026-10-12

投票結果に「B は 20 票」と表示されたとします。その数字を見ただけでは、自分が B に入れた一票が数えられたかは分かりません。集計する側が票を抜いたり、表示する数字を書き換えたりしても、結果の画面は作れてしまいます。

STARK Ballot Simulator は、この疑問を実際に確かめるための投票デモです。投票するとレシートを受け取り、掲示板に載った自分の票を確認し、集計に使われたことと計算の正しさを検証します。意図的に票を抜く、集計表示を変えるといった操作も試せるので、「何を変えると、どの証拠が食い違うか」を観察できます。

説明の中心に置くのは、A〜E の選択肢から B に投票した一人です。この一票と 63 票のボット投票を合わせた、64 票の小さな選挙を追います。暗号の用語は、それが必要になる場面で説明します。

実際の選挙に使うシステムとしては設計していません。たとえば、このデモでは集計するサーバーに投票先と乱数を送ります。公開される証拠から投票先を隠す仕組みはありますが、運営者に対しても秘密投票を実現しているわけではありません。

公開状態

実装は 公開ソースリポジトリ で確認できます。検証画面から取得した bundle.zip と、そのリリースに対応するソースを使えば、手元のコンピューターでも証明と公開データを照合できます。

まずは 投票して、結果を確かめる ところから始めましょう。結果を受け取ることと、その結果を信用できる根拠を得ることの違いが、画面を通して見えてきます。

投票して、結果を確かめる

最初は改ざんのない通常シナリオ S0 で、B に一票を入れてみます。操作は「開始する → 投票する → 集計する → 検証する」の順です。

投票する

Home で開始すると、自分用のセッションが作られます。Vote 画面で A〜E から B を選んで送信すると、投票レシートが返ります。レシートには、票を識別する値と掲示板上の位置が記録されています。このデモでは自分の票はインデックス 0 に置かれます。

ブラウザは、選択した B と、その投票用に作った乱数を手元に残します。あとで「返ってきたレシートは、確かに自分が送った票のものか」を確認するためです。続いて 63 票のボット投票が加わり、進捗表示が完了すると集計へ進めます。

セッションのデータを取得するための鍵もブラウザに保存されます。この鍵が capability token です。別のセッションのデータを取り違えたり、鍵を失ったりした場合は検証に必要な情報を取得できません。

集計する

Aggregate 画面で S0 を選び、集計を開始します。サーバーは票を数えるとともに、どの入力からどの結果を得たかを示す証拠を作ります。この一連の作業を 集計確定（finalization） と呼びます。

集計プログラムを実行したことを、あとから確かめられる暗号学的な証拠が STARK 証明です。AWS 上でこの証明を作る場合は時間がかかるため、画面で完了を待ちます。ブラウザはサーバーへ定期的に進捗を問い合わせます。成功すると Result 画面へ進み、候補ごとの得票数を表示します。失敗やタイムアウトであれば、結果の成功として扱いません。

ここで得られたのは、集計結果と検証用の材料です。まだ結果の数字だけを信用する必要はありません。

検証する

Result から Verify へ進むと、票の記録、集計への反映、計算の証明を確かめます。証明を運ぶデータを STARK レシートと呼びます。その検証が未開始なら開始し、実行中は結果を待ちます。ブラウザに残した投票時の情報も、この段階で使います。

画面の Verified は、必要なチェックがすべて通った場合にだけ表示できます。実行中や証拠不足ならその状態を示し、データが食い違えば失敗を示します。計算の証明だけが成功しても、投票者の票が抜けていれば全体の成功にはなりません。

S0 でも、第三者が観測する掲示板との照合先を設定していない場合は Warning（制限付き）になります。改ざんを見つけたという意味ではなく、その外部照合を行っていないことを示します。

ローカル開発用の pnpm dev では、証明の代わりに動作確認用の代替データ（mock）を使います。また、実際の zkVM を動かしていても開発用レシートを使う構成があります。これらは画面や処理の動作を試すためのもので、本番用の STARK 証明と同じ成功表示にはしません。

票を抜いたら、何が起きるか

通常の流れを確認できたら、新しいセッションで S1 を選んでみます。S1 は、自分の票を掲示板には残したまま、集計プログラムに渡す入力から抜くシナリオです。

この場合、掲示板に票があることは確認できても、集計に反映されたことは確認できません。「記録されている」と「数えられている」が別々のチェックになっている理由を、画面上で確かめられます。他の変更も 改ざんシナリオ で試せます。

証拠を持ち帰る

検証画面から bundle.zip をダウンロードできます。中には計算の証明と、公開して照合できる入力・出力が入っています。サーバーの検証結果に頼らず、自分の環境で証明を検証するための材料です。

ダウンロードにはセッションの鍵が必要ですが、ZIP の中身は第三者に渡せるよう秘密情報を除いてあります。検証サービスのレポート verification.json は別ファイルとして取得し、ZIP には含めません。実行手順は 手元で証拠を検証する に続きます。

一票を結果までつなぐ

B に入れた一票が集計に含まれたと言うためには、何を確かめればよいでしょうか。票の受け取り、記録、集計、表示の間には、それぞれ別の取り違えや改ざんの余地があります。

四つの問い

それぞれの答えを支える証拠を、投票から結果までつなぎます。最後の計算の証明だけでは、最初の三つの答えは得られません。

flowchart TB
  V["B を選んだ記録"] --> R["投票レシート"]
  R --> B["掲示板にある票"]
  B --> T["集計に使われた票"]
  T --> O["表示された結果"]
  P["計算の証明"] --> T

同じ一票を見ていることが大切

一つひとつの証拠が正しくても、別の選挙や別の集計の証拠を混ぜてしまえば、B の一票を確認したことにはなりません。そこで選挙の識別子、掲示板のルート、入力を要約するハッシュなどを照合し、証拠同士を結び付けます。

たとえば、サーバーが証明を作るときだけ一票を抜き、ダウンロード用の入力には全票を載せたとします。公開入力がもっともらしく見えるだけでは、この違いに気付けません。入力コミットメント は、証明に使った入力と公開した入力が対応するかを確かめるための仕組みです。

誰が何を確かめるか

ブラウザは投票時の選択と乱数を保持し、返されたレシートとの対応を確かめます。サーバーは掲示板や集計に関するチェックを行い、Rust の検証サービスが STARK レシートを検証します。ブラウザはその結果と自分の確認結果を合わせ、最終表示を決めます。

ブラウザ自身が STARK レシートを暗号検証する構成ではないため、通常の画面ではサーバーの検証結果を受け取ります。この部分を独立に確かめたいときは、ダウンロードした ZIP と期待するプログラムの識別子（Image ID） を使って、検証サービスを手元で実行できます。

また、掲示板のハッシュが一致していることと、運営者が全員に同じ掲示板を見せていることは別の問題です。独立した観測先と照合する仕組みと、その観測先を用意する条件は STH ダイジェスト で説明します。

投票の記録を確かめる

B に投票したあとで、サーバーが「受け付けました」と返すだけでは、何を受け付けたのかが残りません。そこで、選択肢と乱数から計算したコミットメントを掲示板に記録し、その記録の位置と掲示板の状態を投票レシートとして返します。

この一票が掲示板の先頭、インデックス 0 に入り、その後に 63 票が追加されるとします。確かめたいのは、最初の記録が確かに B を表すことと、64 票になった掲示板にも同じ記録が残っていることです。前者は手元の選択肢と乱数からの再計算で、後者は掲示板のハッシュと Merkle 証明で確認できます。

ただし、自分に見せられた掲示板が筋の通ったものでも、ほかの人に別の掲示板を見せている可能性は残ります。掲示板の状態を表す STH ダイジェストを別の記録源と照合するのは、その食い違いを探すためです。同じサーバーからもう一度値を取るだけでは、独立した確認にはなりません。

記録が残ることと、集計に使われることも別です。集計側はこの掲示板のルートを受け取り、各票がそこに含まれるかを調べます。こうして、投票時の記録が次の計算の基準になります。

投票コミットメント

B に投票したことを後から確かめたい。しかし、掲示板に「B」とそのまま載せると選択肢が見えてしまいます。そこでブラウザは、選択肢 B、選挙 ID、投票ごとに生成する 32 バイトの乱数をまとめて SHA-256 に渡し、32 バイトの値を作ります。これが投票コミットメントです。

選択肢が五つしかないため、B だけをハッシュしても、A〜E を試せば元の選択肢が分かります。乱数は、この総当たりを困難にするために加えます。選択肢と乱数の組を opening と呼びます。同じ opening からは同じコミットメントを計算できるので、ブラウザはこれを保存し、後で投票レシートの値と照合します。

掲示板と公開 ZIP に載せるのはコミットメントで、opening は載せません。ただし、このデモの投票 API には opening も送信し、サーバーが集計に使います。ここで隠しているのは公開物を見る人に対する選択肢であり、運用者に対する選択肢ではありません。

投票時と集計時に同じ値を確かめる

sequenceDiagram
    participant V as ブラウザ
    participant S as サーバー
    participant B as 掲示板
    V->>V: B と新しい乱数からコミットメントを計算
    V->>S: コミットメントと opening を送信
    S->>S: opening から再計算して照合
    S->>B: コミットメントを追記
    S-->>V: コミットメント・位置・投票時のルート
    V->>V: 保存した opening からレシートを照合

集計時には、zkVM ゲストも opening から同じ計算を行います。さらに、そのコミットメントが掲示板に含まれることを確かめてから B の得票数に加えます。ブラウザは手元に保存した opening、ゲストはサーバーから渡された opening を使うため、両者の確認は異なる場所で行われます。

コミットメントの一致だけでは、掲示板に記録されたことは分かりません。レシートにある位置とルートを使った確認は、CT Merkle ツリーが担います。

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

文字列の連結方法が違えばハッシュも変わります。ブラウザの TypeScript とゲストの Rust が同じ値を得られるよう、ハッシュに渡すバイト列を次の形に固定します。

commitment = SHA-256(
    UTF-8("stark-ballot:commit|v1.0")  // 24 バイト
    || election_id                    // UUID の 16 バイト
    || choice                         // 1 バイト
    || random                         // 32 バイト
)

入力は合計 73 バイト、出力は 32 バイトです。出力の 16 進数表記は 64 文字、0x を付けると 66 文字です。UUID や乱数を表示用文字列のままハッシュするのではありません。

ドメイン分離

先頭の固定タグは、このバイト列が投票コミットメント用であることを区別します。同じ SHA-256 を使っていても、掲示板のノードや集計入力のハッシュと解釈が混ざらないようにするためです。

投票には stark-ballot:commit|v1.0、入力コミットメントには stark-ballot:input|v1.0 を使います。掲示板のリーフには 0x00 と stark-ballot:leaf|v1、内部ノードには 0x01 を付けます。STH ダイジェストは専用タグを持たず、ログ ID を含む固定フォーマットで入力を区別します。

安全性

**秘匿性（hiding）**は、十分な乱数を秘密に保つことに依存します。投票ごとに新しい一様な 256 ビット乱数を生成し、再利用しません。同じ選挙で同じ選択肢と乱数を使うと、同じコミットメントになってしまいます。

**束縛性（binding）**は、一つのコミットメントについて、異なる選択肢に開く組を見つけることが困難であるという性質です。SHA-256 の衝突耐性が、異なる opening の組をあらかじめ作る攻撃に対する根拠になります。すでに固定された opening と同じ値になる別の opening を探す攻撃には、第二原像耐性が関わります。

この性質があっても、ブラウザ自体が改ざんされていれば手元の表示や保存内容は信頼できません。コミットメントが保証するのは、与えられた opening と記録の結び付きです。

TypeScript と Rust の実装同期

両実装は、タグの UTF-8 バイト、UUID のデコード、選択肢の 1 バイト表現、乱数のデコードを一致させます。片側だけを変えると、正しい投票でも照合できなくなります。共有の入力例に対するバイト単位の一致をテストし、ブラウザ・サーバー・ゲストが同じ約束を使うことを確認します。

掲示板に票が残っていることを確かめる

投票レシートにあるコミットメントが、後から掲示板から消されていないかを確かめます。そのために、掲示板全体を短いハッシュ値にまとめます。これをルートハッシュと呼びます。記録の値や順序が変わればルートも変わるので、投票時のルートを保存しておくことに意味があります。

ただし、ルートを二つ見比べるだけでは足りません。票が追加されてもルートは変わるからです。必要なのは「自分の票が投票時の掲示板にある」という包含証明と、「その掲示板を残したまま末尾へ票を足した」という整合性証明です。

投票時の一票と、締切時の64票をつなぐ

B のコミットメントがインデックス 0 に記録された時点では、掲示板は 1 リーフです。このときのルートは、そのコミットメントのリーフハッシュそのものになります。投票レシートには、位置 bulletinIndex=0 とルート bulletinRootAtCast が残ります。

その後、63 票のボット票が加わり、掲示板は 64 リーフになります。包含証明で最初のルートを確かめ、整合性証明で最初の 1 リーフが最後の 64 リーフの先頭に残っていることを確かめます。集計ゲストは、各票についてこの最終ルートへの包含を検証します。投票時の包含証明と集計用の包含証明は、対象時点が違います。

flowchart TB
  C[B のコミットメント] --> I[包含証明]
  I --> R1[投票時のルート<br/>1 リーフ]
  R1 --> P[整合性証明]
  P --> R64[締切時のルート<br/>64 リーフ]
  R64 --> G[集計ゲストの入力]

これは記録の削除や書き換えを物理的に不可能にする仕組みではありません。保持したルートと証明を照合することで、変更を検出する仕組みです。サーバーが人ごとに別々の掲示板を見せる問題には、さらに STH の照合が必要です。

RFC 6962 参照ハッシュ規則

Certificate Transparency（CT）は、証明書の記録を監査するための追記専用ログです。この掲示板は RFC 6962 のツリー分割と証明方式を参照し、投票コミットメントの記録に使います。

LeafHash(data) = SHA-256(0x00 || UTF-8("stark-ballot:leaf|v1") || data)
NodeHash(left, right) = SHA-256(0x01 || left || right)

リーフのタグは 20 バイト、コミットメントの data は 32 バイトです。左右の子ハッシュもそれぞれ 32 バイトです。0x00 と 0x01 を分けることで、リーフの内容を内部ノードの組として解釈させる混同を防ぎます。

本実装はリーフに独自タグを加え、後述する 1→2 の整合性証明にも固有の表現を使います。そのため、標準 CT の証明をそのまま交換できるという意味での RFC 6962 互換実装ではありません。

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

ツリーは順序付きのデータ列 d₀, …, dₙ₋₁ から作ります。

MTH({}) = SHA-256(空バイト列)
MTH({d₀}) = LeafHash(d₀)
MTH({d₀, ..., dₙ₋₁}) = NodeHash(
    MTH({d₀, ..., dₖ₋₁}), MTH({dₖ, ..., dₙ₋₁})
)

複数リーフの場合、k は n 未満で最大の 2 のべき乗です。たとえば 5 リーフなら 4 と 1、64 リーフなら 32 と 32 に分け、同じ規則を再帰的に適用します。最終的なデモは 64 票でも、追加途中の 3 票や 5 票に同じ規則を使えます。

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

掲示板はコミットメントを 0x なし・小文字・64 文字の 16 進数に正規化し、ハッシュ計算にはデコードした 32 バイトを使います。各記録には 0 始まりの連番を割り当てます。同一の投票 ID やコミットメントの二重追記を拒否し、追記時点のルートをタイムスタンプとともに保持します。

包含証明（Inclusion Proof）

一つの票からルートまで計算するために、ツリー全体を渡す必要はありません。各分岐で相手側の部分木のハッシュだけを渡せば、自分の側と組み合わせて上へ進めます。この兄弟ハッシュの列が Merkle パスです。

構造

finalization の検証リソースの voterEvidence.userVote.proof と、個票の inclusion-proof API が、この投票時点の証拠を返します。

PATH アルゴリズム

生成時は MTH と同じ位置 k で分割し、対象を含む側を再帰的にたどります。対象が左にあれば右部分木のハッシュ、右にあれば左部分木のハッシュをパスへ追加します。

検証時はリーフハッシュから始め、インデックスとツリーサイズで左右を決めてパスを折り畳み、期待ルートと比較します。64 リーフのツリーならパスは 6 ハッシュです。インデックス 0 の投票時点のツリーは 1 リーフなので、パスは空でも包含を確認できます。

Recorded-as-Cast では、ルート一致に加えて、leafIndex = bulletinIndex と treeSize = bulletinIndex + 1 を要求します。別の位置や別の時点の正しい証明を渡されても、自票の投票時証拠としては使いません。

整合性証明（Consistency Proof）

整合性証明は、古い m リーフの列が、新しい n リーフの列の先頭に同じ順序・同じ値で残ることを、二つのルートに対して確認します。追加後もルートが同じであることを要求するわけではありません。

構造

検証 API は古いルートを投票レシートの bulletinRootAtCast、新しいルートを集計の bulletinRoot と照合します。証明と一緒に届いたルート同士が整合するだけでは不十分です。

SUBPROOF アルゴリズム

MTH と同じ分割を使い、古いツリーに含まれる側を再帰的にたどります。m <= k なら左側の証明に右部分木のハッシュを加え、m > k なら右側の証明に左部分木のハッシュを加えます。再帰中に m = n となったとき、古いツリーの根をそのまま使える部分では空の証明、それ以外ではその部分木のルートを返します。

本実装の 1→2 の特殊ケースでは、2 番目のリーフのハッシュではなく、生の 32 バイトのリーフデータを返します。検証者は次を計算します。

newRoot = SHA-256(0x01 || oldRoot || LeafHash(second_leaf))

この特殊ケースは、掲示板の整合性証明を生成・検証する TypeScript の実装で使います。ゲストが行う包含検査とは別の処理です。

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

recorded_inclusion_proof と recorded_consistency_proof は、投票時の記録と最終掲示板をつなぎます。アプリではサーバーがこれらを評価してブラウザへ返しますが、ハッシュ計算と証明検証自体は、同じ証拠と期待ルートを持つ検証者が再実行できます。

集計ゲストが検証するのは、各入力票の最終掲示板への包含です。それに成功しても、サーバーが全票をゲストへ渡したことまでは分かりません。ゲストのスロット集計が、その不足を数えます。

掲示板の見え方を照合する

自分の票が掲示板に残っていても、ほかの人が同じ掲示板を見ているとは限りません。サーバーが、ある人には 64 票の掲示板、別の人には特定の票を外した 63 票の掲示板を見せたとします。それぞれについて包含証明を作れても、二人が見ている結果は食い違います。これをスプリットビューと呼びます。

この食い違いを探すには、掲示板の状態をほかの記録源と比較します。その照合用の短い値が STH ダイジェストです。どの掲示板かを示すログ ID、票数、時刻、ルートをハッシュでまとめます。

STH は Signed Tree Head に由来する名前ですが、この実装が行うのはダイジェストの一致確認であり、署名検証ではありません。また、同じサーバーの応答同士が一致しても、独立した証人の確認にはなりません。スプリットビューを検出するには、比較先が別の観測を保持していることが必要です。

締切時の状態を証明に結びつける

ゲストは入力のログ ID、票数、時刻、ルートからダイジェストを計算し、公開出力の sthDigest に記録します。サーバーは同じ締切状態を close-statement.json にまとめます。

flowchart TB
  C[締切時の掲示板状態] --> G[ゲストがハッシュ計算]
  G --> J[証明に結びついた sthDigest]
  C --> S[close-statement.json]
  J --> CMP[値を照合]
  S --> CMP
  T[別の記録源の STH] --> CMP

締切記録とジャーナルの一致は、集計がどの掲示板状態を参照したかを確かめる必須条件です。外部ソースとの一致は、その状態を別の記録と照合する追加の確認です。前者が成功したことを、後者も実施したこととして扱いません。

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

sth_digest = SHA-256(
    log_id           // 32 バイト
    || tree_size     // u32 LE、4 バイト
    || timestamp     // u64 LE、8 バイト、Unix 時刻ミリ秒
    || bulletin_root // 32 バイト
)

入力は合計 76 バイトです。LE はリトルエンディアン、すなわち整数の下位バイトから並べる方式です。ダイジェストには専用タグを付けず、次のログ ID と固定の並びで対象を区別します。

ログ ID

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

ログ ID は掲示板の存続中に変わらない識別子です。これをダイジェストに含めることで、票数やルートが同じでも、別の掲示板の締切状態と区別できます。

合意ロジック

検証 API は設定済みソースから応答を取得し、ジャーナルの値と照合します。「合意」とはこの照合の結果を指し、分散合意プロトコルを実行する意味ではありません。

外部応答はこの 5 フィールドだけからなる平坦なレコードです。sthDigest 以外は省略できますが、未知のキー、別名、ラッパーで包んだ応答は受け付けません。

成功には、必要な最小一致数に達し、比較した全レコードが一致することが必要です。設定済みソースに取得失敗、不正な応答、利用不能があった場合も成功にしません。多数の一致で一つの不一致を打ち消す仕組みではありません。判定の詳細は recorded_sth_third_partyに定義しています。

設定

ソース未設定では recorded_sth_third_party は任意チェックの not_run です。設定した場合は必須になり、必要な一致を得られなければ Verified を表示できません。署名検証や外部への自動公開を、この設定によって追加するわけではありません。

同一オリジンと外部 HTTPS の照合先

同一サーバー用の相対ソースとして使えるのは /api/sessions/:sessionId/bulletin/sth です。任意で auditorId クエリを一つ付けられます。API は現在のセッションから直接 STH の値を取り出すため、この内部照合のために HTTP 通信や認証ヘッダー転送は行いません。

このパスを通常の HTTP API として呼ぶ場合は X-Session-Capability が必要です。集計成功済みのセッションについて { data: { sth: { ... } }, meta } の応答を返します。この応答形式は、外部ソースに要求する平坦なレコードとは異なります。

絶対 HTTPS URL は、アプリと同じオリジンを指していても外部ソースとして取得します。セッションの認証情報を送らないので、その取得先はセッション認証なしで照合用レコードを返す必要があります。

同一サーバーが返す timestamp は session.voting.lastActivityMs で、ジャーナルのダイジェスト生成に使った時刻とは限りません。このため、応答の任意フィールドをすべて再連結してダイジェストを作り直すのではなく、上表の条件で照合します。

.env.local.example のコメント例は、相対テンプレートと最小一致数 1 の組です。これは照合の動作を試す構成です。同じサーバーしか観測していない以上、成功しても独立した外部監査を受けたとは言えません。

集計の計算を確かめる

掲示板に B の一票が残っていても、サーバーがその票を集計したとは限りません。「64 票を数えました」という説明に加えて、どのプログラムがどの入力を処理し、何を出力したのかを確かめる証拠が必要です。

このデモは、投票の検査と集計を zkVM という仮想マシンの中で実行し、その計算の証明を作ります。計算する小さなプログラムをゲスト、実行を準備して証明を作るプログラムをホストと呼びます。

ゲストの出力には、候補ごとの得票数だけでなく、提示されなかった票の数や、実際に計上した位置の記録も含めます。そのため、B の一票を外した入力を正しく集計しても、「1 スロットが未提示」という結果が証明に残ります。証明が有効であることと、投票結果を Verified と呼べることが分かれるのはこのためです。

検証者は、期待する集計プログラムの識別子 Image ID を先に選び、そのプログラムの実行証明かを確認します。

zkVM の基礎

サーバーに集計を任せると、その答えがどう計算されたかが見えません。すべての票を公開して各自が数え直す方法もありますが、それでは選択肢まで公開してしまいます。zkVM は、入力の一部を非公開のまま、指定したプログラムが計算した結果であることを検証できるようにします。

zkVM とは

zkVM は、プログラムの実行に対して暗号学的な証明を作る仮想マシンです。このデモでは RISC Zero を使い、Rust で書いた投票検査・集計プログラムをゲストとして実行します。ゲストは RISC-V の RV32IM 命令列として動きます。RISC Zero の技術仕様が、この実行モデルを定義しています。

たとえば B の一票について、ゲストは選択肢と乱数からコミットメントを作り直し、掲示板の記録と一致するかを調べます。さらに、その記録が最終掲示板に含まれることを確認してから得票数へ加えます。これを提示された全レコードに対して繰り返し、集計結果を出します。

証明が伝えるのは、**「指定したプログラムが、ある入力を処理して、この公開出力を出した」**という事実です。プログラムの設計は、レビューやテスト・形式化によって検討します。また、渡した入力が必要な票をすべて含むかは、ゲストが出す欠落数や公開入力との照合によって確認します。

ジャーナルとレシート

ゲストが公開する出力をジャーナル、その出力を計算に結びつける証明を含む成果物を zkVM レシートと呼びます。投票時にブラウザが受け取る「投票レシート」とは別のものです。

flowchart TB
  IN[入力票<br/>選択肢と乱数を含む] --> G[ゲストが検査・集計]
  G --> J[ジャーナル<br/>得票数と検査結果]
  G --> P[計算の証明]
  J --> R[zkVM レシート]
  P --> R

ジャーナルには得票数、除外スロット数、入力コミットメント、二つのビットマップルート、掲示板の締切状態などが入ります。レシートの検証が成功すると、この出力が指定ゲストの実行に結びついていると確認できます。出力を変更すれば、同じ証明では検証できなくなります。

別ファイルの journal.json は、レシート内部のジャーナルを読みやすい JSON に変換したものです。ファイル名だけで証明済みの値とみなさず、検証済みレシートから取り出した値との一致を確認します。

Image ID が必要な理由

攻撃者が「入力にかかわらず好きな得票数を返すプログラム」を作った場合も、そのプログラムを正しく実行した証明は作れます。だから検証者は、証明の差出人が指定したプログラムを無条件で受け入れてはいけません。

Image ID は実行対象のゲストを識別する 256 ビットの値です。検証者が別途選んだ期待値を Receipt::verify(expected_image_id) に渡すことで、意図したゲストの計算であることを確認します。具体的な選択方法は Image IDで定義します。

ホスト・ゲスト・検証サービス

ホストが「成功」とログに出したことは、レシートの検証成功ではありません。アプリでは独立した Rust バイナリ verifier-service に検証を委ね、そのレポートを受け取ります。ブラウザとサーバーがそれぞれ確かめる内容は、検証の実行フローにまとめています。

RISC Zero を採用する理由

集計規則を通常の Rust コードとして書き、テストできることが、この構成の利点です。暗号回路専用の言語へ集計ロジックを移し替えずに、実行するプログラムと検証するプログラムの識別子を対応させられます。

RISC Zero は長い実行を複数セグメントへ分割して証明できます。このデモは Composite receipt を配布し、Groth16 への圧縮は行いません。この STARK 証明経路は、証明ごとの秘密の初期設定値を作る trusted setup を必要としません。

開発用の fake receipt は、ゲストとの入出力連携を試すためのものです。実際の STARK 証明を持たないので、形式が似ていても上記の暗号学的保証は得られません。

STARK が計算を検査する考え方

STARK は、プログラムの各ステップの状態と、その間の遷移を検査対象にします。状態の列を有限体上の多項式として表し、命令の制約を満たしているかを確かめます。

概念的には、評価点の集合 H 上で制約多項式 C(x) がすべて 0 になることを調べます。H 上で 0 になる多項式を Z_H(x) とすると、制約を満たす場合は C(x) が Z_H(x) で割り切れます。STARK は、このような関係を Merkle コミットメントや FRI を使って効率よく検証します。FRI は、提示された値の列が低い次数の多項式として振る舞うかを少数の問い合わせで検査する仕組みです。

実際の証明方式の構成は RISC Zero の技術仕様と STARK by Handに詳述されています。アプリがレシートを採用する境界では、SDK の検証 API を使い、この数学的検証を独自に実装しません。

ゲストが票を調べ、数える

集計ゲストは、渡された票をそのまま足すプログラムではありません。B の一票が掲示板のインデックス 0 にあるなら、その位置、opening、コミットメント、包含証明を順に検査し、すべてを通過した場合だけ B の得票数へ加えます。

同時に、「検査に通らなかったレコード」と「掲示板にはあるのに渡されなかった位置」を記録します。64 スロットある掲示板に対し、63 票しか提示されなかったことを、計算結果自身に残すためです。

処理パイプライン

flowchart TB
  I[入力全体の形式と量を確認] --> V[各票を検査]
  V --> T[有効票を候補別に加算]
  V --> C[提示・除外・却下を記録]
  T --> J[ジャーナルを出力]
  C --> J
  I --> H[入力と締切状態のハッシュ]
  H --> J

入力全体が処理可能かという検査と、一票を有効と認める検査は分けています。処理量の上限を超えれば実行を拒否します。一方、範囲内の入力に無効票や重複があれば、それを却下した結果をジャーナルに残します。

投票の 6 段階検証

入力レコードを受け取った順に検査します。最初に失敗したところで、そのレコードの検査を打ち切ります。

1、2 を通過した時点で、そのスロットを seenBitmap に記録します。3〜6 で失敗しても「提示された」という事実は残ります。6 まで通過すれば includedBitmap も立て、対応する候補へ 1 票を加えます。

重複の検査は先着順です。先のレコードが検証に失敗しても、その位置を後続レコードでやり直すことはできません。コミットメントも、照合と重複検査を通過して登録された後は、包含検査に失敗しても予約されたままです。

コミットメントの計算は投票コミットメントの式、包含検査は CT Merkle の規則を使います。

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

スロットは掲示板上の位置、レコードはゲストに渡された票データです。一つの位置に重複レコードを何件送っても、掲示板のスロット数は増えません。この二つを分けると、何が不足したのかを説明できます。

スロットは「計上済み」「提示されたが未計上」「一度も提示されなかった」の三つに分かれます。

validVotes + invalidPresentedSlots + missingSlots = treeSize
seenIndicesCount = validVotes + invalidPresentedSlots
excludedSlots = missingSlots + invalidPresentedSlots

excludedSlots > 0 なら、少なくとも一つの掲示板スロットを数えられていません。rejectedRecords は、それとは別に、重複や範囲外を含む却下レコードの総数です。最後の例のように除外が 0 でも却下が 1 になり得ますが、アプリが Verified として受け入れるには却下も 0 であることを要求します。

入力レコードと得票数には、さらに次の関係が成立します。

sum(verifiedTally) = validVotes
validVotes + invalidVotes = totalVotes
rejectedRecords = invalidVotes
rejectedRecords >= invalidPresentedSlots

totalVotes はゲストへ提示したレコード数で、掲示板のスロット数ではありません。totalExpected は選挙設定が要求する票数です。ゲストはこれを入力から出力へ引き継ぎ、treeSize との一致は検証側が確認します。

ジャーナル出力

ジャーナルは、上の計算を検証者へ伝える公開出力です。下表は公開 JSON の名前と論理的な値を定義します。

ジャーナルの信頼モデル

期待する Image ID で本物のレシート検証が成功したとき、そのレシート内のジャーナルを、指定ゲストが出した結果として受け入れられます。得票数や不足数はゲストの計算結果ですが、選挙 ID、設定ハッシュ、掲示板ルート、期待票数は入力から引き継いだ値です。これらが対象の選挙・掲示板に一致することは、公開入力や投票時の記録との照合で確かめます。

inputCommitment は決められた公開フィールドだけを束縛します。sthDigest はゲストに渡された締切状態のハッシュであり、外部の記録源が同じ状態を観測したことを、それだけで示すものではありません。

レシート内部と JSON の表現

Rust の VerificationOutput は election_id: [u8; 16] などのフィールドを持ち、env::commit(&output) が RISC Zero serde で直列化します。この receipt 内部のバイト配置は公開 JSON の仕様ではありません。固定オフセットや手書きの packed layout で読みません。

ホストがデコードした camelCase JSON では UUID とハッシュがバイト配列で出力され、配布用 journal.json では UUID 文字列・16 進数文字列へ変換されます。検証サービスの decode-journalは、同じレシートを検証してから Rust の契約でデコードします。

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

seenBitmap と includedBitmap はそれぞれ treeSize 個のビットを持ち、提示された位置と計上した位置を表します。全ビットをジャーナルへ載せる代わりに、それぞれの Merkle ルートを載せます。

これにより、自票の位置 0 について「提示されて数えられた」「提示されたが無効だった」「提示されなかった」を証明に結びつけて調べられます。未計上の提示スロットがなければ、両ビットマップの集合もルートも一致します。バイト表現と個票の証明はビットマップ Merkleで定義します。

入力データ構造

入力の Rust フィールドは次のとおりです。opening を含む入力全体は公開 ZIP に入れません。

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

入力の境界条件

bulletin_root の全ゼロ、tree_size=0、timestamp=0 は拒否します。さらに、ツリーサイズ・期待票数・レコード数・各候補の得票数は最大 1,000,000、各パス長は最大 u16::MAX、全パスノード数は最大 1,000,000、推定構造化入力サイズは最大 64 MiB です。

votes.length > tree_size は、それだけでは入力全体の拒否理由になりません。上限内であれば個々の重複・範囲外レコードを検査し、却下数を出力できます。

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

現在の methodVersion は 14 です。これはジャーナル契約の識別に使います。実際に実行したゲストバイナリの識別は Image IDで行い、バージョン番号の一致だけで証明を受け入れません。

投票の却下・スロット分割・処理量の上限は、Lean の抽象モデルと Rust の共有ベクトルでも検査しています。その対応検査は、ゲストを含むシステム全体の実装証明ではありません。

計算するプログラムを指定する

「正しく実行された」という証明だけでは、どのプログラムを実行したのかが決まりません。攻撃者が任意の得票数を返すゲストを用意すれば、そのゲストについて有効な証明を作れてしまいます。検証者は、証明を受け取る前に、受け入れる集計プログラムを決めておく必要があります。

その識別に使うのが Image ID です。RISC Zero はゲストの ELF バイナリから 256 ビットの識別子を導出します。検証者は別途用意した期待値を Receipt::verify(expected_image_id) に渡し、指定したゲストの実行結果かを確認します。レシートに書かれた ID をそのまま期待値として採用するだけでは、プログラムの選択を差出人に任せたことになります。

RISC Zero の Image ID

flowchart TB
  S[レビューした集計プログラム] --> B[固定した環境でビルド]
  B --> E[ゲスト ELF]
  E --> I[Image ID を導出]
  I --> X[検証者が期待値として選択]
  R[受け取ったレシート] --> V[レシートを検証]
  X --> V

Image ID はゲストの実行イメージから決定的に導出されます。ELF ファイル全体を単純に SHA-256 した値でも、プローバーのコンテナイメージの digest でもありません。

ゲストのソース、依存ライブラリ、Rust コンパイラ、RISC Zero SDK、ビルド環境が変わり、生成されるゲストが変われば Image ID も変わり得ます。同じソース名や同じ methodVersion であることだけでは、同じバイナリの証拠になりません。

Image ID の導出

ホストはビルド時にゲスト ELF とその Image ID を埋め込みます。証明を生成せず、そのホストが使う値を確認するには、リポジトリルートで次を実行します。

./zkvm/target/release/host --print-image-id --json

出力には imageId と methodVersion が入ります。このコマンドは埋め込まれた値を表示するので、どのソースとビルド環境から作ったホストかを別途確認します。変更後の ID を確定するときは、新しいビルド出力先を使い、以前のゲスト成果物を再利用していないことを確かめます。

variant とアーキテクチャ

公開マッピングは、ビルド環境別に二つの値を管理します。

ARM64 と x86_64 はホスト側のビルド環境です。どちらもゲストの命令セットは RV32IM です。検証者のマシンの CPU に合わせて値を選ぶのではなく、受け取ったレシートを生成したゲストに対応する値を選びます。

各 variant は confirmed または unconfirmed の状態を持ちます。前者には imageId と由来の provenance があり、後者には requiredEvidence: "accepted-prover-release" があるだけで、期待 Image ID としては使えません。

Image ID マッピング

public/imageId-mapping.json は、公開検証者がバージョンとビルド由来を確認するための台帳です。現在の current は 14 です。変更後のゲストについて、default は採用済み ARM64 プローバーリリースの証拠を待つ unconfirmed、x86_64 は新しい出力先で行ったローカル production ビルドに基づく confirmed です。deprecated は空です。

マッピングは公開リポジトリで履歴を確認できます。ただし、正しい期待値として使うには、そのソースとビルド由来を信頼する判断が必要です。攻撃者が用意したマッピングとレシートを一緒に検証しても、その判断を省略したことには変わりありません。

Image ID の解決

アプリは検査済みジャーナルの methodVersion を使って期待値を解決します。現在の検証フローが受け入れるのは、現行のジャーナル契約です。

EXPECTED_IMAGE_ID_VARIANT は default または x86_64 に限定します。実行環境の自動判定は行いません。未知のバージョン、不正または読み込めないマッピング、未確認の variant はエラーになり、別の値で検証を続けません。

明示した EXPECTED_IMAGE_ID は、対象 methodVersion のゲストに対応させる必要があります。AWS のデプロイでは、選択したプローバーリリースの Image ID と method version を使い、公開マッピングとも照合します。公開マッピング自体が、コンテナを実行してよいという許可を与えるわけではありません。

ローカル検証での選択

verifier-service 単体は EXPECTED_IMAGE_ID を読みますが、EXPECTED_IMAGE_ID_VARIANT を直接は読みません。たとえばローカル x86_64 で生成したレシートの期待値は、次のスクリプトで導出します。

node verifier-service/scripts/read-image-id.mjs \
  public/imageId-mapping.json --variant x86_64

この出力を検証 CLI の --image-id または EXPECTED_IMAGE_ID に渡します。ARM64 の配布レシートには、そのリリースに対応するソースの確認済み default を使います。現在のソースでは default が未確認のため、ARM64 の期待値の解決と通常の App デプロイは停止します。

検証パイプラインでの役割

検証サービスはレシートラッパーの image_id を期待値と比較し、さらに暗号学的な Receipt::verify を行います。単に JSON の文字列が一致したことを証明検証の代わりにはしません。

アプリは stark_image_id_match と stark_receipt_verify の両方を必須とし、レポート・集計結果側の ID の整合も確認します。それらが成功しても、投票の記録、入力の完全性、表示の得票数に対する確認が残ります。

ゲスト更新とコンテナ更新

ゲストが変わる更新では、新しい Image ID を確定し、マッピング、検証側の期待値、生成するレシートをそろえます。片側だけの更新では、新旧の不一致として検証できなくなります。

一方、ゲストが変わらないコンテナの起動処理の更新なら、コンテナ digest が変わっても Image ID は変わらないことがあります。AWS はこの二つを別々に検査します。コンテナの出所と実行許可はイメージ署名、ゲストの実行結果は Image ID に対するレシート検証で確認します。

証明と公開入力を結び付ける

サーバーが自分の B 票を外し、63 票で集計の証明を作ったとします。そのうえで、公開ファイルだけを元の 64 票に戻したらどうなるでしょうか。証明そのものは 63 票の計算について有効でも、公開された投票列はその計算を表していません。

この差し替えを見つけるため、ゲストは処理した入力の公開部分をハッシュにまとめ、ジャーナルの inputCommitment に記録します。検証者も public-input.json から同じハッシュを計算し、検証済みレシートに結びついたジャーナルと比較します。63 件を処理した実行に 64 件の公開入力を組み合わせれば、この値が一致しません。

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

これは「公開された投票列が、証明済み実行のものか」を確かめる仕組みです。公開ファイルも 63 票のままならハッシュは一致し得ます。その場合でも、掲示板は 64 スロットなのでゲストの missingSlots が 1 になり、完全性のチェックで失敗します。入力の同一性と、全票が提示されたことは別々に確認する必要があります。

選択肢と乱数はこのハッシュの入力に含めません。投票コミットメントを使ってその公開部分を結びつけ、opening の正しさはゲストが投票ごとに検査します。また、公開ファイルの全フィールドがこの一つのハッシュに入るわけでもありません。

正準エンコーディング

公開入力は JSON ですが、JSON の文字列をそのままハッシュしません。空白やキーの順で値が変わらないよう、対象フィールドを決まったバイト列へ変換します。

バイトレイアウト

input_commitment = SHA-256(
    UTF-8("stark-ballot:input|v1.0") // 23 バイト
    || version                      // u32 LE、固定値 10
    || election_id                  // UUID の 16 バイト
    || bulletin_root                // 32 バイト
    || tree_size                    // u32 LE
    || total_expected               // u32 LE
    || votes_count                  // u32 LE
    || vote_entry ...               // 下記の順序で正準化
)

ここでの version=10 はハッシュ入力の形式を示す固定値です。public-input.json の version フィールドを取り込むものではなく、ゲストの methodVersion とも別です。

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

vote_entry =
    index             // u32 LE、4 バイト
    || commitment_len // u16 LE、2 バイト、固定値 32
    || commitment     // 32 バイト
    || path_len       // u16 LE、2 バイト
    || path_nodes     // path_len 個の 32 バイト値

votes_count は提示されたレコード数です。各レコードの index は掲示板上の位置であり、配列の何番目かに置き換えません。包含証明のパスノードも含むため、同じコミットメントでも別のパスを提示すればハッシュ入力は変わります。

フィールド一覧

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

入力コミットメントの対象外のフィールドも、公開ファイルを受け取る境界や別のチェックで検証します。

これらのファイルは、公開バンドルに同梱されます。一つのハッシュが一致しただけで全項目の確認を済ませず、それぞれが何と結びつくかをたどります。

正準化規則

ソート規則

投票レコードは index の昇順に並べます。正常入力のインデックスは一意です。重複があった場合も同じバイト列を作れるよう、次にコミットメントのバイト列、さらに Merkle パスのバイト列を辞書順に比較します。パスの共通部分が同じなら短い方を先にします。重複をこの順序で並べられることと、重複票を有効として集計できることは別です。

この正準化はハッシュを計算するための順序です。ゲストが入力レコードを検査するときの先着処理を並べ替えるものではありません。

エンディアン規則

整数はすべてリトルエンディアンです。u16 は 2 バイト、u32 は 4 バイトを使い、表現できない件数やパス長は拒否します。

16 進数正規化

UUID はハイフンを除いた 16 進数から 16 バイトへ変換します。コミットメント、ルート、パスノードは、0x があれば除去して 32 バイトへデコードします。文字列の大文字・小文字はデコード後の同じバイトを意味します。

TypeScript と Rust の同期

サーバーの TypeScript とゲストの Rust は、この同じ並びを独立に計算します。入力順序を入れ替えてもハッシュが変わらない性質や、長さ・整数の境界は、生成入力を使うテストと Lean が出力する入力コミットメントのベクトルで確認します。

アプリの counted_input_commitment_match はサーバー側での照合結果です。公開入力とレシートを入手した第三者は、ローカル検証で同じ対象フィールドの一致を再確認できます。これに成功しても、非公開の opening を公開したり、自票のブラウザ内データを再現したりすることにはなりません。

自票の採用状況を確かめる

「64 票のうち 63 票を数えた」という数字だけでは、数えなかった一票が自分の B 票かどうか分かりません。そこでゲストは、掲示板の位置ごとに、票を受け取ったか、数えたかを 1 ビットずつ記録します。

この記録をビットマップと呼びます。ゲストは二つのビットマップの Merkle ルートをジャーナルへ書き込みます。投票者は自分の位置のビットとその証明を取得し、レシートに結びついたルートと照合できます。

二つのビットで自票の状態を区別する

seenBitmap[i] は範囲内の位置 i が提示されたこと、includedBitmap[i] はその位置の票を有効と認めて計上したことを表します。インデックス 0 の B 票なら、見るのはそれぞれの先頭ビットです。

S1 のように自票を入力から外せば、掲示板は 64 スロットのままで、位置 0 のビットは両方 0 になります。S2 のように表示の得票数だけを変えた場合は、ゲストへの入力が元の 64 票なので、この一票のビットは両方 1 のままです。表示の改変は、別の得票数照合で見つかります。

Merkle 証明で確かめるのは、取得したビットがジャーナルのルートに結びつくことです。そのルートをゲストの計算結果として信頼するには、期待 Image ID に対するレシート検証も必要です。アプリの検証画面では、サーバーがこの個票証明を評価して結果を返します。

ビットマップの構造

ビット数は treeSize と同じです。64 スロットなら 64 ビット、すなわち 8 バイトです。

LSB-first ビットパッキング

位置 0 を最初のバイトの最下位ビットへ置き、位置が一つ進むごとに上位ビットへ進めます。8 ビット分を埋めたら次のバイトへ移ります。

byte[i / 8] の bit (i % 8) が、位置 i の状態

64 票すべてを計上: ff ff ff ff ff ff ff ff
位置 0 だけ未計上: fe ff ff ff ff ff ff ff

上の除算は整数除算です。最初の fe は、最下位ビットだけが 0 であることを示します。これは実装規則から作った説明用の値で、実行結果の採取例ではありません。

32 バイトチャンク分割

パックしたバイト列を 32 バイトずつ区切り、最後は 0 で埋めます。1 チャンクに 256 スロットが入るので、64 票のデモは 8 バイトの記録と 24 バイトのゼロからなる 1 チャンクです。このチャンクが Merkle ツリーのリーフになります。

Merkle ツリーの構築

ハッシュ規則は掲示板の CT Merkleと同じですが、リーフの中身は投票コミットメントではなく 32 バイトのチャンクです。

LeafHash(chunk) = SHA-256(0x00 || UTF-8("stark-ballot:leaf|v1") || chunk)
NodeHash(left, right) = SHA-256(0x01 || left || right)

各チャンクをハッシュし、隣同士を左右の子としてまとめます。奇数個で最後に余ったノードは、ハッシュを加えず次の段へ持ち上げます。1 リーフしかない 64 票のデモでは、そのリーフハッシュがそのままルートです。

Merkle 証明の生成と検証

証明の構造

GET /api/sessions/:sessionId/finalizations/current/bitmap-proofs/:kind/:voteIndex は、現在の集計について次の証明材料を返します。

応答は標準の { data, meta: { requestId } } 形式です。kind=included は計上、kind=seen は提示の証明を選びます。セッションの capability が必要で、要求できる voteIndex は自票の位置だけです。リーフ位置やビット位置は応答を信用して受け取るのではなく、要求した voteIndex から導出します。

検証手順

1. 証明に結びついたジャーナルから、正の整数 treeSize と、対象の 32 バイトルートを得る。0 <= voteIndex < treeSize を確認する。
2. leafIndex = floor(voteIndex / 256)、bitOffset = voteIndex % 256、leafCount = ceil(treeSize / 256) を計算する。
3. チャンクと各兄弟ハッシュが 32 バイトであること、パスの長さと左右の並びが leafIndex と leafCount から決まるツリー形状に合うことを確認する。
4. 最後のチャンクのうち treeSize より後の未使用ビットが、すべて 0 であることを確認する。
5. リーフハッシュから始め、パスをたどってルートを再計算する。兄弟が左なら NodeHash(sibling, current)、右なら NodeHash(current, sibling) を使う。
6. includedBitmapRoot または seenBitmapRoot と一致した場合に、対象ビットを状態として読む。

64 票の 1 リーフ構成なら auditPath は空です。ただし、チャンク長、位置の範囲、ゼロ埋め、ルートの照合は必要です。空のパスを無条件の成功として扱いません。

ビット抽出

byteIndex = floor(bitOffset / 8)
bitInByte = bitOffset % 8
value = (chunk[byteIndex] AND (1 << bitInByte)) != 0

included=false だけでは未提示と無効を区別できません。検証できた seen の証明を組み合わせて分類します。seen の証拠を取得・検証できなければ、理由は unknown_excluded として扱い、推測で決めません。

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

ジャーナルに入るのは二つのルートで、ビットマップ全体ではありません。ホストは入力からビットマップを再構成し、ゲストのルートと一致した場合に非公開の補助ファイルを出力します。サーバーも保存・復元時に長さ treeSize とルートを照合し、集計成功と同じ保存処理で採用します。

included-bitmap.json と seen-bitmap.json は個票証明の生成元ですが、公開 ZIP には含めません。証拠が保存されていなければ、件数やルートだけから中身を推測して補いません。証拠不足と、取得済み証明の不一致ではチェック結果も異なります。正確な分岐は counted_my_vote_includedに定義しています。

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

API が要求を自票の位置に制限しても、返すのはその位置を含むチャンク全体です。したがって同じチャンク内のほかの位置の状態も読めます。64 票のデモでは全票の計上・提示状態が一つのチャンクに入ります。選択肢や乱数を示すビットではありませんが、一票だけの状態を開示する方式でもありません。

チャンクを小さくすれば開示範囲を減らせる一方、ツリーのリーフ数、証明パス、ゲスト内のハッシュ計算は増えます。現行のデモはユーザー 1 票とボット 63 票を対象に、32 バイト単位を使っています。

ビット境界、ゼロ埋め、ルート計算は、生成入力のテストと Lean のビットマップベクトルで検査します。

ホストと証明生成

ゲストが投票を検査するには、サーバーが保存した opening と、掲示板の記録を一つの入力にまとめる必要があります。ホストはその入力を読み、ゲストの実行と証明生成を行い、レシートと公開出力を書き出します。

B の一票なら、位置 0、選択肢 B、投票時の乱数、コミットメント、最終掲示板への包含証明を渡します。投票時のレシートにある小さいツリーへの証明を、そのまま集計入力に流用するわけではありません。

パイプライン全体像

flowchart TB
  V[保存した投票と opening] --> I[TypeScript が入力を構築]
  B[最終掲示板と包含証明] --> I
  I --> H[Rust ホスト]
  H --> G[ゲスト実行と証明生成]
  G --> R[レシート]
  G --> J[デコードした公開出力]
  R --> A[配布用ファイルを構築・検査]
  J --> A

入力を作る TypeScript、計算を証明する Rust、配布用ファイルを作る処理は、それぞれ受け渡し先で内容を検査します。ホストの終了コードだけで集計を成功として扱わず、出力の形式と整合性も確認します。レシートの暗号学的検証は、さらに検証サービスが担当します。

入力構築

現行 PoC の選挙構成

デモのセッションは A〜E、ユーザー 1 票とボット 63 票、合計 64 スロットです。最終的な掲示板ツリーの深さは 6 になります。この構成は contract-constants.ts と election-config.ts に定義します。

64 はデモの選挙設定であり、Merkle アルゴリズムやゲストの処理上限ではありません。入力は選挙設定の totalExpected と掲示板の treeSize を別々に持ち、検証側で一致を確認します。

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

入力ビルダーは、掲示板の最新 STH スナップショットからルート、サイズ、時刻を取得します。選挙設定とそのハッシュの一致を確認し、保存した各票の選択肢を A=0〜E=4 に変換します。その票の元の掲示板インデックスを使って、最終状態への包含証明を取得します。

通常の入力ではインデックスが 0 から連続することを要求します。S1 の除外では、位置 0 を外しても残りを 0〜62 に振り直さず、1〜63 のまま渡します。掲示板は 64 スロットなので、ゲストは位置 0 が足りないと数えられます。

Merkle パスの解決戦略

包含証明は、そのセッションの掲示板から取得します。リーフ位置とツリーサイズを照合し、取得できない証明や一致しない証明で入力構築を続けません。保存した投票レコードは、代わりに使う別のパスを持ちません。

ホストプログラムの実行

TypeScript のアダプターは、UUID とハッシュの文字列をバイト配列へ変換し、Rust が読む JSON を作ります。ホストは固定長配列と現在の入力フィールドを検査し、ExecutorEnv へ直列化して、組み込まれたゲストを実行します。処理量の上限もゲストの境界条件に従います。

正常に証明を生成すると、ホストはレシート内部のジャーナルをデコードして、出力 JSON を作ります。

ビットマップは入力から再構成し、ゲストの公開ルートとの一致を確認できた場合に書き出します。出力の UUID・ハッシュを配布用の文字列表現にする処理は、ホストの生出力を受け取ったアダプターや artifact 生成処理が行います。

Image ID の確認だけなら host --print-image-id --json を使います。この場合は入力ファイルの読み取りも証明生成も行いません。

同期モード

ローカルの実証明プロファイルでは、Node.js が zkvm/target/release/host を子プロセスとして起動し、終了を待ちます。shell を介さず引数を渡し、専用の POSIX プロセスグループで起動します。

入力と出力は .zkvm-temp/ に置きます。アダプターは出力の現在のフィールド集合を検査し、欠落や未知のフィールドを拒否してから、アプリ用の値へ変換します。UUID は文字列、ハッシュは 0x 付き 16 進数へそろえます。

終了と一時ファイル

証明の期限は 600 秒です。期限到達またはホスト終了時には、所有するプロセスグループへ SIGTERM を送り、最大 5 秒待ってから SIGKILL、さらに最大 1 秒待ちます。残ったプロセスの終了を確認できなければ成功にはしません。これは Linux、WSL、macOS の POSIX グループを対象にした後始末です。

成功・失敗のどちらでも、入力と四つの出力ファイルの削除を試みます。ファイルがすでに無い場合は問題とせず、それ以外の削除失敗は安全な警告として残します。起動失敗、非ゼロ終了、外部シグナル、期限切れ、サーバー停止、出力欠落を区別して扱います。

非同期モード

AWS では、時間のかかる証明生成を ECS Fargate の専用タスクへ渡します。API は完了まで接続を保持せず、ブラウザが現在の集計状態を問い合わせます。

sequenceDiagram
  participant API as API
  participant Q as キューと実行管理
  participant H as Fargate のホスト
  participant S3 as S3
  participant C as 完了処理
  API->>S3: 非公開の入力を保存
  API->>Q: 証明生成を依頼
  Q->>Q: 実行条件とイメージ署名を確認
  Q->>H: タスクを起動
  H->>S3: 入力を取得
  H->>H: ゲスト実行と証明生成
  H->>S3: 検査済み成果物を保存
  H-->>Q: タスク終了
  Q->>C: 成功または失敗を通知

ホストの入出力契約は同期実行と共通です。実行の重複・取消・再試行や結果の保存は、非同期プローバーの処理が担います。

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

非同期の入力ファイルは、通常のゲスト入力に加えて election_config を含みます。ホスト CLI では省略可能ですが、非同期の公開ファイル生成には必要です。内側の設定キーは camelCase を使います。

コンテナの entrypoint は Rust の prover-artifacts を呼び、入力とホスト出力から journal.json、public-input.json、election-manifest.json、close-statement.json を作ります。現在の method version、入力コミットメント、正準ハッシュ、各値の対応を検査し、生成した四つのファイルを読み直して確認します。その後、許可されたファイルだけで ZIP を構築・検査し、S3 にアップロードします。

非公開の入力と二つのビットマップは ZIP に含めません。S3 にはホストの *-output.json、*-receipt.json、公開ファイル、非公開ビットマップ、ZIP が保存されます。公開 journal.json は ZIP 内にあり、その固定名で ZIP の隣へ別オブジェクトを保存する方式ではありません。同梱ファイルの正確な一覧はバンドル構造に定義します。

失敗時は分類だけを持つ非公開の failure-marker.json の保存を試み、実行管理から失敗の完了処理を呼びます。この記録も公開 ZIP には入りません。

非同期モードの特性

証明生成が終わったことと、検証サービスがその証明を検証したことは別の状態です。AWS では検証の要求を受けた後、別のキューと worker がレシートを確認します。

開発モードの動作

開発中に毎回 STARK 証明を作ると、入出力の修正を確認するにも時間がかかります。そこで、用途に応じて次の実行を使い分けます。

ホストと証拠の組は、実行プロファイルの選択で決まります。

開発用ホストは RISC0_DEV_MODE=1 で証明を作らずに fake receipt を返せます。production feature のビルドはこの開発モードを受け入れません。AWS entrypoint は対象の production プロファイルを要求し、ホストの環境から開発モード指定を除去します。

アプリでどの実行を使うかは、起動時に確定する runtime profile が決めます。fake receipt は入出力契約を試す材料ですが、計算の暗号学的証拠ではありません。検証サービスも成功へ昇格させず、開発用の診断結果として区別します。

検証サービス

ホストがレシートを作れても、それを検証者が受け入れてよいかは別に確かめます。verifier-service は、レシートと期待する Image ID を受け取り、RISC Zero の Receipt::verify を実行する Rust の CLI です。

アプリはこの CLI をサーバー側で呼び出し、ブラウザへ結果を返します。

検証フロー

flowchart TB
  R[レシートを読み込む] --> M[Image ID のメタデータを照合]
  M --> V[期待 Image ID で<br/>暗号学的に検証]
  V --> O[成功・失敗・開発用を報告]

メタデータの一致は、証明を検証する前の確認です。JSON の image_id を期待値に書き換えても、その値を使った暗号学的検証に通るわけではありません。

入力形式の解決

非開発用のレシートには、JSON のトップレベルの image_id が必要です。receipt.imageId だけでは代用できません。検証サービスはこの値を期待 Image ID と照合した後、レシート本体を検証します。

CLI がこれらの形式を読めることと、アプリの公開 ZIP として適切であることは別です。アプリはバンドルの構造と公開境界も検査してから検証サービスへ渡します。

Image ID の照合と開発用レシート

InnerReceipt::Fake は開発用のレシートです。image_id が存在して期待値と異なれば、Fake でも failed です。Fake の場合に限りメタデータがなくても暗号学的検証の分岐へ進み、検証が成功するか InvalidProof で拒否されたときは dev_mode、その他の失敗は failed として報告します。

非 Fake はメタデータ欠落を拒否します。メタデータが一致し、Receipt::verify(expected_image_id) が成功した場合だけ success です。production feature は SDK の開発モードを無効化し、開発モードを扱えるビルドも Fake を成功とは報告しません。

STARK 検証の実行

成功した検証は、レシートの証明が有効で、その内部のジャーナルが期待するゲストの実行結果に結びつくことを確認します。ゲストが全票を受け取ったか、表示値がジャーナルと一致するかは、ジャーナルの内容を使ってアプリが別途確認します。

検証済みレシートから出力を取り出す

配布された journal.json をレシートと照合するには、レシート内部から同じ出力を取り出す必要があります。decode-journal は、一度読み込んだレシートを検証し、成功したその同じレシートのジャーナルを現在の Rust 契約でデコードします。

./verifier-service/target/release/verifier-service decode-journal \
  --bundle /path/to/bundle.zip \
  --image-id "$EXPECTED_IMAGE_ID" \
  --output /tmp/receipt-journal.json \
  --quiet

期待 Image ID は、マッピングとビルド由来を確認して設定します。このコマンドは開発用レシート、検証失敗、Image ID 欠落、現行でない methodVersion を拒否します。

出力はホストと同じ camelCase JSON で、検証済みの imageId を含みます。UUID とハッシュはバイト配列なので、公開 journal.json の UUID・16 進数文字列とは表現が異なります。ローカル検証手順では、この表現をそろえて値を比較します。receipt の固定バイトオフセットを読む手順ではありません。

検証レポート

verify は、検証が完了した試行について JSON レポートを出します。呼び出し側は終了コードとレポートの両方を確認します。

終了コード1でも、レポートが生成されている場合があります。例えば、標準出力へレポートを出した後に --output のファイル書き込みが失敗する場合です。レポートがあるだけでは正常終了と扱えません。--quiet は標準出力を抑えるので、レポートを残すには --output を併用します。

success では errors を持たず、dev_mode_receipt=false、二つの Image ID が一致します。dev_mode では dev_mode_receipt=true で、レシートの ID が存在すれば期待値と一致します。failed は一つ以上の非空の診断文字列を持ちます。errors の各文字列は固定エラーコードではありません。

アプリがレポートを受け取る境界

Node.js アダプターは --output に指定したファイルを最大 1 MiB まで読みます。標準出力を検証結果の根拠にはしません。フィールド形式、Image ID、時刻、数値の範囲、ファイル名、status 間の条件を検査したうえで、終了コードとの組が 0/success、2/dev_mode、3/failed のいずれかであることを要求します。

さらに、呼び出し時の期待 Image ID とバンドル名に対応するレポートかを確認します。不在、不正、組の不一致は拒否します。API の verifierResult.report へ投影するときは二つのパスフィールドを除きます。

デプロイメントモデル

アプリからの検証要求は、セッションと集計 ID で対象を指定します。クライアントが任意のローカルパス、S3 キー、receipt 本文を指定する API ではありません。サーバーが、その集計結果に保存したバンドルの所在を解決します。

AWS の集計完了コールバックは結果の復元・保存を行います。その時点で STARK 検証を自動完了するわけではありません。POST /api/sessions/:sessionId/finalizations/:finalizationId/verification で検証を要求すると、API は running を保存し、キューへ作業を送って返ります。

worker は S3 のバンドルを取得・検査し、CLI を実行してレポートを保存します。終了した検証結果は、セッションと集計 ID に対応する独立した保存レコードへ書きます。ブラウザは検証リソースを繰り返し取得して完了を知ります。

再試行と終端状態

S3 取得、バンドル検査、プロセス起動、成果物アップロード、結果の記録などの基盤処理で失敗した場合は SQS で再試行し、3 回目の受信でも失敗すれば終端の failed と内部の失敗分類の保存を試みます。暗号学的な不一致で CLI が返した failed とは区別します。

レポートやその所在が残るかは、失敗した段階によって異なります。CLI の実行前なら、その試行のレポートはまだありません。アップロード時の失敗なら生成済みでも配送情報は記録されず、検証結果の記録時の失敗なら、S3 のレポートと配送情報がすでに保存されている場合があります。ファイルの存在だけで検証作業の成功を判断しません。

検証 POST を再送しても、success、failed、dev_mode は再検証せず同じ終端結果を返します。running も実行中として返しますが、AWS でキュー送信の記録がなければ同じ集計の作業を再発行して補修します。未設定または not_run なら新たな実行へ進みます。

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

ブラウザはこの検証サービスの結果をサーバー経由で受け取るため、その報告を信頼します。自分で再検証する場合に必要な材料は 手元での検証、画面の他の確認との関係は 検証の実行フローに示します。

公開 ZIP には、検証レポートの代わりにレシート自体を含めます。受け取った人が同じ暗号学的検証を実行できるようにするためです。全レポート verification.json は、別の認証付き API で取得します。

証拠をつないで結果を判定する

ここまでの証拠を集めたら、投票結果としてどんな表示を返せるでしょうか。掲示板の記録も公開入力も揃っていて、得票数に食い違いが見つからなくても、STARK の検証がまだ実行中なら結論は待つ必要があります。

証拠を取得できなかった場合と、取得した証拠が矛盾する場合も、意味が違います。前者は確認できていない状態、後者は不一致を見つけた状態です。どちらも Verified にはできませんが、利用者が次に確認すべきものは異なります。

検証画面は、各チェックの結果と実行状態を合わせて、成功、失敗、待機、証拠不足、制限付きなどを表示します。ブラウザ自身が行う投票時の照合と、サーバーが報告する掲示板・集計・STARK の確認を区別しながら、一つの結果にまとめます。

まず四つの問いと証拠を実際のチェックに対応させ、その後で実行場所と表示条件を確認します。

4 段階検証モデル

投票の記録、掲示板、集計、計算の証明は、それぞれ違う疑問に答えます。検証画面の四つの段階は、その違いを表しています。

Stage 1: Cast-as-Intended

最初の問いは「B を選んだ自分の操作と、サーバーが受け付けた記録が一致するか」です。

ブラウザは、保存しておいた選挙 ID、選択肢 B、32 バイトの乱数から コミットメントを再計算します。それがサーバーから取得した投票レシートの値と一致すれば、手元の投票内容と受理記録を結びつけられます。選択肢の範囲、乱数の形式、レシートの存在も確認します。

この確認では、投票した端末に残る情報が必要です。localStorage を消した場合や別の端末で開いた場合、サーバーの集計結果が正常でも、投票時の意図との照合はできません。また、手元のブラウザや保存データ自体が正しく動作することは前提です。

Stage 2: Recorded-as-Cast

レシートの値が正しくても、その記録が集計まで掲示板に残っているとは限りません。そこで二つの Merkle 証明をつなぎます。

包含証明は、自分のコミットメントが投票時のツリーにあることを確かめます。インデックス 0 の票なら、その時点のツリーサイズは 1 です。証明から計算したルートを、レシートに残る投票時のルートと照合します。

整合性証明は、投票時のツリーが、集計時の 64 スロットのツリーの先頭部分として残っていることを確かめます。二つの時点を比較し、その間に既存の記録が差し替えられず、追記だけが行われたかを検証します。CT Merkle ツリーには、この二つの証明の計算規則を示しています。

ただし、自分に示された二つのツリーが整合していても、別の人にも同じツリーが示されたとは限りません。設定された STH ソースがある場合は、集計時のツリー状態を他の応答と照合します。この確認は STH のダイジェストなどの一致を見るもので、電子署名の検証ではありません。同じサーバーの応答同士を照合しても、独立した観測者による裏付けにはなりません。独立性と照合条件は STH ダイジェストで説明します。

Stage 3: Counted-as-Recorded

記録が掲示板に残っていても、サーバーがそれを集計プログラムへ渡すとは限りません。ゲストは掲示板の全スロットを基準に、受け取った票と計上した票を数えます。

たとえば、インデックス 0 を渡さず、残り 63 票だけを正しく集計すると、ジャーナルには「未提示 1、除外 1」が残ります。得票数の計算が正しくても、掲示板全体の集計としては失敗です。さらに ビットマップ証明を使うと、その除外に自分の票が含まれるかを確かめられます。全体の除外数と自票の状態を併用することで、「自票は数えられたが、他の票が欠けた」という場合も検出できます。

集計値の比較もこの段階の役目です。画面に出す A〜E の得票数を、ジャーナルの verifiedTally と候補ごとに照合します。B から一票減らして別の候補へ加える操作は、総数が 64 のままでも検出できます。

そのほかに、公開入力の形式、インデックスとコミットメントの重複、想定票数とツリーサイズ、選挙設定、締切時の掲示板状態を確認します。入力コミットメントを再計算して、公開された入力側の記録とゲストが使った入力を結びつけます。入力コミットメントに含まれないフィールドは、対応する選挙マニフェストや締切ステートメントとの照合で確認します。

Stage 4: STARK Verification

ここまで何度も使ったジャーナルについて、最後に必要なのが「指定した集計プログラムが、実際にこの出力を計算した」という裏付けです。

Rust の検証サービスが、期待する Image ID を指定して STARK レシートを検証します。成功したレシートに結びつくジャーナルを使うことで、集計値、除外数、入力コミットメント、ビットマップルートをゲストの計算結果として扱えます。

この成功は、ゲストへ渡された入力に対する計算の正しさを示します。入力が掲示板全体を表すか、手元の票と一致するか、表示された得票数が同じかは、前の三段階との照合で確かめます。開発モードのフェイクレシートには、本番用 STARK 証明としての裏付けがありません。

四段階をどう最終表示へまとめるかは、Verified の表示条件で定めています。ここまでの順序は証拠の関係を説明する順序です。実際の画面は STARK の完了を待ってから各段階を順に表示します。

検証の実行フロー

「検証へ進む」を押すと、ブラウザとサーバーがそれぞれの持つ証拠を使って確認を始めます。ブラウザには投票時の B と乱数が残り、サーバーには掲示板の証拠、集計入力、STARK レシートが保存されています。

誰が何を検証するか

API の検証応答には全 22 チェックが並びますが、Cast の 4 チェックは not_run です。サーバーだけでは投票者の手元の意図を検証できないためです。ブラウザはこの 4 件をローカルで再計算した結果に置き換え、共通の表示判定規則を適用します。

この画面の Recorded / Counted と STARK の結果は、サーバーが行った検証の報告を利用します。ブラウザがすべての暗号検証を独立に実行するわけではありません。サーバーの報告から独立してレシートや公開入力を調べる場合は、手元での検証を行います。その場合も、ZIP だけでは手元の投票意図や自票の証拠まで揃いません。

画面で進む処理

結果画面は、集計結果をその finalizationId とともに保存します。「検証へ進む」を押すと開始時刻を記録し、必要なら STARK 検証を先に起動して、完了を待たずに検証画面へ移ります。

sequenceDiagram
  participant B as ブラウザ
  participant A as API
  participant R as Rust 検証サービス
  B->>A: この集計の STARK 検証を開始
  Note over B: 結果画面から検証画面へ移る
  A->>R: レシートと期待 Image ID を渡す
  R-->>A: 検証結果を保存
  loop STARK の完了を待つ
    B->>A: 同じ集計の検証状態を取得
    A-->>B: 状態とチェック結果
  end
  B->>B: Cast を手元で再計算し、各段階を表示
  B->>B: 共通の規則で最終表示を決定

検証の開始には POST /api/sessions/:sessionId/finalizations/:finalizationId/verification、状態の取得には同じパスの GET を使います。AWS では POST がキューへ仕事を渡し、ワーカーが検証サービスを動かします。ローカルでは、選択されたローカル保存先のバンドルを直接検証します。

検証画面は、開始時刻と集計結果が保存された継続状態から処理を引き継ぎます。必要ならそこで STARK 検証を起動します。継続状態がなく、STARK も not_run のまま検証画面へ直接アクセスした場合は、自動開始しません。

STARK が終了してから段階表示を始めるので、画面上の順番と実際の処理順は一致しません。ポーリングのタイムアウトや通信失敗は成功として処理せず、検証実行の失敗として表示します。

証拠がない場合と、壊れている場合

投票時の証拠を取得できない場合、何も矛盾が見つからなかったとしても、記録を確認できたとは言えません。逆に、取得した証拠のインデックスやコミットメントが保存済みの票と食い違う場合は、単なる不足ではありません。

検証リソースの内部では、この違いを次のように扱います。

読み取り準備が返すリソース全体の unavailable / corrupt と、正常な応答内の voterEvidence.availability は別の状態です。現在の GET は、前者をエラー応答の検査へ通すため 500 になります。正確な wire 形式は API エンドポイントに示します。

取得した JSON は、チェック評価の前に形式と相互整合性を検査します。期待と違うジャーナルや部分的な証跡を、空値や成功値へ補正しません。一方、教育用シナリオの「表示集計だけが違う」という状態は、その差を失敗の証拠として保持します。証拠の内容を変えて辻褄を合わせることはありません。

判定後に記録する観測

最終表示が確定し、保留中のチェックがなく、サーバー応答と STARK の終了状態を確認できた後、ブラウザは Cast の 4 チェックの状態だけを観測 API へ送ります。選択肢、乱数、レシート、最終判定そのものは送りません。サーバーは残りの証拠から観測内容を組み立てます。

この送信は運用上の集計に使います。失敗しても、すでに確定した検証結果は変わりません。同じ集計についての再送と競合の扱いは、観測 APIに定めています。

Verified の表示条件

全 64 票について正しい計算の証明があり、表示された得票数も同じだったとしても、投票時の手元データを失っていれば「自分が選んだ B と一致するか」は確認できません。反対に、自票が正しく数えられていても、別の一票が除外されていれば、集計全体の検証は失敗です。

Verified は、必要な確認がすべて終わり、その結果が矛盾なく揃ったときだけ表示します。 STARK レシートの検証成功は、その条件の一つです。

最終判定の種類

「不明」と「不正を検出した」は分けます。どちらも緑にはなりませんが、Warning を改ざんの証明として説明することもありません。

必須確認と補助確認

チェック一覧の required は必須確認です。既知の必須チェックが一件でも欠けている、not_run、pending、running、failed のいずれかなら、Verified にはなりません。

optional は補助確認です。失敗や未実行だけで必須確認の失敗にはしませんが、verified_with_limitations として Warning を表示します。たとえば STH ソースが未設定なら、そのチェックは未実行の補助確認になります。STH ソースを設定した場合は必須へ昇格し、取得・照合に成功することが必要です。補助確認でも pending / running が残る間は、最終ラベルの表示を待ちます。

チェックが空、または未知のチェックしかない場合は、集約結果を作れません。既知チェックと未知チェックが混在する場合も、その未知部分を成功と解釈せず、失敗や進行中の判定がなければ証拠不足とします。API から受け取る正式なリソースでは、そもそも定義外・重複・不正なチェック構成を拒否します。

ステータスの判定順序

まず、チェック結果を集約して「どの理由を伝えるか」を決めます。次に、その集約結果だけでなく証拠と表示準備も調べ、「そのラベルを表示してよいか」を決めます。集約値の summary が fully_verified でも、後者の条件を満たさなければ Verified は表示しません。

複数の状態が同時に現れたとき、集約は次の順で理由を選びます。

画面へ表示する条件

API とブラウザは共通の deriveVerificationPresentationPolicy を使います。ブラウザは Cast を手元で再計算したあと、この規則を適用します。

最終ラベルは、検証開始済み、段階表示の完了、全チェックの pending / running の解消を待って表示します。表示内容は、明示的な実行失敗、証拠から分かる重大な失敗、上表の集約結果、進行中の警告の順に選びます。タイムアウトや検証シーケンスの失敗も、明示的な実行失敗です。

票の除外は、集約結果だけに頼らず確認します。missingSlots、invalidPresentedSlots、excludedSlots のいずれかが正数、不正な数値、または三値の関係が矛盾する場合は、重大な失敗とします。整合性証明、完全性、期待票数、選挙マニフェスト、締切ステートメント、STARK レシートの失敗と、設定済み STH の失敗もこの経路で確認します。Image ID とレシートの失敗は、明示的な証明失敗としても扱います。

したがって summary = fully_verified という値だけを書き換えても、Verified を許可しません。四段階がすべて成功し、開発用の証拠がなく、失敗信号もなく、表示準備が完了している必要があります。

公開 API 応答の整合性

API 応答の成功フラグも検査対象です。チェック定義と状態、段階の状態、投票者の証拠、レポート、付属ジャーナル、改ざん情報が互いに矛盾しないことを確認し、同じ規則で表示資格を再計算します。

Verified を主張するリソースには、特に次の事実を要求します。

• シナリオは S0、STARK は本番用の success、改ざん検出はなく、改ざん数はゼロ。
• 投票者の証拠が利用でき、票の ID、コミットメント、投票時の位置とツリーサイズが集計側の値と整合する。
• missingSlots = invalidPresentedSlots = rejectedRecords = excludedSlots = 0。
• seenIndicesCount = treeSize = totalExpected で、seen / included のビットマップルートが一致する。
• 表示集計と検証済み集計が候補ごとに一致し、その合計も totalExpected と一致する。
• 必須チェック、四段階、表示資格と準備状態が整合する。

レポートがある場合は、その状態と期待 Image ID・レシートの Image ID も照合します。STARK の success という状態だけでは、Image ID の確認成功は満たせません。

rejectedRecords は「何スロットが除外されたか」を数える値とは異なりますが、上記の成功条件ではゼロを要求します。ゲストのスロットとレコードの区別を、成功条件からこの値を外してよい理由にはしません。

STARK 検証のゲーティング

STARK の検証状態に応じて、ジャーナルを使うチェックを待機させます。これを実装では zkGate と呼びます。

公開入力の形式と二つの重複確認は、STARK の完了前にも評価できます。また、すでに除外や異常なカウントが見えている場合、その失敗は待機状態で隠しません。対象のチェック ID と例外は チェック一覧にまとめています。

開発用の dev_mode は、core evaluator で明示的に許可された場合に success、それ以外は not_run に正規化して扱います。現在の GET の表示用組み立てでは、許可されない開発モードは failed として扱います。許可した場合も証拠には開発用であることが残り、最終表示は Verified にはなりません。

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

四つのステップは、それぞれに属する必須チェックから状態を導きます。Cast は 4 件、Counted は 10 件、STARK は 2 件です。Recorded は包含・位置・整合性の 3 件が基本で、STH ソースの設定時は STH も加わります。包含と整合性から派生する二つの補助チェックは、単独でステップの状態を決めません。

集約の優先順は failed、running、pending、全件成功の success、それ以外の not_run です。表示上の入力ハイライトは、必須に限らず、その段階の全チェック定義から導きます。

サーバーのステップ構築には追加条件があります。Counted はジャーナルがない場合、必須失敗がなければ not_run にします。Recorded は投票時の証明の treeSize がなければ not_run にします。Cast はサーバー応答では not_run とし、ブラウザがローカル結果を反映します。

不変条件のまとめ

Verified に必要なのは、完全な必須チェック集合、その成功、除外のない整合した集計、本番用の証明、そして表示準備の完了です。不足、不正形式、未知のデータ、開発用の証拠を、成功の代わりに使うことはできません。

この表示規則は テストと Lean のモデル・実装対応確認で継続して検査しています。改ざんシナリオでは、何を変えるとこの条件を満たさなくなるかを実際の証拠で示します。

改ざんして、検出を確かめる

自分の一票を集計から外す操作と、集計後の得票数を書き換える操作では、壊れるつながりが違います。前者では掲示板と集計入力、後者では計算結果と表示が食い違います。

このデモでは、その違いを確かめるために集計時のシナリオを選べます。S0 は変更を加えない基準です。S1・S3・S5 は一票を集計入力から外し、S2・S4 は画面へ出す得票数だけを変えます。

どちらの改ざんでも、STARK レシート自体は正常に検証できる場合があります。前者では「63 票を受け取り、一票の未提示を記録した計算」が正しく実行され、後者では「元の 64 票の正しい集計」がそのまま証明されるためです。検証画面は、この証明に結びついた結果を掲示板や表示値と比較して、集計全体の失敗を見つけます。

各シナリオでは、B を選んだインデックス 0 の一票と、63 票のボット票について、何を変え、どの証拠に差が出るかを追います。

シナリオごとに何が食い違うか

B を選んだユーザー票はインデックス 0、ボット票は残り 63 票です。集計画面で選ぶシナリオは一回につき一つで、掲示板の 64 スロットはそのまま残します。操作するのは、ゲストへ渡す票か、画面へ出す得票数です。

シナリオ一覧表

S0: 正常（改ざんなし）

元の 64 票をゲストへ渡します。各票が有効なら全スロットが計上され、excludedSlots = 0、表示集計と verifiedTally は一致します。ユーザー票の included ビットも 1 になります。

これは他のシナリオと比べる基準です。S0 を選んだこと自体は検証成功の根拠になりません。手元の証拠、掲示板の証明、STARK なども成功し、補助チェックにも制限がない場合に Verified を表示します。

S1: ユーザー票の除外

インデックス 0 の票を集計用の入力から外し、63 票をゲストへ渡します。掲示板には元のコミットメントが残っているので、投票時の包含証明や追記の整合性証明は成功できます。

しかしゲストは、掲示板のサイズが 64 なのに一つのスロットを受け取っていないと数えます。残りの票が有効なら、ジャーナルは次の値になります。

missingSlots = 1
invalidPresentedSlots = 0
excludedSlots = 1

これにより counted_missing_indices_zero が失敗します。自票のビットマップ証明を取得できれば、index 0 の seen と included がともに 0 であることも確認でき、counted_my_vote_included は失敗します。「入力には来たが無効だった」ではなく、「ゲストへ提示されなかった」と説明できます。

表示集計も 63 票の入力を基にするため、表示と verifiedTally は一致します。STARK 検証も成功できますが、全 64 スロットの完全性を満たさないため、全体は Verification Failed です。自票の証明が不足していても、全体の一票除外という事実は消えません。

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

ゲストには元の 64 票を渡します。表示側だけで B の得票数を一つ減らし、別の候補を一つ増やします。加算先は B 以外から選び、ユーザー票の振替先として表示する値とも一致させます。

flowchart TB
  V["元の 64 票"] --> P["ゲストの計算と証明"]
  P --> J["ジャーナルの得票数"]
  V --> T["表示用に B を −1<br/>別候補を ＋1"]
  J --> C{"候補ごとに一致するか"}
  T --> C
  C --> F["不一致を検出"]

合計はどちらも 64 なので、合計だけでは検出できません。候補ごとに比較する counted_tally_consistent が失敗します。入力やジャーナルは変えていないため、入力コミットメント、自票の包含、STARK は通常成功します。必要な他の証拠が揃えば、最終理由は published_tally_mismatch です。

この場合、ZIP に収める計算の証拠は正常です。表示集計は ZIP に入っていないため、ZIP のローカル検証だけで S2 の表示改変まで再現検出できるとは限りません。表示された値との比較が必要です。

S3: ボット票の除外

現在の実装はインデックス 1 のボット票を入力から外し、63 票を渡します。残りの票が有効なら、S1 と同じく missingSlots = 1、invalidPresentedSlots = 0、excludedSlots = 1 です。

counted_missing_indices_zero は失敗しますが、ユーザー票の index 0 は計上されるので、自票のビットマップ確認は成功できます。このとき最終理由は votes_excluded です。自分の票が数えられたことと、全体の票が欠けていないことを別々に確認する必要性が分かります。

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

ボット票を一つランダムに選び、その元候補の得票数を表示側だけで一つ減らし、別の候補へ一つ加えます。ゲストに渡す入力は元の 64 票です。

S2 と同様に counted_tally_consistent が表示とジャーナルの差を検出します。入力コミットメント、STARK、ユーザー票の包含は通常成功できます。必要な他の証拠が揃えば、全体の失敗理由は published_tally_mismatch です。

S5: ランダムな票の除外

64 票の中からランダムに一票を選んで、集計入力から外します。残りの票のインデックスは詰め直さず、掲示板上の位置を保ちます。候補を書き換える操作はしません。

missingSlots = 1 と excludedSlots = 1 により、counted_missing_indices_zero が失敗します。選ばれたのがユーザー票なら、自票の証明でも未計上を示せます。ボット票なら自票は含まれたままです。どちらの場合も、全体の完全性の確認で検出できます。

表示集計は除外後の 63 票を基にするので、ジャーナルと一致します。counted_tally_consistent の成功は、この一票除外を見落とした結果ではなく、比較する対象が異なるためです。

改ざんを反映する場所

実装では S1 / S3 / S5 を tamperMode = input、S2 / S4 を tamperMode = claim、S0 を none として扱います。入力改変の場合だけ、変更後の票集合をゲストへ渡します。表示改変の場合は元の票を渡し、変更後の得票数を表示用に保存します。

同期・非同期のどちらでも、ゲストが返したジャーナルの集計値や除外数を、シナリオ説明に合わせて上書きしません。ignoredCount、recountedCount、claimedCounts は表示用の情報です。S5 の変更記録は IGNORED、ignoredCount = 1、recountedCount = 0 です。

API は、シナリオ、除外数、改ざん数、対象ボット、得票差の説明も相互に検査します。S0 / S1 / S3 / S5 は表示と検証済み集計の一致を要求し、S2 / S4 は一候補 −1、別候補 ＋1 という差を要求します。説明と証拠が矛盾する応答を、シナリオの正常な結果として受理することはありません。

実行モードと検証の前提

上の結果は、実 API での処理について、残りの証拠が有効で STARK 検証が成功した場合を説明しています。実行場所は runtime profile が選ぶ同期・非同期の構成に従います。

ブラウザ mock の固定応答は、実 API と異なるチェック結果を返すことがあります。local-demo と static-mock-e2e は本番用 STARK 証明を生成せず、local-proof-development のフェイクレシートも本番用の暗号的裏付けにはなりません。証明未完了や証拠不足が加わる場合の状態は、チェック結果の対応表で区別しています。

シナリオとチェック結果の対応

各シナリオで生じる差を、検証結果の ID と照合するための表です。実 API の検査を通過した証拠が揃い、STARK が成功した時点を示します。

主要チェックの対応（STARK 解決後のサーバー評価）

API の Cast 4 件は常にブラウザの再計算待ちです。手元の証拠が有効なら、ブラウザが再計算した後の Cast は成功します。表の「未実行」はシナリオによる失敗ではありません。

自票のビットマップ証明が不足すると、counted_my_vote_included は失敗の代わりに not_run となる場合があります。S5 で対象がユーザー票なら自票チェックも失敗し、ボット票なら通常成功します。

4 段階と最終理由

Recorded が成功できるのは、各シナリオが掲示板の既存エントリを削除しないためです。STARK が成功できる理由と、S2 / S4 の ZIP だけでは表示改変を検出できない理由は、シナリオ本文で説明しています。

S0 でも、STH 未設定など補助チェックが未実行なら verified_with_limitations です。一票除外が分かっていて自票の状態が確認できなければ、votes_excluded_unknown とします。除外が見つからず必須証拠が足りない場合は missing_evidence です。

証明の完了を待つ間

STARK が not_run / running の間、依存する Counted チェックは通常 not_run / pending です。公開入力の形式・重複は先に確認でき、正の除外数や異常なカウントも先に失敗を示せます。STARK 自体が失敗すると、それに依存するチェックも失敗になります。正確な対象 ID は STARK 結果への依存に示します。

これらは集約前のチェック結果です。最終表示には、ブラウザでの Cast、証拠不足、開発用レシート、表示準備の状態も反映します。Verified の表示条件に従い、サーバーの STARK success だけから成功ラベルを出すことはありません。

証拠を持ち帰って確かめる

画面に表示された「証明の検証に成功した」という報告を、自分の環境でも確認できます。検証画面から取得する bundle.zip には、STARK レシートと、その計算に対応する公開入力・出力が入っています。

確かめるときに大切なのは、ファイルを一つずつ読むだけで終わらないことです。正しい証明に、別の集計の journal.json や公開入力を添えても、その一組の証拠が正しいことにはなりません。

flowchart TB
  I["手元で選んだ期待 Image ID"] --> R["STARK レシートを検証"]
  R --> J["証明内の出力と journal.json を比較"]
  J --> P["公開入力・選挙設定と照合"]

ZIP で確かめられること

監査では、期待したプログラムの production STARK 証明が検証できること、証明内の出力が journal.json と一致すること、公開入力と選挙設定・締切時の掲示板がその出力に結び付くことを順に確認します。投票位置の欠落や不採用がないことと、得票数の合計も調べます。

期待する Image ID は、検証したいリリースに対応するソースの public/imageId-mapping.json から選びます。受け取ったレシートに書かれた ID をそのまま期待値にすると、別のプログラムの証明を受け入れてしまうためです。

画面の結果との違い

S2 は、証明に使う入力を変えず、画面へ渡す集計表示を変えます。そのため ZIP 内の証拠が整合していても、画面の表示と一致するとは限りません。表示用の presentation.tally は検証 API が返し、ZIP には入りません。

同様に、投票時にブラウザへ残した選択・乱数、投票レシートと投票時ルートの照合状態、自票のビットマップ証明、第三者の掲示板との照合結果も ZIP だけでは揃いません。手元の監査の成功は、画面の四段階すべてを再実行したという意味にはなりません。

実際の準備とコマンドは 手元で証拠を検証する にまとめています。ZIP のファイル形式を確認したい場合は バンドル構造 を参照できます。

公開できる証拠と、手元に残す情報

選択肢と乱数を公開すれば、第三者は一票ずつ集計をやり直せます。しかし、それでは誰かのコミットメントがどの候補への票かも分かってしまいます。そこで bundle.zip には、投票内容を開かずに計算や入力のつながりを確認するための証拠を収めます。

公開入力には、ゲストに渡した票のインデックス、コミットメント、Merkle パスが含まれます。個々の記録を公開監査に使う設計ですが、選択肢と乱数は収めません。なお、このデモではサーバーが投票時に選択肢と乱数を受け取ります。公開アーカイブから秘密を除くことと、運営者から秘密を隠すことは別です。

公開可能と、誰でもダウンロード可能の違い

本書の「公開可能」や public は、第三者へ渡せる内容であるというデータの分類です。無認証のダウンロードを意味しません。

ブラウザと CLI は、セッションへのアクセス権を示す capability を使って証拠を取得します。取得した bundle.zip を第三者へ渡し、その人が ローカルで検証することができます。レポートは別の保護対象で、ZIP と同じ公開範囲には含めません。

bundle.zip に入れないファイル

最初の四つは同期・非同期のどちらでも保護対象です。failure-marker.json は非同期実行時だけ生成され得る診断用ファイルで、レポートの取得 API からも配布しません。

ビットマップのファイル全体は ZIP に含めず、画面は自票の位置について証明を取得します。ただし、その証明には自票を含む 32 バイトの区画が入ります。このデモの全 64 位置は同じ区画に収まるため、他の位置の採用・提示状況も読み取れます。通常の API は証明の対象インデックスをそのセッションのユーザー票に限定しますが、区画内の他のビットを隠すものではありません。完全なビットマップや投票時の手元データが ZIP にないため、ZIP 単体では検証画面の最終判定を完全には再現できません。

許可したファイルだけを収める

新しい内部ファイルが増えたとき、それが自動的に ZIP へ入ると、秘密の公開につながります。そのため、アーカイブの構成は一つのマニフェストで明示します。登録されていないファイルは、既定で非公開です。同期・非同期それぞれの正確なメンバーは バンドル構造に示します。

生成処理はファイル一覧を選ぶだけでなく、完成した ZIP を検査します。必須ファイルの欠落、保護対象・未知のファイル、同名重複、大文字小文字だけが違う衝突、絶対パス、親ディレクトリへの移動、正規の名前でないエントリを拒否します。同期・非同期の公開前にこの規則を適用し、ローカル配信時にもアーカイブ全体を再検査します。

S3 配信では、公開前に検査済みのオブジェクトを読み出します。配信時に ZIP を再解析する代わりに、HEAD で固定した同一オブジェクト表現に結びつけて全体または範囲のバイト列を返します。

bundle と report の取得経路

どちらもセッション capability と、現在成功済みの集計に一致する finalizationId が必要です。API が権限と対象を確認してから、選択されたローカル保存先または S3 を読みます。利用者への通常配信には、生の S3 URL や署名付き URL を使いません。

大きい ZIP は同じ API のバイト範囲取得でダウンロードします。保存先に対象がない場合は別の保存方式を探しに行かず、取得失敗として返します。HTTP の範囲取得とエラーの契約は API エンドポイントに示します。

バンドル構造

bundle.zip を開くと、集計結果だけでなく、何を集計したかを照合するための JSON が並びます。中心になるのは、入力側の記録、計算の出力、それを裏付けるレシートです。

flowchart TB
  P["public-input.json<br/>公開できる入力の記録"] --> C["入力コミットメントを再計算"]
  C --> J["journal.json<br/>集計結果と照合用の値"]
  R["receipt.json<br/>計算の証明"] --> J
  E["election-manifest.json<br/>選挙設定"] --> J
  S["close-statement.json<br/>締切時の掲示板状態"] --> J

図の矢印は照合関係です。JSON が互いに一致することに加えて、期待する Image ID に対するレシートの検証と、レシート内のジャーナルとの一致が必要です。

アーカイブのメンバー

同期 ZIP は必須 6 ファイルと任意 2 ファイル、非同期 ZIP は必須 5 ファイルだけを認めます。任意の二つは、現在の通常フローでは生成されません。構成を決める正本は public-bundle-manifest.json です。許可外ファイルや危険なパスを拒否する規則と、秘密入力を収めない理由は 公開境界に定めています。

receipt.json の存在や、その image_id の自己申告だけでは、計算の正しさは確かめられません。また、開発用のレシートも同じファイル名を使えるため、ファイル名から本番用 STARK 証明だとは判断しません。

公開入力の構造

public-input.json は、入力コミットメントの再計算と、選挙設定・締切状態との照合に使います。秘密入力を丸ごと写したファイルではありません。

inputCommitment はこの JSON 全体のハッシュではありません。入力コミットメントで定めるフィールドとバイト表現から再計算します。それ以外の項目は、対応するマニフェストや締切ステートメント、ジャーナルと別途照合します。

journal.json は、ゲスト出力を UUID・hex・camelCase のフィールドへ変換した公開表現です。レシート内部のジャーナルは RISC Zero のシリアライズ形式を使うため、JSON の文字列をそのままハッシュして照合することはできません。ゲストプログラムに論理フィールドと表現の関係を示しています。

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

ローカルの同期生成では、TypeScript の処理がホストの出力から公開 JSON を構築し、選挙設定・締切状態・入力コミットメント・ジャーナルの整合を確認して ZIP を作ります。保存先はセッションと集計ごとのローカルディレクトリです。

AWS の非同期生成では、Fargate コンテナが入力を S3 から取得し、ホストを実行します。その後 Rust の prover-artifacts が秘密入力とホスト出力を検査して公開 JSON を構築し、生成済みの JSON を読み直して正準ハッシュと相互整合性を確認します。シェルは検査済みのファイルから ZIP を作り、完成後の構成検査を経て S3 へアップロードします。

コールバックは ZIP からジャーナル、レシート、公開入力、マニフェスト、締切ステートメントを復元し、利用可能なビットマップの隣接オブジェクトも検査して保存します。ジャーナルのカウントをシナリオ表示に合わせて変更することはありません。検証レポートは、その後の STARK 検証を処理したワーカーが保存した場合に利用可能になります。

現在の Rust の変換処理は method version 14 の出力を要求します。異なる契約の出力を推測で読み替えません。非同期処理の完了・再試行の条件は 非同期プローバーに示します。

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

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

保存ディレクトリには ZIP の外に保護対象のファイルもあります。次の配置は、すべてを一緒に配布してよいという意味ではありません。

{VERIFIER_WORK_DIR}/{sessionId}/{finalizationId}/
  input.json
  public-input.json
  election-manifest.json
  close-statement.json
  journal.json
  receipt.json
  metadata.json
  included-bitmap.json
  seen-bitmap.json
  verification.json
  bundle.zip

ビットマップのファイルは計上・提示の保存証拠、verification.json は検証サービス実行後のレポートです。ZIP の内容は、冒頭のメンバー表だけで決まります。

非同期モード（S3）

s3://{BUCKET}/sessions/{sessionId}/{finalizationId}/
  input.json
  {inputBase}-receipt.json
  {inputBase}-output.json
  {inputBase}-journal.json
  public-input.json
  election-manifest.json
  close-statement.json
  included-bitmap.json
  seen-bitmap.json
  bundle.zip
  verification.json
  failure-marker.json

inputBase はコンテナの一時入力名に由来します。ホストの生出力名と、ZIP 内の固定名 receipt.json / journal.json は異なります。{inputBase}-journal.json はホストが生成した場合だけ存在します。

この配置図には異なる時点の任意ファイルも含みます。レポートは後続の検証後に保存される場合があり、failure-marker.json は非ゼロ終了時にだけ最善努力で保存する内部診断です。成功した ZIP と失敗診断が必ず同時にできることを示してはいません。

アーカイブの再現性

同期 ZIP は、エントリ時刻をゼロに固定し、ファイル名順で追加します。同じ内容から作ったアーカイブの再現性を保つためです。非同期のシェルは zip -r を使い、同じ時刻固定の実装ではありません。内容の検証と、ZIP ファイル全体のバイト一致は分けて確認します。

実際に取得した ZIP を安全に展開し、レシートと各 JSON を照合する操作は、ZIP のローカル検証に続きます。

手元で証拠を検証する（Ubuntu）

検証画面で取得した bundle.zip を、対応する公開ソースと照合します。長い検査処理はリポジトリの scripts/docs/audit-bundle.sh にまとめてあります。このスクリプトは、アプリと同じ ZIP 読み取り・データ検査・入力コミットメント計算を使い、STARK レシートの暗号検証には Rust の verifier-service を使います。

1. ソースとツールを用意する

検証したいリリースに対応する 公開ソース を取得し、そのルートで作業します。必要なのは Ubuntu 22.04 / 24.04、Node.js 24、Corepack、Rust と次のビルド用ツールです。

sudo apt update
sudo apt install -y build-essential pkg-config libssl-dev jq curl ca-certificates
corepack enable
pnpm install --frozen-lockfile

pnpm のバージョンはルートの package.json にある packageManager から Corepack が解決します。Rust がまだなければ導入します。

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

リポジトリ内では rust-toolchain.toml が指定する Rust を使います。Rust の導入後も、以降のコマンドはリポジトリのルートで実行してください。

2. production 用の検証サービスを作る

cargo build --manifest-path verifier-service/Cargo.toml --release --features production

production feature は RISC Zero の開発モードを無効にします。生成先は verifier-service/target/release/verifier-service です。すでに別用途でビルドしたバイナリがあっても、このコマンドで production 用にビルドしてから監査します。

3. ZIP を検査する

ダウンロードした ZIP のファイル名に置き換えて実行します。

bash scripts/docs/audit-bundle.sh "$HOME/Downloads/stark-ballot-verification-REPLACE.zip"

期待する Image ID は通常 variants.default を使います。対象リリースが x86_64 向けの別ビルドを使った場合は、明示的に選びます。

bash scripts/docs/audit-bundle.sh "$HOME/Downloads/stark-ballot-verification-REPLACE.zip" x86_64

これは手元の CPU を自動判定する指定ではなく、証明を生成したゲストビルドの選択です。public/imageId-mapping.json の該当値が未確定なら処理は止まり、他の値で代用しません。

スクリプトは毎回新しい一時ディレクトリに ZIP をコピーし、六つの検査を順に実行します。失敗した場合はそこで停止します。最後に表示する Audit files: の場所には、対象 ZIP、展開したファイル、生成できた検証レポートが残ります。

実行中に確かめていること

ZIP は同じメモリ上のバイト列を検査してから展開します。ZIP 読み取り側は各ファイルの展開後サイズを 64 MiB、合計を 512 MiB、エントリー数を 10,000、パスを 4,096 バイトに制限し、CRC も確認します。そのうえで、実際に許可するファイル名と数を公開バンドルの規則で絞ります。

レシート検証では、レポートに success と書かれているだけでは通しません。共通のレポート読み取り処理が形式と終了コードの組を検査します。開発用の 2/dev_mode、失敗の 3/failed、その他の不一致は監査の成功にしません。

さらに decode-journal で同じレシートを再検証し、RISC Zero の形式で格納された出力を読み出します。比較するのは選挙 ID・設定ハッシュ、掲示板ルートと STH、各票数、候補別集計、ビットマップルート、入力コミットメント、方式のバージョンです。receipt.json の隣にある JSON を読んだだけでは、証明の出力を確認したことにならないためです。

票数については、excludedSlots、missingSlots、invalidPresentedSlots がゼロであること、totalExpected = treeSize、totalVotes > 0、候補別の verifiedTally 合計が validVotes と等しいことを確認します。位置数とレコード数の違いは ゲストプログラム の定義に従います。

結果を読む

六つが通ると Bundle audit passed と表示します。これは「手元で検証した証明と、この ZIP の公開データが、上記の条件で整合した」という結果です。S1 の票の欠落は位置の検査で失敗します。一方、S2 のように画面へ渡す集計表示だけを変更した場合、ZIP の監査は通り得ます。画面に必要な追加の証拠 まで揃えて初めて、画面の最終判定と比較できます。

失敗した場合は、表示された検査番号とエラー、Audit files: にある対象データを確認します。期待値を受け取った ZIP の値に合わせたり、失敗した検査を省略したりして続行しないでください。再実行も同じコマンドで行えば、新しい監査ディレクトリが作られます。

AWS で証明生成を動かす

「集計する」を押してから STARK 証明ができるまで、ブラウザをサーバーにつなぎ続ける必要はありません。API は集計要求を保存して受付結果を返し、別の計算ジョブが証明を作ります。ブラウザは途中経過を取得し、できあがった証拠を使って検証へ進みます。

この時間の差が、AWS 構成を分ける出発点です。ページ配信と投票受付には短い応答が必要です。一方、証明生成には多くの CPU とメモリが必要で、同時に起動できる数も制限します。両方を同じ処理にすると、証明の待ち時間や再試行が利用者への応答を巻き込みます。

flowchart TB
  B["ブラウザ"] -->|集計要求| A["API：受付を保存"]
  A -->|作業を登録| Q["キュー"]
  Q --> P["別ジョブで証明生成"]
  P --> R["結果と証拠を保存"]
  B -->|進捗を取得| R

処理を分けると、今度は「同じ作業が届いた」「待っている間に取り消された」「証明はできたが結果の保存に失敗した」という問題が生まれます。非同期プローバーは、作業の識別子と保存済みの状態を照合し、古い作業が現在の結果を書き換えないようにします。

さらに、実行するコンテナと変更手順にも根拠が必要です。承認したイメージを内容のダイジェストで固定し、起動前に署名を確かめます。インフラの変更は保存した Terraform 計画を承認して適用し、適用後の確認結果を受入記録に結び付けます。ログと監視は、これらの処理のどこで止まったかを調べるために使います。

本番環境の stark-prod/main は、Cloudflare と CloudFront を経由して公開デモを提供します。開発環境の stark-dev/develop は、運用者向けの署名付き Cookie で入口を制限します。ブラウザから AWS へ入るでは、この入口とセッションの操作権限を説明します。

次の構成図は、通常稼働時の入口、証明生成、検証と保存先をまとめたものです。本番と開発は別々の資源を持ち、図の入口部分に環境ごとの違いを示しています。図を選ぶと拡大して確認できます。

AWS で証明生成が完了しただけでは「Verified」にはなりません。表示には、投票・掲示板・集計結果を含むすべての必須確認が必要です。

ブラウザから AWS へ入る

本番環境（main）では、利用者はページを開くときも投票するときも同じ公開ホスト名へ接続し、Cloudflare を経由して CloudFront へ入ります。CloudFront は静的ファイルを S3 から配信し、/api/* の要求を API Gateway へ転送します。S3 への読み取りは CloudFront の OAC（Origin Access Control）で許可し、バケットを直接公開しません。ブラウザは保存先のバケットや内部のワーカーを選びません。

flowchart TB
  B["ブラウザ"] --> F["Cloudflare"]
  F -->|本番の入口認証| C["CloudFront"]
  C -->|ページ・静的ファイル| S["非公開S3"]
  C -->|/api/*| G["API Gateway"]
  G --> A["public-api Lambda"]

拡張子のない画面URLは index.html へ解決し、その後の画面遷移を React Router が処理します。API Gateway の先では、Hono がルート定義に従ってハンドラーを呼び出します。外部向けのパスと応答形式は packages/api-contract/src/routes/inventory.ts が定義し、apps/api/src/server/api/routes/definitions.ts が実行環境へ接続します。

入口の許可と一票の許可

本番の経路には二つの認証があります。CloudFront は、ページ・静的ファイル・API のいずれでも、公開ホスト名と Cloudflare が付ける専用トークンを確認し、入口の迂回を拒否します。トークンはハッシュで照合し、転送前に取り除きます。さらに CloudFront は API へ専用の origin-verification header を付け、API はその値が欠落・不一致なら拒否します。API Gateway の直接URLも、この確認を通過しなければ利用できません。

利用者の IP も、この認証済み経路を前提に扱います。CloudFront は単一の CF-Connecting-IP があり、形式条件を満たすことを確認します。API は TRUSTED_PROXY=cloudflare でその値を有効な IPv4 / IPv6 アドレスとして検証し、欠落・不正な値を別の転送ヘッダーやプロキシの IP で補いません。

main では公開セッションの作成時に、サーバーで Turnstile を検証します。token がない場合、検証に失敗した場合、用途やホスト名が一致しない場合は作成しません。

開発環境（develop）は Cloudflare を経由せず、CloudFront の署名付き Cookie で運用者向けに入口を制限します。対象はページ、静的ファイル、/api、/api/* です。CloudFront へ登録するのは公開鍵だけで、署名用の秘密鍵は KMS 内に残ります。この Cookie による制限は main にはありません。

どちらの環境でも、特定のセッションを操作する権限は別に確かめます。セッションに属する API は、URL の sessionId と X-Session-Capability を照合します。入口を通過しても、別の人のセッションを操作できるわけではありません。各ルートでは、必要な capability、Turnstile、レート制限、入力検証を定められた順序で適用します。

証拠のダウンロードにも同じセッション権限が必要です。「公開可能なバンドル」は再配布できる内容の分類であり、保存バケットを誰でも読めるという意味ではありません。ブラウザと CLI は capability で保護された API から取得し、S3 の直接URLや署名付きURLを通常の取得経路にしません。具体的な配布条件は公開境界に定義しています。

実行環境を一組で選ぶ

ローカルで画面を試すときに本物の証明生成を待つ必要はありません。ただし、模擬証拠を AWS の証明と取り違えないように、保存方式や証明方式を独立したフラグで混ぜず、実行プロファイルを一つ選びます。

サーバーは RUNTIME_PROFILE、ブラウザのビルドは VITE_RUNTIME_PROFILE を使います。サーバーはアダプターを作る前に選択を解決し、保存先、証明方式、集計方式、証拠配信、レート制限、Turnstile の設定を一組として検証・固定します。

AWS 用プロファイルは DynamoDB、S3、非同期処理、DynamoDB のレート制限、Turnstile の迂回禁止をまとめて選びます。模擬証拠や開発用レシートへ切り替えることはできません。休止用の target-aws-async-quiesced はサーバー専用で、ブラウザには対応する値を公開しません。復旧時のキュー消費停止は、停止して復旧先を切り替える手順で明示的に制御します。

AWS のデプロイ先は RUNTIME_DEPLOYMENT_ENV=develop|main で指定し、アカウント、リージョン、テーブル、キューなどの識別子を別途検証します。秘密値はプロファイルへ直接渡さず、許可された参照先から解決します。参照を解決する処理も、最初に確定したアカウント・リージョン・環境に固定されます。

REST Gateway の入力境界

リポジトリの構成は Regional REST API と live stage を使います。CloudFront が stage を origin path に加えるため、公開 URL は変わりません。共有 request schema から生成したモデルで、投票、finalization 作成・cancel、verification 開始・観測の POST 本文を Lambda より先に検査します。session 作成の本文省略は維持します。 Gateway の拒否は capability 認証を済ませた証拠ではなく、本文と認証が両方不正なら 400 が先になる場合があります。Hono の認証・本文上限・意味の検証は残ります。

相関には利用者が上書きできない extendedRequestId を使い、ログには resource template と固定分類だけを記録します。共通 CloudWatch role は App から変更しません。 JSON 本文をバイナリ扱いしないよう binary media type は指定せず、応答には Lambda の レスポンスストリーミングを使います。Hono の応答を元の bytes に戻して送るため、ZIP は Accept の順序に依存しません。artifact の読み出し上限は維持し、API cache は無効です。 モデル拒否、CORS、binary 配信と metrics の実測は、別途承認された AWS 切り替え後に確認します。この source の記述は配備済みであることを意味しません。

処理を分けて待ち時間を引き受ける

投票受付と証明生成では、使う資源も失敗したときの対応も異なります。投票受付は、その場で入力を確かめて保存し、レシートを返す処理です。証明生成は、保存した入力を使って長時間計算する作業です。AWS のサービスは、この違いに合わせて分担しています。

短い処理はLambdaで返す

public-api Lambda は、投票、集計の受付、進捗の取得、証拠の配信を担当します。DynamoDB がセッションと投票の状態を保持するので、次の要求を処理する Lambda が前回と同じ実行個体である必要はありません。

証明生成を始める要求に対しては、API が入力と作業状態を保存し、SQS に作業を登録して 202 Accepted を返します。この応答が示すのは受付までです。計算の成功や検証の成功を先取りしません。

長い計算はFargateの一回限りのジョブへ渡す

プローバーは ARM64 Linux の CPU 用コンテナです。現行 IaC の既定値は 16 vCPU / 32 GiB で、ECS Fargate が一回限りのタスクとして実行します。ブラウザ向けのサーバーではなく、S3 から入力を読み、証明と関連ファイルを書き出して終了します。

SQS と Step Functions は別の待ち時間を受け持ちます。SQS は、起動要求を一時的な障害で失わないためのキューです。proof-dispatcher が要求を確認して Step Functions を開始すると、SQS 側の仕事は終わります。その後の署名確認、同時実行枠の待機、タスクの実行、結果保存は Step Functions が順序を管理します。

flowchart TB
  Q["SQS：起動要求を保持"] --> D["dispatcher：要求を確認"]
  D --> S["Step Functions：実行順序を管理"]
  S --> P["Fargate：証明を計算"]
  P --> W["writer：結果を保存"]

この分担により、計算資源が埋まっていても API は進捗を返せます。同時実行枠を待っている間は pending のままで、実際に開始を許可した時点で running に変えます。取消や重複配送も含む正確な遷移は非同期プローバーで説明します。

証明の検証も独立した作業にする

証明を作れたことと、その証明を期待する Image ID で検証できたことは別です。検証要求はもう一つの SQS キュー verification-work に入り、verification-worker Lambda が Rust の verifier-service を呼び出します。

このワーカーは保存済みバンドルを読み、STARK レシートを検証し、保護された検証レポートを保存します。証明生成のキューを使い回さないため、計算を待つ作業と、できあがった証拠を検証する作業の滞留を分けて調べられます。ブラウザは引き続き通常の API から結果を取得します。

変更の周期も分ける

API の修正のたびに、証明生成用のネットワークやコンテナのビルド環境まで作り直す必要はありません。そこで稼働アプリ、実行の前提となる資源、デプロイの仕組みを、それぞれ App、Foundation、Bootstrap という Terraform の管理単位に分けます。

App は選ばれたコンテナを使い、Foundation はイメージ保管庫や署名設定を用意し、Bootstrap は計画・承認・適用の経路を管理します。どの変更がどの承認を必要とするかは、この単位で決まります。Terraformでは、その分担を保存済み計画と受入記録へどう結び付けるかを説明します。

状態と証拠をどこへ保存するか

ブラウザを閉じても、受け付けた集計作業とその進捗は AWS 側に残ります。DynamoDB は「今どの状態か」を保持し、S3 は「何を入力し、どの証拠ができたか」を保持します。状態が完了を示すとき、対応する証拠を読み出せるように、両者を sessionId と finalizationId で結び付けます。

DynamoDBに残す状態

sessions table のパーティションキーは文字列の sessionId です。ただし、セッションに関する情報を一つの大きな行へ詰め込みません。作成時に固定する選挙情報と、投票で変わる掲示板、集計の進捗、検証結果を別のレコードにします。別々のワーカーが更新するときに、担当外の情報まで上書きしないためです。

votes table は (sessionId, voteIndex) の複合キーを使い、voteId、暗号化した選択肢と乱数、コミットメント、時刻、rootAtCast、isUserVote、expiresAt を保持します。ブラウザはこれらのテーブルへ直接アクセスせず、API とワーカーがそれぞれの IAM 権限で読み書きします。

期限のあるセッション関連レコードは用途に応じて expiresAt を持ちます。レシート掲示板の全体カウンターは独立した TTL なしのレコードです。API のレート制限には、別の RateLimitEvents / RateLimitCounters テーブルを PAY_PER_REQUEST で使い、プローバーの同時実行枠にも専用の DynamoDB テーブルを使います。

本番環境は Terraform が管理する primary の sessions / votes の組を参照します。develop では、休止を伴うアプリ復旧経路で replacement の組へ切り替えられます。個々のワーカーが独自に保存先を選ぶことはありません。

S3に残す入力と成果物

証明ファイルの保存先は非公開・バージョニング有効の S3 バケットです。サーバー側暗号化は AES256 を使い、現在版と旧版のオブジェクトはともに7日で削除するライフサイクルを設定します。

一回の集計のファイルは、次の同じ接頭辞にまとめます。

sessions/{sessionId}/{finalizationId}/

AWS では S3_PROOF_PREFIX=sessions/ が Terraform と実行時検証の共通条件です。API、dispatcher、writer、verification worker は、保存キーがこの形式と対象の識別子に一致することを確認します。名前の一致を曖昧にすると、別の集計のファイルを読み込む危険があるためです。

input.json はプローバーへの非公開入力です。プローバーが生成する *-receipt.json と *-output.json は host の中間出力で、それぞれ配布用の receipt.json と journal.json の元になります。配布用 ZIP の中身と、外に残すビットマップなどのファイルはバンドル構造で定義しています。

同じ S3 に保存されていても、すべてのファイルを配布するわけではありません。API は公開境界に従ってファイルの種類とセッション権限を確認してから返します。

生成済みの証拠を検証する通信

集計の完了後、検証開始 API は capability、現在の集計が成功していること、集計ごとのバンドル保存場所、期待する Image ID を確認します。作業を verification-work に登録した応答は verificationStatus=running と finalizationId、推定所要時間、冪等な再要求かどうかを返します。

sequenceDiagram
  participant B as ブラウザ
  participant A as API
  participant Q as 検証キュー
  participant W as verification-worker
  participant S as S3
  participant D as DynamoDB
  B->>A: 検証を開始
  A->>Q: 対象集計とバンドルの場所を登録
  A-->>B: running
  Q->>W: 作業を配送
  W->>S: bundle.zipを取得
  W->>W: Rustでレシートを検証
  W->>S: verification.jsonを保存
  W->>D: 検証結果と保存場所を記録
  B->>A: 検証状態を取得
  A->>D: 最新の結果を読む
  A-->>B: 検証結果

ワーカーは Receipt::verify(expected_image_id) を実行します。AWS では検証結果を verification.json として保存することも完了条件です。レポートがない場合やアップロードに失敗した場合、検証作業を成功として扱いません。

保存に成功すると、結果は VERIFICATION_RESULT、バンドルとレポートの保存場所は VERIFICATION_DELIVERY に分けて記録します。レポート保存に失敗しても既存の s3BundleKey は失いません。このレポートは後続の capability 付き API から取得でき、公開 ZIP には入れません。

この通信で得る STARK 検証結果を、ブラウザは投票時の記録や掲示板の確認と合わせます。ワーカーの成功だけで画面全体の判定は決まりません。

プローバーだけをVPC内に配置する

本番で稼働する Fargate のプローバータスクは、Foundation が管理する VPC に配置します。develop も同じネットワーク構成を使います。API Gateway、Lambda、DynamoDB、S3、CloudFront は VPC 外のマネージドサービスとして動きます。

VPC の範囲は 10.42.0.0/20。利用可能な最初の二つの AZ に、それぞれ 10.42.0.0/24 と 10.42.1.0/24 のパブリックサブネットを置きます。AZ の末尾文字は固定せず、Terraform が取得した値を使います。

flowchart TB
  P["Fargateタスク<br/>パブリックIPあり"] --> G["Internet Gateway"]
  G --> E["ECR：イメージ取得"]
  G --> S["S3：入力・証拠"]
  G --> L["CloudWatch Logs"]

タスクのセキュリティグループは受信通信を全拒否します。パブリック IP があっても、外部から接続を開始することはできません。送信は 0.0.0.0/0 への全プロトコル・全ポートを許可します。これはプローバーが ECR、S3、ログなどへ接続するための構成であり、送信先を厳密に限定したネットワークではありません。

非同期プローバー

集計要求が受け付けられてから、実際に計算が始まるまでには待ち時間があります。キューの再配送で同じ要求が届くことも、その間に利用者が取り消すこともあります。非同期プローバーは、作業が届いたという理由だけでは起動せず、保存済みの集計状態を確認してから計算へ進みます。

集計要求を受け付ける

POST /api/sessions/:sessionId/finalizations は、URL のセッションと capability を照合し、Turnstile、レート制限、集計開始の前提条件を確認します。AWS の非同期経路では、次の順で作業を登録します。

1. zkVM 入力を構築し、集計状態を pending として保存する。
2. 非公開 S3 の sessions/{sessionId}/{finalizationId}/input.json に入力を保存する。
3. 正しい S3 キーを含む作業メッセージを SQS へ送る。
4. 202 Accepted と、pending の FinalizationResource を返す。

応答には状態取得 URL を含めません。クライアントは既知の GET /api/sessions/:sessionId/finalizations/current を capability 付きで呼び出します。

キューから作業を起動する

proof-dispatcher は SQS メッセージを一件ずつ読みます。まずメッセージの形、recordType、セッションと集計の識別子を検証し、入力、出力先、バンドルの S3 キーが同じ集計の正規の配置であることを確認します。必要な AWS 設定が欠けていても開始できません。

次に、現在の集計レコードを読みます。該当するレコードがない場合や、メッセージの finalizationId が現在の pending と一致しない場合は、古い作業として破棄します。取消後に再配送された要求が、新しい計算を始めるのを防ぐためです。一方、壊れたメッセージ、キーの不整合、一時的な AWS 呼び出し失敗は再試行し、解消しなければ DLQ へ移します。

条件を満たすと StartExecution で Step Functions を開始します。dispatcher は入力ファイルを保存し直さず、この時点では状態を running にも変えません。計算資源の空きがまだ分からないからです。

develop の保守設定を有効にすると、新規セッション作成とプローバー・検証の SQS event-source mapping を止めます。未消費の要求はキューに残り、集計も pending のまま残り得ます。既存セッションの書込みと実行中の仕事の停止・整合確認は別途必要です。再開は新しいソースの保存 plan と承認で扱います。

Step Functions

Step Functions は、起動前の確認と計算の後始末を順序付けます。

flowchart TD
  S["コンテナの署名を検証"] -->|成功| C["同時実行枠を取得"]
  C --> G["現在も開始できる集計か確認"]
  G -->|開始を許可| P["Fargateで証明生成"]
  G -->|取消・別の集計へ移行済み| R["枠を解放して終了"]
  P --> F["枠を解放"]
  F --> W["成功・失敗・時間切れを保存"]

署名を確かめてから資源を確保する

最初の VerifyImageSignature は、image-signature-verifier Lambda の runtime alias を呼びます。対象は、デプロイ時に内容のダイジェストで固定したプローバーイメージです。result = VERIFIED と mode = cryptographic の両方がそろった場合だけ、同時実行枠の取得へ進みます。

署名処理中、署名プロファイルの不一致、検証資産や信頼ポリシーの不整合、暗号学的検証の失敗、時間切れはすべて起動を止めます。Lambda 呼び出し自体が回数を制限した再試行後も失敗すると、RecordSignatureInvocationFailure が拒否結果へ変換し、CallbackSignatureFailed で失敗を記録します。イメージ署名が説明するように、署名処理の完了表示だけではこの条件を満たしません。

待っている間の取消を見落とさない

AcquireProverSlot は DynamoDB の semaphore で、RunProver へ同時に進める数を制限します。枠が埋まっている間は Step Functions 内で待機・再試行し、利用者へは pending を返します。待機の上限に達すれば容量待ちの失敗を記録します。

枠を取れた後、MarkProverStarted が finalization-writer を呼び、ストアの更新条件をもう一度確認します。ここで開始を許可した場合だけ running と startedAt を保存します。待機中に取り消されたり、別の集計へ置き換わったりしていれば、枠を返して終了し、タスクを起動しません。

RunProver は ecs:runTask.sync で Fargate タスクを起動して完了を待ちます。正常終了、時間切れ、その他の失敗に応じて枠を解放し、writer に結果を通知します。running は開始が許可された状態なので、タスク開始の再試行中も含みます。

解放し損ねた枠を回収する

通常の解放は state machine の成功・時間切れ・失敗経路が担います。semaphore-janitor は、その後始末が完了しなかった場合を補います。

janitor は Step Functions の終了イベントで所有者の解放を試み、さらに30分ごとの確認で「タスクの時間制限＋15分」より古い所有者を調べます。古いというだけでは削除しません。対応する実行が RUNNING または PENDING_REDRIVE なら保持し、終了済みか存在しないことを確認できた実行だけを条件付き更新で解放します。

コンテナ内で証明を生成する

プローバーは 16 vCPU / 32 GiB を既定とする一回限りのタスクです。Step Functions から、入力の INPUT_S3_BUCKET / INPUT_S3_KEY、出力の OUTPUT_S3_BUCKET / OUTPUT_S3_PREFIX、期待する EXPECTED_IMAGE_ID を受け取ります。

コンテナの entrypoint は S3 から入力を取得し、必須フィールドを確認して zkVM host を実行します。続いて Rust の prover-artifacts が非公開入力と host 出力を厳密に読み、journal.json と公開監査用の public-input.json、election-manifest.json、close-statement.json を作ります。

ファイルを書けただけでは配布しません。同じ Rust ツールで読み直し、ジャーナルと公開監査ファイルの methodVersion、入力コミットメント、選挙情報の一致を確認します。その後、次の五つだけを ZIP にして、個別の関連ファイルとともに非公開 S3 へアップロードします。

receipt.json
journal.json
public-input.json
election-manifest.json
close-statement.json

公開監査ファイルと正規化したハッシュの計算は zkvm/host/src/artifacts.rs が担当します。shell はプロセス起動、ファイル、ZIP、S3 と配布対象の制限を担当します。AWS 用プロファイルとこのコンテナは本物の STARK 証拠だけを許可し、開発用レシートを成功証明にできません。

生成したファイルを公開用と内部用に分ける

一回の集計に属するファイルでも、すべてを ZIP に入れません。input.json など、公開しないファイルを除外します。形式と配置はバンドル構造にあります。

生成したビットマップは ZIP の外の同じ集計用接頭辞へ保存します。S3 に存在するだけで利用可能とは宣言せず、writer が内容を検証し、集計結果と一緒に保存できたことをもって利用可能にします。verification.json はこの段階ではまだなく、後続の検証作業で保存した後にレポート取得 API から配信します。

failure-marker.json の契約

コンテナが非ゼロ終了した場合、entrypoint は可能なら failure-marker.json を保存します。これは画面へ生のエラーを出さずに、障害の種類を writer へ伝えるための非公開ファイルです。

内容は category だけで、値は configuration、input、prover_execution、infrastructure_interruption、artifact、upload、timeout、unknown に限定します。生のエラー、識別子、保存先、イメージ情報、認証情報は入れません。

同じ集計の S3 接頭辞に新規作成のみを許可し、既存の異なる内容を上書きしません。writer は形と値を検証できたときだけ障害詳細へ取り込みます。存在しない場合や不正な場合は、一般的なタスク失敗として扱います。公開 ZIP、レポート、ブラウザ向けダウンロードには含めません。

結果の通知と保存を確定する

成功通知を受けた finalization-writer は、まずバンドルのキーが sessions/{sessionId}/{finalizationId}/bundle.zip と一致することを確認します。バンドルからレシート、ジャーナル、公開監査ファイルを復元し、存在する個別ビットマップをビットマップの契約で検証します。

復元が一時的に失敗した場合は、Step Functions が回数を制限して通知を再試行します。一時的ではない復元失敗は FINALIZATION_BUNDLE_RESTORE_FAILED として記録し、集計を failed にします。

復元できた結果とビットマップの利用可否、利用可能と宣言する付随データは、一つのトランザクションで保存します。この保存が失敗しても succeeded は公開せず、通知が再試行された場合に保存をやり直します。

失敗通知では署名、タスク、時間切れなどの理由を保存します。PROVER_TASK_FAILED の場合は、同じ集計の failure-marker.json を上記の条件で読み取ります。通知自体の配信失敗も Step Functions の再試行上限と失敗状態に従います。

ブラウザが完了を待つ

GET /api/sessions/:sessionId/finalizations/current は、現在の集計について次の進捗を返します。

succeeded は証明生成の完了です。画面の「Verified」は、これからレシート、ジャーナル、投票と掲示板の証拠を評価して決まります。

証拠をダウンロードする

バンドルとレポートは capability で保護された API から取得します。大きい bundle.zip は Range 応答で分割取得できます。API は集計の識別子と S3 キーを照合し、別の集計のファイルや正規の配置でないファイルを返しません。直接の S3 URL や署名付き URL は通常のブラウザ・CLI の取得契約ではありません。

起動するコンテナを確かめる

STARK レシートを期待する Image ID で検証すれば、計算を行ったゲストプログラムを確かめられます。しかし、その検証は計算の後です。未承認のコンテナが先に起動し、入力や実行権限へ触れてしまうことは防げません。

そこで AWS では、起動するプローバーコンテナ自体にも署名を要求します。承認された内容のダイジェストを選び、期待する署名者で検証できることを、アプリへの採用前と証明生成の直前に確かめます。

Image ID との関係

二つの「イメージ」は対象が異なります。

flowchart TB
  C["コンテナの署名を確認"] --> P["プローバーを起動"]
  P --> R["STARKレシート"]
  I["期待するImage ID"] --> V["レシートを検証"]
  R --> V

コンテナの署名が正しくても、得票表示や投票の包含まで正しいとは言えません。公開検証でゲストの同一性を判断する根拠は、期待する Image IDと STARK レシート検証です。さらに総合判定には他の必須チェックも必要です。

この署名方式は AWS Signer のプロファイル、ECR の署名設定、検証ツールと信頼ルート、デプロイ権限の分離を信頼します。第三者がコンテナの再現可能ビルドを独立に証明する仕組みではありません。署名の事前確認や採用記録は運用側の記録で、公開証拠 ZIP には入りません。

ダイジェスト固定

タグは別のイメージへ付け替えられます。そこで、アプリが使う prover_image_uri は @sha256:<64-hex> で終わる URI に限定します。ビルドや push でタグを使っても、事前確認と実行時確認は常にこの内容ダイジェストを対象にします。

ベースとなる RISC Zero Toolchain もダイジェストで固定します。ただし、署名の扱いは二つのリポジトリで異なります。

Foundation が両リポジトリを管理し、Signer プロファイルと ECR managed signing の対象は Prover に限定します。App はリポジトリやイメージを作らず、採用済みのダイジェスト固定 URI を受け取ります。

ビルドと署名の概念

新しいプローバー候補は ARM64 用にビルドします。まず Image ID と methodVersion を取り出し、ECR へ push した後、そのダイジェストを指定して pull し直します。再取得したコンテナから同じ二値を取り出して比較し、手元で確認したものと登録したものの一致を確かめます。

候補のメタデータを出す前に、ECR scan が PASS、期待する署名プロファイルの managed-signing status が COMPLETE であることを要求します。記録にはコンテナのダイジェスト、スキャン、Image ID / methodVersion、ソース、固定した Toolchain の参照、managedSigningStatus: COMPLETE を結び付けます。

ここで COMPLETE が示すのは署名処理の完了です。実際の署名を信頼ポリシーに照らして検証できたことは、まだ示していません。暗号学的検証は後述の App 事前確認と実行前確認で行います。

候補を作る承認と、その候補を採用する承認は別です。候補・リリースの記録は内容のハッシュを含むキーで保存し、採用先を指すポインターにはリリース記録のキーだけを置きます。ポインターは初回作成または比較してからの条件付き更新で進め、別の更新を上書きしません。

flowchart TB
  B["候補作成の承認"] --> C["ビルドと候補検査"]
  C --> R["候補記録を保存"]
  R --> A["採用の承認"]
  A --> P["リリース記録と採用先を更新"]

保持済み候補を選ぶ existing でも、この二つの承認を分けます。入力は内容ハッシュで特定する候補キー一つだけです。Toolchain との結び付き、ECR 上のダイジェスト、HIGH / CRITICAL の検出が0件であること、署名処理完了を改めて確認します。この経路の候補確認は読み取りのみで、ビルド、push、スキャン・署名要求、候補の書き換え、ECR の変更は行いません。

App の変更前と起動前に確認する

通常の App デプロイは、呼び出し元が先に固定した対象環境について、現在の Foundation と Toolchain / Prover の採用先を一度だけ解決します。現在の Foundation が選択ソースの資源・consumer 要件を満たし、Prover の記録が要求するゲスト契約と対応することを確認した選択を、後続処理へ引き継ぎます。

準備工程では、チェックサムで固定した Notation、AWS Signer plugin、ECR credential helper、信頼ルートを CodeBuild で使い、選択した digest を native CLI で検証します。同じ assets を runtime Lambda の ZIP にまとめ、成功証跡と正確な S3 VersionId・SHA-256 を完全な App 計画へ結びます。拒否、失効、timeout や不一致では配備へ進みません。

通常の App 計画を一度承認し、Apply が verifier のコード・設定と変更不能バージョンを配備します。Step Functions はその qualified ARN を直接呼び、Prover 起動直前にも署名を再検証します。事前配備、preflight/runtime alias、別承認はありません。Apply と Smoke が同じコード・設定・バージョンを確認してから受入記録を公開します。

検証する順序

verifier は次の六段階を実行します。

1. アカウント、リージョン、リポジトリ、ダイジェスト、URI、署名プロファイルの整合を確認する。
2. DescribeImageSigningStatus を時間と回数を制限して呼び、期待するプロファイルが一意で COMPLETE であることを確認する。
3. 同梱ファイルの許可一覧、種類、サイズ、モード、チェックサムを確認し、期待する資産マニフェストと信頼ルートに照合する。
4. 対象リポジトリと署名プロファイルに限った strict trust policy を一時作業領域に作る。
5. notation verify <digest-pinned-image-uri> を、実行時間を制限して呼び出す。
6. 成功時は result = VERIFIED、mode = cryptographic、verifier version、trust-policy hash を返す。失敗は定義済みの理由コードへ絞って返す。

Step Functions が次へ進むのは VERIFIED と cryptographic の両方があるときだけです。署名の準備不足、資産やポリシーの不一致、Notation の失敗、時間切れ、Lambda 呼び出し失敗では、同時実行枠の取得も ECS 起動も行いません。

検証器自体の取り違えを防ぐ

デプロイ時には Lambda のコードハッシュと、設定を正規化して計算したハッシュを必ず照合します。AWS の COPY モードの応答がネイティブの ConfigSha256 や ResolvedS3Object を省略した場合は null のまま保持し、値を補作しません。AWS が返した場合はそのハッシュや S3 座標も照合します。部分的に壊れた S3 座標は拒否し、期限付きのダウンロードURL Code.Location は保持しません。

VPC を使わない関数では、VPC 設定全体の省略、または VPC ID が空・セキュリティグループが空・IPv6 dual stack が明示的に false の場合に限る subnet ID の省略を、VPC なしの設定として正規化します。それ以外の不完全な応答を VPC なしと推定しません。

署名準備で使った assets と、計画に固定した ZIP を一致させ、Apply 後は実際の immutable version と Step Functions の呼出先を確認します。Smoke が別バージョンを観測した場合は失敗です。過去の App 受入記録による再構成は行わず、修正した現在ソースを新しい計画と承認で配備します。

変更する内容を計画と承認に結び付ける

デプロイの途中でソースやイメージが変わると、レビューした内容と実際に動かした内容が食い違います。この構成では、変更前に Terraform の計画を保存し、対象ソース、入力、実行環境、計画のチェックサムをまとめて承認します。Apply は、その保存済み計画を作り直さずに適用します。

適用できたことだけでも十分ではありません。適用後の動作・構成確認である Smoke が成功してから、何を受け入れたかを記録します。この「受入記録（acceptance）」が、後の差分調査で参照する具体的な構成と成果物を定めます。

レビュー対象の plan package は変更不能な参照として保存します。成功した各 root の現在の受入記録は checkpoint.json に置き、Plan が観測した ETag に対する条件付き更新で進めます。初回作成は明示した不在条件に限ります。過去の版は S3 VersionId で特定でき、失敗した実行から成功記録を公開しません。

次の図はソースに定義された継続運用の経路です。Bootstrap はローカルのレビュー済み操作、Foundation・Toolchain・Prover・App は4本の管理パイプラインです。両環境のアカウント・権限・保存先を分離します。ソースの定義と各環境への導入状況は別であり、この図は本番への切替完了を表しません。

flowchart TD
  Source[固定したソース] --> Bootstrap[Bootstrap: local 計画 → 承認 → 適用 → Smoke]
  Source --> Foundation[Foundation: 計画 → 承認 → 適用 → Smoke]
  Source --> Toolchain[Toolchain: candidate → 昇格]
  Source --> Prover[Prover: candidate → 昇格]
  Source --> App[App: 準備・計画 → 承認 → 配備・Smoke]
  Toolchain --> Prover
  Prover --> App
  Foundation --> App
  App --> Evidence[受入記録・成果物・現在の状態]

変更の単位を分ける

API、コンテナ保管庫、デプロイ権限は変更の周期が違います。そこで Terraform の root を分け、それぞれが独立した state、計画、実行権限を持ちます。アプリの修正計画へ、署名基盤やデプロイ制御の変更が紛れ込まないようにするためです。

flowchart TB
  B["Bootstrap<br/>変更を実行する仕組み"] --> F["Foundation<br/>アプリの前提資源"]
  B --> A["App<br/>稼働アプリ"]
  F -->|検証済みの設定と参照| A

App と Foundation は明示的な root です。Bootstrap は CodeBuild ロググループの共通 module を使います。共有化によって state やデプロイ経路を増やさず、既存の資源 identity と保持ログを保全します。通常の計画審査では move/import を拒否し、state の手編集で迂回しません。

変更対象と保存先を固定する

packages/deployment-authority/deployment-targets.json は、許可対象、各経路、state、backend、ポリシー、生成名の共通の定義です。三つの root は同じ JSON を読み、選択と root 入力の不一致を拒否します。対象全体のハッシュ targetConfigurationSha256 は、共有名と閉じている経路も含む完全な設定を拘束します。

対象は stark-dev/develop と stark-prod/main です。共通の root と target 設定を使いながら、account・state・権限・採用記録を分離します。検証済み source の変更を環境ごとの計画と承認で配布し、dev の計画や署名・採用記録を prod に流用しません。配置済み source の差と、採用構成からの drift は区別します。

state の識別には account_alias、deployment_environment、state_scope、state_backend_key を使います。S3 のキーにも範囲を含めます。

追跡する backend.tf は backend "s3" {} という部分設定で、bucket、region、key、lockfile 設定は root ごとの検証済み入力から与えます。呼び出し元のロール、ソースブランチ、アカウント、環境、state 範囲を合わせて確認し、別環境への取り違えを防ぎます。

Foundation と App の変更は AWS 管理の CodePipeline / CodeBuild を通し、Bootstrap と差分調査は別のローカル操作を使います。ローカルの App apply は通常の配備経路ではありません。名前、参照、ハッシュ、計画、承認、条件付き公開の検証は @stark-ballot/deployment-authority に集約します。

Bootstrap が変更の仕組みを管理する

Bootstrap は、変更を実行する側の権限も管理します。state bucket と KMS key、root ごとの backend grant、CodePipeline / CodeBuild、デプロイロール、ログ、成果物と受入記録の保存先がここに属します。

Bootstrap は Linux の固定実行環境、独立した管理者 identity、既存 backend、停止・drain 済みの管理処理を確認し、完全な保存計画をレビューします。対象・source・package hash を結び付けた承認後に Apply と Smoke を実行し、checkpoint を条件付き公開します。新しい対象に限り、backend と制御基盤を順に作る専用 initializer を使えます。既存環境で checkpoint がないことは初期化の根拠になりません。

すべての現行 CodeBuild プロジェクトは、固定したソースからリポジトリにある buildspec を選びます。起動時には project、role、source、buildspec、計算資源、実行設定、特権実行の有無、解決済みソースを照合します。特権実行が可能なのは ARM Docker を作る Toolchain / Prover の候補 project だけです。

実行中の BatchGetBuilds 応答を、ソースが所有する project inventory と照合します。buildspec、service role、compute type、environment type、privileged mode の不一致・欠落を拒否します。現在の project 設定を、その実行で使われた設定の証拠として代用しません。IAM による起動制限も別途維持します。

App の Source は CODEBUILD_CLONE_REF を渡します。後続の CodeBuild が Git の追跡ファイル、差分、祖先関係を検査できるようにするためです。接続の利用権限は、これを消費する CodeBuild ロールの、正確な CodeConnections ARN への codeconnections:UseConnection に限定します。

保存済み計画と承認

Plan は target、backend、source、実行、Terraform version とアーカイブ checksum、provider lock、非秘密入力、成果物・依存記録の正確な参照、保存 binary plan と plan JSON を一つの plan package に結びます。Apply は同じ lock と保存計画を使い、その場で再計画しません。

計画の実行可否も意味のある差分と照合します。完全な計画が applyable: false になるのは、すべての resource、read、root output の action が no-op の場合だけです。差分があるのに実行不可、差分がないのに実行可能、あるいは move、import、deferred change、action invocation、不完全・不正な解析結果があれば拒否します。承認を付けてもその不整合は救済しません。

Apply は plan package の正確な VersionId・SHA-256 と同じ実行の承認を検証します。変更前に Plan が固定した mutation owner を条件付きで引き継ぎ、execution/stage/action ごとの開始マーカーを新規作成します。再試行で build ID が変わっても同じ変更を再実行できません。後段は同じ owner と先行 action の成功を要求します。

Bootstrap、Foundation、すべての App デプロイでは no-op 計画にも承認が必要です。App の署名確認は準備工程で実行し、verifier を含む完全な計画を一度承認します。

Plan 用マネージドイメージを変更する場合は、適用した設定を読み取りで確認した後、同じソースで対象経路の新しい Plan を実行します。変更前の実行環境の記録を、変更後に作った計画の証拠として使わないためです。

Foundation がアプリの前提を用意する

Foundation は、Prover / Toolchain の ECR とリリース保存先、Prover の署名設定、秘密値・設定の参照先、ネットワークを用意します。Bootstrap が作ったパイプラインで計画・承認・適用・Smoke を行い、アプリが使う前提を受入記録へ固定します。

新しい Foundation の初回構築も通常の Plan・承認・Apply・Smoke を使います。既存の本番環境は既存 state を保ち、契約切替として checkpoint の初回公開を明示します。新規 state の初回構築と checkpoint の初回公開は異なる条件です。

初回の不在条件は、正確な対象の完全な版一覧など、成功した読み取りで確かめます。アクセス拒否、timeout、不完全な一覧、削除マーカーを「未作成」と扱いません。過去の失敗が残した mutation owner も新しい計画で確認します。

Foundation checkpoint は plan package と実行・backend を結び、ネットワーク、image authority と明示的な consumer contract を公開します。利用側が必要とする資源の要件と、image 作成時の来歴を分けて検証します。

通常の App と Prover は現在の Foundation を一度選び、現在の source が要求する資源・契約への適合を確認します。image 作成時の Foundation ハッシュは不変の来歴です。digest、署名、ImageID、ゲスト契約などが適合し、実 image が存在すれば、無関係な IaC 変更や同じ digest の再昇格だけで再ビルドしません。イメージ署名も参照してください。

App の計画から受入記録まで

App は現在のソースと採用済み image を選び、四つの stage で配備します。

Source
  → Prepare（release 解決・native 署名検証・完全な保存済み計画）
  → ManualApproval（空計画でも必須）
  → DeployApplication（Apply・静的配信・Smoke・受入と current 公開）

最後の stage は QUEUED で順序を保ちます。ただしトランザクションではなく、失敗した部分配備は新しい計画で確認する必要があります。

通常の変更

Prepare は現在の Foundation と Toolchain / Prover を一度だけ選びます。Plan は source 検査と native 署名検証を実行し、使用した同じ固定 assets を Lambda ZIP にまとめます。対象、source、実行、digest、trust、S3 の正確な VersionId と SHA-256 を保存済み計画へ結びます。

通常の App Apply が verifier のコードと設定を更新し、変更不能なバージョンを公開します。Step Functions はその qualified ARN を直接呼びます。Apply は実際のコード、設定、IAM と呼出先を検証し、Smoke は同じバージョンを確認します。部分配備や不一致では受入・current を公開しません。

初回の受入記録を作る

既存 target は現在の checkpoint を使います。欠落や読取り失敗から初期化へ切り替えません。初回公開は対象の実際の state・owner と不在条件を明示的に確認し、完全な計画、承認、Apply、静的公開、Smoke を通します。既存環境の修復に新規初期化を使いません。

承認が必要になる条件

すべての action が no-op でも ManualApproval / ApproveTargetRuntimeApply は必須です。frontend だけの変更も同じ承認を通ります。Apply は保存済み計画、実行 ID、source、checksum に結び付く承認証跡を検証します。署名確認専用の別承認はありません。

修正したソースを配備する

過去の App 受入記録から構成と成果物を再構成する汎用 rollback は撤去しました。現在の契約に適合する修正 commit を用意し、新しい計画、承認、Apply、Smoke を通します。適合する採用済み image は再利用します。データ復元、state 修復、本番操作や削除には、それぞれ別の許可が必要です。

動作確認後に受入記録を残す

同じ execution/package の owning Smoke が成功してから、root の現在の記録 deployment/{targetKey}/{root}/checkpoint.json を公開します。source、実行、plan package の正確な参照、backend、再現用の入力を結び、App では配置した image・method と runtime identity も確認します。

Plan 前の ETag または明示的な初回不在条件を使って更新します。別の owner/checkpoint が進んでいれば拒否し、後続実行の値を読み直して古い結果を上書きしません。アクセス拒否は不在ではありません。応答不明や部分変更の後は実際の effects を確認し、新しい実行・計画・承認で進めます。

S3 の VersionId は保存版の特定、ETag は比較更新に使います。PublishCurrentStatus は成功した checkpoint から状態を導くキャッシュであり、承認や投票結果の Verified を成立させる証拠ではありません。

静的ファイルの公開が競合しないようにする

静的配信は両環境とも通常の App 経路で行います。Apply、静的配信、Smoke、状態公開を一つの QUEUED stage に置き、同じ対象への公開順序を守ります。専用の static-fast 経路と S3 リースは廃止しました。

この順序制御はトランザクションではありません。失敗すると一部のファイルが更新済みになることがありますが、失敗した公開から新しい受入記録は作りません。公開中の処理を止めて次の実行を先行させず、修正したソースで通常の計画・承認・配備をやり直します。

公開するファイル群の識別には、専用のドメイン分離をした形式で、整列したパス、正確なバイト数、SHA-256 を含めます。各ファイルを必ず同じチェックサムでアップロードしてから、不要なキーを削除します。S3 sync の時刻やサイズを内容の根拠にしません。静的配信も現在の選択ソースから作った成果物を使います。

DynamoDB の復旧先を切り替える

PITR と元テーブルを保ち、停止期間を設けて別名の sessions / votes テーブルへ復元します。4 段階の復旧制御とマニフェストによる自動切替は廃止しました。復元先の二表の対応、スキーマ、索引、KMS、TTL、PITR、削除保護、IAM を検証してから、具体的な参照先の設定変更を新しいソースと保存 plan・承認・smoke で配備します。元テーブルを削除して同名へ復元する手順は使いません。

develop の application_quiesced はソースとしてレビューする保守設定です。新規セッションとキュー消費、期限切れ finalization の sweep を止めますが、既存セッションへの書込みや実行中のジョブを自動停止しません。運用者が入口を閉じ、すべての書込み元の停止・処理完了を確認する必要があります。再開も新しい plan と承認で行います。旧表へ戻しても新表への書込みは同期されません。データ検証、RTO / RPO、停止許容時間、再開、後日の削除は個別の許可と証跡を要し、リポジトリのテスト成功だけでは復旧可能とは主張しません。

開発環境の入口の鍵を管理する

develop の入口 Cookie の鍵は、追跡する keyset manifest で世代と状態を管理します。App は各世代に RSA_2048 / SIGN_VERIFY の KMS key を作り、公開鍵だけを CloudFront trusted key group へ登録します。発行元は必ず一つとし、trusted-retiring と detached で鍵の重なりと失効を表します。Smoke は develop の鍵構成を照合し、main ではこの Cookie による入口制限が無効で、鍵や trusted key group を持たないことを確認します。

秘密鍵は KMS から取り出しません。state、リポジトリ、パイプライン成果物、Smoke 証拠には秘密の署名材料を入れず、Plan / Apply / Smoke / 稼働アプリのロールには kms:Sign を与えません。Cookie の発行は、それらから分離した運用者の署名権限で行います。

受入済みの構成との差分を調べる

三つの root はそれぞれ、現在の checkpoint の正確な版から、採用した source・plan package・provider lock・非秘密入力・成果物を再現します。差分調査は root 固有の読み取り role を使うローカル操作です。管理 project や定期 scheduler はありません。

1. 独立して選んだ target、root、identity と checkpoint を検証する。
2. checkpoint が固定した source と checksum 検証済み Terraform、provider lock、入力・成果物を専用領域へ展開する。
3. 必要 image の存在、管理処理の drain、checkpoint・mutation owner・state の版、lineage、serial を確認する。
4. terraform plan -refresh=true -lock=false を実行し、同じ観測項目を実行後にも再確認する。
5. 終了値 0 は差分なし、2 は差分あり、1 は確認失敗とする。失敗や依存欠落を clean にしない。

診断は秘匿化した限定的な差分を返し、state/lock、checkpoint、remote report を書きません。Apply や自動修正にも進みません。競合、欠落 image/artifact、読取り拒否、秘密漏洩のおそれは確認失敗です。変更は通常の担当経路で新しい計画と承認を通します。

記録と保存先を保護する

Foundation のリリース保存先、Bootstrap の Terraform 受入保存先、App 保持用保存先はバージョニングを有効にします。バケットポリシーでも、変更不能な記録は新規作成だけ、ポインターは初回作成または If-Match 付き更新だけを許可し、曖昧な条件ヘッダーと権限対象の削除を拒否します。クライアント側の条件チェックだけに任せません。

一つの SSE-KMS key を要求するポリシーは、alias ではなく正確な key ARN を比較します。書込み側が alias を解決する場合は、その定義済み alias への kms:DescribeKey で同じアカウント・リージョンの有効な鍵を確認し、S3 に ARN を渡します。この識別用の読取りと、S3 経由の暗号権限を分けます。

Full App の実行中の成果物は、対象ごとの非公開・バージョニング有効・KMS 暗号化バケットに置きます。受入記録、配備用成果物、承認、verifier 証拠、キャッシュを置く App 保持用バケットとも区別します。短命な実行ファイルの失効で、受入記録の根拠を失わないためです。

イメージ保持数と欠落時の扱い

保存期間は App / Bootstrap の storage_retention.tf に固定し、実行ごとの任意入力にしません。App はキュー、証拠ファイル、静的ファイルの旧版、ログ、五つの DynamoDB テーブルの PITR を管理し、Bootstrap は state の旧版、実行成果物、キャッシュ、ビルドログ、保持する監査記録を管理します。受入記録と採用ポインターは通常の実行成果物の失効から分離します。

ECR は各 repository で push 時刻が新しい5イメージを残す native lifecycle policy を使います。promoted/current-use の保護タグや独自 retention controller はなく、利用中の image も削除され得ます。必要 image が欠落すれば選択・配備・drift は失敗し、明示した通常の build・検証・promotion で作り直します。Toolchain が必要なら先に作り、続いて Prover と新しい App 計画を扱います。再ビルド後の digest/ImageID が元と同じとは仮定しません。

操作権限を限定する

ロールに与える権限には、操作を許可する identity policy と、その許可の上限を定める permissions boundary を使います。実際の許可は両者の共通部分に限られるので、上限側だけを見ても操作できるとは判断できません。

state は root ごとの key と lock に、Lambda は各担当処理に、Fargate は証拠接頭辞・ECR pull・ログに限定します。デプロイ、checkpoint 公開、差分調査、Cookie 発行の権限を分けます。CodeBuild の実行時検査は正確な build と native action を読み、project trust と起動経路を IAM でも制限します。

AWS provider の refresh が必要とする限定的な例外は、所有 root の調査ロールと対象に閉じます。たとえば App 調査の task definition 確認は ecs:DescribeTaskDefinition の AWS 全体の指定を必要としますが、それを ECS の一般権限へ広げません。EventBridge の名前系列を共有 boundary の上限に使う場合も、各 identity policy は現在の正確なルール一覧に限定します。

IAM の依存関係だけでは権限の反映完了を証明できません。制御経路を切り替える際は、旧 starter の権限撤去、実処理の drain と反映確認、旧 guard/role の撤去を順にレビューします。古い Apply の再実行や手動の権限追加を代替にしません。

ツールのバージョン条件

各経路は公式 Terraform linux_amd64 アーカイブのチェックサムを検証してから展開し、実際の version / platform を確認します。解決した provider lock は計画ごとの実行証拠で、追跡する root lockfile を正本にはしません。Bootstrap の共有 child module は互換性のある下限・範囲指定を持ちます。現行 root は Archive provider を使いません。

待ち時間と失敗の原因を調べる

集計画面が pending のままなら、まだ配送されていないのか、計算枠が埋まっているのか、それとも処理が止まったのかを知りたくなります。同じ画面上の状態でも原因は違います。ログと監視は、要求がどこまで進み、どの種類の失敗で止まり、どのデプロイの前後に起きたかを調べるために使います。

一方、CloudWatch のグラフが平坦でも、投票や集計の正しさは分かりません。利用がなかっただけかもしれません。画面の「Verified」は証拠と必須チェックから決め、ログ保存や通知の成功・失敗で変更しません。

投票の検証と運用の観測を分ける

flowchart TB
  E["投票・掲示板・STARKの証拠"] --> C["必須チェック"]
  C --> V["画面の判定"]
  V -->|判定後の観測| L["ログ・メトリクス"]
  L --> O["運用者が原因を調査"]

観測送信の失敗、logger の例外、CloudWatch の一時的な停止は、導出済みの判定を変えません。監視から検証へ判定を戻す経路はありません。表示条件は検証の判定規則で決まります。

観測対象とシグナル

まず、利用者の待ち時間をどの処理が引き受けているかを調べます。

ダッシュボードは調査の入口です。一回の投票操作を追うには、アプリのイベント、AWS の観測、デプロイの記録を照合します。X-Ray / OpenTelemetry の分散トレースやブラウザ RUM は構成していないため、一つの trace で全経路を復元できるわけではありません。

構造化ログと安全な相関

出力元ごとのログ形式

ログは自由文を全文検索して処理結果を推測するのではなく、定義済みイベントと値の集合を使います。TypeScript の discriminated union と実行時の許可リストが、受け入れる項目を決めます。

代表的なイベントは、受付後の finalization_admitted、古い配送などの dispatch_dropped、状態変化の finalize_state_transition、queue_publish、検証結果の verification_run_summary、bundle_download_failed です。

特に受付数を数える finalization_admitted は、共通の保存結果を観測する処理が、新しい none → pending を実際に保存した後だけ出します。固有フィールドは長さと形式を制限した finalization_id です。保存失敗、冪等な再要求、競合で負けた更新を新規受付へ数えません。ただしログの配送は重複し得るため、集計側でも同じ ID を除きます。

出力元によって JSON の包み方は違います。

Lambda の metric filter は $.message.* の正確なフィールドを見ます。ECS と台帳には外側の envelope がないので、検索でもこの違いを明示します。

相関キー

非同期処理では最初の HTTP 接続はすでに終わっています。そのため、ブラウザが付けた request ID を最後まで信頼して引き回すのではなく、保存した集計の識別子を使います。

非同期処理の主な照合キーは session_id_hash と finalization_id です。IP や保存接頭辞の照合が必要な場合も、実行時参照から解決した salt と用途ごとのドメイン分離を使います。salt の変更をまたいで同じハッシュになるとは仮定しません。

観測イベントと台帳の情報を絞る

観測のために、秘密や個別資源へのアクセス手掛かりを増やさないようにします。アプリの定型イベント、prover の要約、運用台帳では、出力元ごとの検証で次の値を除外します。

• 生の session ID、IP、選択肢と乱数、要求本文
• capability、Cookie、秘密値・設定値、署名鍵
• S3 bucket、完全な key / URI、署名付き URL、非公開のローカルパス
• アカウント ID、ARN、ダイジェスト付きイメージ URI
• 生の例外、AWS Cause、CloudWatch の state reason、ECS の stopped reason

共通 sanitizer は既知の秘密フィールドや値の形式を拒否し、深さとバイト数を制限します。ただし、任意の文章からすべての機密情報を見つける仕組みではありません。出力元が外部エラーを生で渡さず、定義済みの理由・分類へ変換することが必要です。AWS 管理ログや実行履歴に残る資源識別子はアクセスを制限した運用証拠として扱い、このイベントや台帳へコピーしません。

ブラウザの観測を受け取る

投票時の選択肢と乱数を使う確認の一部は、ブラウザ内で行います。サーバーだけでは、その確認結果まで含む画面の最終判定を観測できません。

判定後、ブラウザは capability 付きで POST /api/sessions/:sessionId/finalizations/:finalizationId/verification/observations へ、ブラウザ内の Cast チェック四つの状態だけを castChecks として送ります。セッションと集計の識別は URL から取り、本文の finalizationId、利用者が指定する総合判定、サーバー側チェック、秘密値、自由記述は受け入れません。

サーバーは現在の集計との一致、終了済み検証結果、保存済みシナリオ、サーバー側チェック、STH の実行時条件を確認し直します。一回の集計につき最初の一件だけを条件付きで記録し、同じ fingerprint の再送は冪等に扱います。異なる内容や、現在の集計と違う URL は conflict です。

記録後、総合状態とは独立に、必須チェックのうち success でない数を数え、verification_run_summary を可能なら出力します。この観測は画面判定の記録を補うもので、表示を書き換えたり、検証を再試行させたりする入口ではありません。

証拠レベルの読み分け

アラームを定義しただけでは通知できたとは言えません。確認結果は次の四つを分けます。

アラームの OK は、対象期間にしきい値超過が観測されなかったという意味です。利用の少ないデモでは、正常な操作も失敗した操作もなく OK のままであることがあります。ダッシュボード、適用後 Smoke、入口の確認、投票から検証までの実行、受入記録も、それぞれ確かめる事実が違います。

メトリクスと検出レイヤ

AWS が提供する測定値

Terraform は、一期間で検出する調査用アラーム、検証判定の矛盾を直接通知するアラーム、異常の持続を確認して通知するアラームを分けて定義します。

調査用アラームは通知アクションを持ちません。データ欠落は notBreaching として扱い、利用のない時間を障害に数えません。通知する五つは、一度の急増で反応せず、次の状態が続いたときに ALARM へ移ります。

ログの決まった値から測定する

アプリの判断は、ログの定義済みフィールドから測定値へ変換します。

session、finalization、request、IP、保存キーは dimension に使いません。秘密を守ると同時に、custom metric の種類が利用数に応じて無制限に増えることも防ぎます。

ダッシュボード

ダッシュボードは直近24時間の API 要求・5xx・p99 遅延、Lambda の errors / throttles、キューの経過時間・DLQ、集計の破棄・終了、検証失敗分類、通常は0である判定矛盾を並べます。さらに28日分の API 成功率と集計受付・終了の件数を表示します。

割合には必ず標本数を添えます。一回成功した100%と、多くの要求が成功した100%を同じ根拠にしないためです。p99 は調査用の表示で、遅延 SLO のアラームは定義していません。

時間内に終わった作業の割合を測る

28日間の API 指標は API Gateway Count を全件、Count - 5XXError を good、5XXError を bad とします。認証、capability、origin、レート制限、入力不正などの想定内4xxも non-5xx として good に含むため、これは投票完了率ではありません。Count = 0 は100%とせず insufficient_evidence です。

非同期集計は、保存成功後の finalization_admitted を起点に、同じ finalization_id の受付と最初の確定した終了遷移を重複排除します。完了期限は受付から75分。ログが遅れて届くための猶予を、その後に別の5分置きます。猶予は完了期限を80分へ延ばすものではありません。

この「good」は、集計値の正しさを意味しません。利用者の取消や不正な成果物の拒否を、基盤が正常に処理できた場合も含みます。想定内理由の定義は packages/diagnostics/src/canonicalEvents.ts、期限と集計は scripts/aws/lib/finalization-sli.ts に集約しています。

これらは調整中の測定値です。burn-rate アラームや error budget によるデプロイ制限は設けておらず、測定結果は Apply、rollback、復旧、キュー再投入の許可になりません。

通知の境界

検証の矛盾を知らせる専用アラームは、次の組み合わせだけを検出します。

outcome == fully_verified
AND independently_counted_failed_required_checks > 0

これは票の改ざんを検出したという通知ではありません。「必須チェックが満たされないのに完全検証と記録された」という判定処理自体の矛盾を疑う通知です。証拠の保全と調査を促し、判定は変更しません。

別の ops-actionable SNS topic には、上記の持続条件を持つ五つのアラームと、管理対象 CodePipeline の正確な FAILED イベントだけを送ります。アラームは EventBridge が対象名と ALARM 状態を確認して中継し、パイプライン失敗は別のイベント経路として扱います。

通知本文は、定義済みの環境、資源またはパイプライン、時刻、状態、dashboard、runbook ID と、パイプライン通知だけに必要な制限済み execution ID に絞ります。source SHA、ARN、アカウント、セッション、生の理由、秘密、成果物の場所は含めません。通知は調査を始めるもので、Apply、rollback、復旧、再投入、削除、ポインター変更を自動実行しません。

二つの通知経路のメール購読は独立した任意設定です。それぞれ専用の固定 SSM SecureString が契約どおり存在するときだけ構成し、topic、policy、宛先を共有しません。宛先は公開文書、追跡する tfvars、Terraform output、パイプライン証拠、ログに出しません。構成されたこと、受信者の確認、テスト通知の配送は経路ごとに別々に確認します。

運用台帳へ記録する

障害とデプロイの前後関係を長い期間で見るため、運用台帳へ四種類のイベントを記録します。EventBridge が必要項目の候補を取り出し、normalizer がイベントごとの正確なキー集合と値を再検証してから保存します。

共通項目は ts、event_type、env、resource_name、state です。追加する項目は次に限ります。

pipeline_execution_id は管理対象のパイプラインと対応する受入イベントの小文字 UUID、deployment_mode は normal / rollback、plan_disposition は changed / empty だけです。キーの欠落・追加や別名を許可しません。

元イベントや event ID、source SHA、repository / branch、アカウント、ARN、タスク・コンテナ・イメージの詳細、自由文の理由は台帳に残しません。例えばソースの正確な SHA を調べる場合は、台帳の deployment_id を受入証拠へ照合します。

EventBridge の配送は重複し得るため、この台帳も exactly-once の監査ログではありません。変更後の状態を見る query は pipeline_execution_id と定義済み状態で重複を除き、受入数、開始から受入まで、パイプライン終了、次の受入までの経過、再開・置換・再試行の手間を project 単位の代理指標として表示します。

保持期間

長期の前後関係を見る台帳と、詳しい診断ログでは寿命を分けます。開発環境と本番環境の保持期間は、Terraform で次のように管理します。

runtime のログ名は Terraform が管理する物理名とコンポーネントの接尾辞に合わせ、image-signature-verifier だけは stark-ballot-sim- を名前接頭辞に使います。CodeBuild のログは Bootstrap が管理します。

CloudTrail は App / Foundation / Bootstrap の稼働構成には含めず、アカウントや組織側で別途管理される場合があります。CloudFront のアクセスログも App では構成しません。これらを運用台帳と同じ記録として扱いません。

監視のためにセッション、票、非公開証拠の TTL やライフサイクルを延ばすことはありません。また、定期的な実証明 E2E を実行する CloudWatch Synthetics は構成していないため、監視画面だけで利用者の一連の操作が正常だったとは結論しません。

REST の metric dimension は ApiName/Stage、Count は SampleCount、 4XXError/5XXError は Sum を使います。source の変更と実際の metric 到着・ AWS 切り替えは別の証拠です。execution logging と data tracing は無効です。

検証する実装を、どう確かめるか

票の抜けを検出するはずのプログラムに、票の抜けを見逃すバグがあったらどうなるでしょうか。暗号の仕組みが正しくても、チェックの呼び忘れや画面の判定ミスで誤って Verified と表示してしまう可能性があります。

そこで、既知の失敗を再現するテスト、さまざまな入力を作って試すテスト、条件を満たす限り成り立つことを数学的に示すモデルを組み合わせています。

三つは異なる穴を探します。手書きテストは経験した失敗を確実に残せます。生成テストは人が思い付かなかった組み合わせを探せます。Lean は抽象モデルの条件を証明できますが、そのモデルと実際の TypeScript・Rust が対応するかは、さらにテストで照合する必要があります。

特に防ぎたいのは、証拠が不足しているのに成功を表示することと、秘密を含むファイルを配布してしまうことです。これらは一つの関数だけでは決まらないため、単体テストから画面を通すテストまで を使って確認します。

単体、結合、E2E テスト

S1 で一票を抜いたときに、集計関数が欠落を検出するだけでは十分ではありません。その情報が API を通ってブラウザに届き、画面が成功表示を止めるところまで確認する必要があります。

関数から画面まで

単体テストでは、入力コミットメントの計算、ジャーナルの読み取り、最終判定などを小さく切り出して確かめます。たとえば必須チェックを failed にしたときや、未知のチェックを混ぜたときに、完全成功を返さないことを検査します。

結合テストでは、部品をつないだときの取り違えを探します。投票と集計の状態遷移、API の要求・応答、保存した証拠の読み出し、Rust 検証サービスが返す状態などが対象です。公開 ZIP の許可リストも、生成側と配布側の両方で守られているかを確かめます。

CLI テストはブラウザを使わずに、セッション作成から投票、集計、検証までを実行します。Playwright の E2E テストは画面を操作し、同じ流れが利用者の操作として成立するかを確認します。アクセシビリティ検査には axe も使います。

軽い確認と、本物の証明を使う確認

日常の画面開発では mock の証明を使い、短時間で失敗を見つけます。一方、証明の入力・出力形式、Image ID、レシート検証の条件を変更した場合は、実際の production STARK 証明を通す必要があります。

開発用レシートが通ることは、production STARK 証明が検証できることの証拠にはなりません。テスト結果を見るときも、どの証明を使った実行かを区別します。

mock E2E でも、API を実際に通す

pnpm dev は Vite の開発サーバーとブラウザ内の mock API を使います。これに対して mock E2E は、production モードでビルドしたフロントエンドを静的 Hono サーバーから配信し、同じオリジンの API を呼び出します。画面だけでなく、HTTP と保存処理までつながる点が違います。

保存方式と証明の組は、実行プロファイルに定義します。

E2E の起動スクリプトがブラウザとサーバーのプロファイルを揃えます。AWS 向けの pnpm build:ci では target-aws-async を選び、出力に mock API やテスト用の Turnstile 回避処理が混入していないことも検査します。

テストを継続して発見する

Vitest のテストは対象実装のそばに置き、Playwright のテストは tests/e2e/ に置きます。各ワークスペースとリポジトリ用ツールが担当するテストを明示し、未発見や重複実行を検査します。ブラウザ環境の jsdom を使うのは web ワークスペースだけです。

各ワークスペースの test は狭い確認に使えますが、全体の単体・結合テストはルートの pnpm test:run で実行します。CI ではこれに画面テスト、Rust、形式化、公開ソースの検査を組み合わせます。

入力を生成して、性質を試す

64 票で通った包含証明が、63 票や 65 票でも正しく動くとは限りません。Merkle ツリーの枝分かれや、ビットをバイトに詰める処理には、大きさが一つ変わっただけで別の分岐を通る箇所があります。

Property-based Testing（PBT）は、こうした入力を多数生成し、「どの入力でも成り立ってほしい性質」を実装に対して試す方法です。TypeScript には fast-check、Rust には proptest を使います。失敗が見つかると、原因を追いやすい小さな入力へ縮めます。

順番を変えても、同じ入力を表すか

入力コミットメント は、同じ票の集合なら入力順を変えても同じ値になる設計です。PBT では票を生成して並べ替え、元の入力と計算結果を比較します。

正常な票だけでは、同じインデックスを持つ異常なレコードの並び方を確かめられません。そのため重複インデックスも生成し、追加の比較規則によって順序が一定になるかを試します。一方、選挙 ID、掲示板ルート、票数、各票のコミットメントや Merkle パスを変えた場合は、試したケースでハッシュが変わることを確認します。

このテストは実装の並べ替えやバイト列化の誤りを探します。SHA-256 の衝突困難性を証明するものではありません。

一つのビットが境界を越えるとき

自票が採用されたかを示すビットマップでは、7 と 8 の間でバイトが変わり、255 と 256 の間で 256 ビットの区画が変わります。境界の前後でビットを取り違えると、別の票の採用状況を表示してしまいます。

生成したビットマップから証明を作り、任意のインデックスで元のビットと一致するかを確かめます。区画の内容や証明パスを変更すれば拒否されること、論理的な票数を越えた位置を証明として使えないこと、末尾の埋め草が非ゼロなら拒否されることも試します。

固定ケースには 0、1、7、8、255、256、257、511、512、513、1025 ビットを残しています。生成テストに加えて、重要な境界は毎回必ず通すためです。

検査する性質と実装

ジャーナルでは、次の式と「採用済みの位置は提示済みでもある」という関係を検査します。

totalVotes = validVotes + rejectedRecords
invalidVotes = rejectedRecords
seenIndicesCount = validVotes + invalidPresentedSlots
validVotes + invalidPresentedSlots + missingSlots = treeSize
excludedSlots = missingSlots + invalidPresentedSlots

Rust 側の zkvm/methods/guest/src/property_tests.rs でも、入力の並べ替え、Merkle 証明、ビットマップ、ゲストの集計数と重複処理を検査します。Merkle ツリーやビットマップは比較用の実装と照合し、同じ誤りをそのまま期待値にしてしまう可能性を減らします。

生成テストから証明へ

PBT が確認できるのは、生成器が作り、実際に実行したケースです。実行時間を増やしても、生成器が作らない種類の入力は試せません。

同じ性質をすべてのモデル入力について述べたい場合は、Lean による形式化 を使います。そこで証明したモデルと実装の対応も、生成したテストケースを介して確かめます。

Lean による形式化

「完全成功と判定したなら、必須チェックはすべて成功している」。これは、いくつかのテストケースだけでなく、判定規則そのものについて確かめたい性質です。

Lean 4 では判定規則を数学的なモデルとして定義し、このような性質を証明します。証明の対象はそのモデルです。実際に動く TypeScript や Rust との対応は、モデルから作ったテストケースを使って別に確認します。

票が抜けていないことを式で表す

掲示板の各位置は、「有効票として採用された」「提示されたが採用されなかった」「提示されなかった」の三つに分かれます。ゲストプログラム の票数を、Lean では自然数のモデルで表します。

validVotes ≤ seenIndicesCount ≤ treeSize
missingSlots = treeSize - seenIndicesCount
invalidPresentedSlots = seenIndicesCount - validVotes
excludedSlots = missingSlots + invalidPresentedSlots

この関係から、excludedSlots = 0 なら、未提示の位置も、提示されたのに採用されなかった位置もなく、validVotes = seenIndicesCount = treeSize と示せます。B の一票を入力から抜いた S1 なら missingSlots が増えるので、この条件を満たせません。

ゲストのモデルは、単に数を置くだけでなく、票を一件ずつ処理します。範囲外・重複インデックスを拒否し、初めて現れた位置を提示済みにした後、選択肢、コミットメント、包含証明を調べ、採用した票を加算します。この処理順序の下で、見た位置が重複せず範囲内にあり、採用数が提示位置数を超えないことを証明します。

証明している性質

整数の証明では、treeSize と提示レコード数がそれぞれ 1,000,000 以下であることを仮定します。候補ごとの得票数も 1,000,000 以下になることは、その仮定から導かれる結論です。Rust の集計経路も入力上限を検査し、加算時のオーバーフローを拒否します。

モデルは formal/StarkBallotFormal/ の JournalCounts.lean、VerificationSummary.lean、InputCommitment.lean、Bitmap.lean、GuestModel.lean にあります。チェックの型などは Basic.lean が定義します。

実装との接続

モデルで正しいと示した規則と、実装した規則が違っていれば、モデルの証明だけではバグを防げません。そこで Lean から入力と期待結果の組を生成し、同じ入力を TypeScript・Rust に与えます。

flowchart TB
  M["Lean のモデル"] --> P["性質の証明"]
  M --> V["入力と期待結果を生成"]
  V --> T["TypeScript と照合"]
  V --> R["Rust と照合"]

生成するファイルは次の六つです。保存先は docs/formal/generated-vectors/ です。

生成元は formal/Scripts/EmitTestVectors.lean です。各ファイルの種類、フィールド、モデル上限と実装定数の一致、内容の SHA-256 を消費側で調べ、古い値や別種のデータを受け入れないようにしています。内容のハッシュは、自身のハッシュ欄を除き、キー順を再帰的に揃えた空白なし JSON から計算します。

この照合が確認するのは生成ケースの対応です。Rust ゲスト全体や画面描画全体を形式的に証明したことにはなりません。また、SHA-256、RISC Zero、コンパイラーや実行環境の正しさは、このモデルから導く結論ではなく前提です。

証明と生成物を点検する

docs/formal/formal-report.json に主張と前提を、formal-audit.json に定理のハッシュ、公理への依存、証明の点検結果、保存した生成ファイル全体のハッシュを記録します。ファイル全体のハッシュと、前節の JSON 内容のハッシュは計算対象が違います。

証明に未完成を許す sorry や、手書きのプロジェクト固有公理はありません。定理の依存は #print axioms で調べます。ビットを取り出す pack_bits_get_bit では有限の組み合わせを native_decide で計算しており、その生成された判定用公理も依存先として記録します。

Rust の生成ケース照合は Rust テストのワークフローで実行します。公開ソースを作る前にも Lean をビルドして pnpm formal:verify を実行するため、生成物が古い状態や照合に失敗する状態では公開処理を進められません。

API リファレンス

一票の操作を API でたどると、まずセッションを作り、そのセッションに投票し、集計を作成して検証します。ダウンロードする証拠も、どのセッションのどの集計に属するかを URL で指定します。

/api/sessions
  /:sessionId/votes
  /:sessionId/finalizations
    /current
    /:finalizationId/verification
    /:finalizationId/artifacts/bundle
    /:finalizationId/artifacts/report

セッション作成時に受け取る capability token を、それ以降の要求では X-Session-Capability ヘッダーに付けます。URL の識別子だけではデータを取得できません。集計 ID も現在のセッションと一致するかをサーバーが確認します。

実際の要求・応答とエラーは エンドポイント一覧 にまとめています。再読み込みや別タブで操作したときの状態の扱いは セッションの保存と継続 で説明します。

エンドポイント一覧

セッション作成から証拠の取得まで、ブラウザと CLI が呼び出す API の要求・応答をまとめます。すべてのパスは /api で始まります。

API 一覧

共通仕様

HEAD は GET 処理前に 404 で拒否します。

セッション capability

POST /api/sessions 以外の API は、次の組み合わせでセッションの所有者を特定します。

• sessionId: URL のパスパラメーター
• X-Session-Capability: 必須ヘッダー

集計 ID を含む URL では、finalizationId も現在の集計と照合します。

セッション認証の共通エラーは次のとおりです。

• SESSION_CAPABILITY_REQUIRED (401)
• SESSION_CAPABILITY_INVALID (401)
• SESSION_CAPABILITY_EXPIRED (401)
• SESSION_NOT_FOUND (404; セッションを読み取る API)

JSON の成功応答

JSON の成功応答は、結果を data、要求 ID を meta に入れます。ファイル取得 API は、そのファイルの本文を直接返します。

{
  "data": {},
  "meta": {
    "requestId": "request-id"
  }
}

スキーマにない追加フィールドは受理しません。掲示板のページ情報だけは、ページを指定した要求時に meta.page として追加されます。

JSON のエラー応答

公開 API の標準エラーは HTTP ステータス を本文に重複させず、次の形を使います。

{
  "error": {
    "code": "INVALID_REQUEST",
    "message": "Invalid request",
    "details": {
      "kind": "validation",
      "issues": {
        "formErrors": [],
        "fieldErrors": {}
      }
    }
  },
  "meta": {
    "requestId": "request-id"
  }
}

details は任意で、公開スキーマが許可する種類の詳細情報だけを返します。すべての API に共通し得る エラーは INVALID_REQUEST (400)、AWS 上のオリジン検証の SAME_ORIGIN_REQUIRED (403)、 ハンドラー内の予期しない失敗に対する INTERNAL_ERROR (500) です。

数値のクエリー・パスパラメーター

掲示板の offset、整合性証明の fromTreeSize / toTreeSize、ビットマップ証明の voteIndex は、0..Number.MAX_SAFE_INTEGER（9,007,199,254,740,991）の10進整数文字列を 受理します。0 自体を除く先頭ゼロ、符号、指数表記、小数、範囲超過は拒否し、丸めません。 掲示板の limit は先頭ゼロのない10進整数文字列で 1..1000 に限定します。

ボディサイズ、Turnstile、レート制限

JSON 本文 を持つ API は API_REQUEST_BODY_LIMIT_BYTES（既定 16 KiB）の対象で、超過時は PAYLOAD_TOO_LARGE (413) を返します。

Turnstile のトークンは本文の turnstileToken に置きます。AWS の main では、表で action を示した三つの API で検査を必須とします。AWS の develop では、運用者用の入口制限を通った要求に限り省略します。 ローカルの四つのプロファイルでは Turnstile を省略します。

セッションと投票

POST /api/sessions

新規セッションと capability token を発行します。

要求本文:

• turnstileToken（環境により必須）
• 本文省略時は空オブジェクトとして扱います

応答 (200) の data:

• sessionId
• electionId
• electionConfigHash
• logId
• capabilityToken

主な固有エラー:

• CAPTCHA_FAILED (403)
• GLOBAL_LIMIT_EXCEEDED (503)
• SESSION_LIMIT_EXCEEDED (503)

POST /api/sessions/:sessionId/votes

ユーザー投票を保存し、ボット63票の保存完了を待って投票レシートを返します。 同一セッションで同じ選択・乱数・コミットメントを再送すると、未完了のボット処理を再開し、 保存済みの票 ID・投票時刻・投票時ルートを返します。別の投票内容への変更は ALREADY_VOTED で拒否します。 集計開始後の同一投票の再送はレシートの取得だけを行い、票を追加しません。

通信切断や INTERNAL_ERROR (500) は、投票が未保存であることを意味しません。 同じ投票内容を保持して再試行してください。認証・レート制限・環境ごとの Turnstile 検証は再送にも適用されます。 この復旧は再試行を契機に行い、利用者の離脱後にバックグラウンドで完了させる保証ではありません。

要求本文:

• commitment: 32 バイトの16進文字列
• vote: A / B / C / D / E
• rand: 32 バイトの16進文字列
• turnstileToken（環境により必須）

応答 (200) の data:

• voteId
• commitment
• bulletinIndex
• bulletinRootAtCast
• castAtMs

主な固有エラー:

• CAPTCHA_FAILED (403)
• ALREADY_VOTED (400)
• SESSION_FINALIZED (400)
• INVALID_COMMITMENT (400)
• DUPLICATE_VOTE (409)
• GLOBAL_LIMIT_EXCEEDED (503)

GET /api/sessions/:sessionId/progress

投票進捗を返します。

応答 (200) の data:

• count
• total
• completed
• userVoted
• finalized
• distribution（任意。A-E のシミュレーション上の票数）
• distributionKind（任意。存在する場合は simulated）
• updatedAtMs（任意）
• animationSeed（任意）

Finalization API

Finalization resource

集計の作成・現在状態の取得・キャンセルは、同じ集計リソース形式で返します。共通フィールドは次のとおりです。

• finalizationId
• status: pending / running / succeeded / failed / timeout
• queuedAtMs
• runtimeDiagnostics
  • asyncMode: enabled / disabled
  • queue（任意または null）
  • progress（任意。実行中の段階から導出した進捗）

status ごとの追加フィールド:

succeeded の result は、証明に結び付く値、画面表示、投票者の証拠、ファイル取得の可否に分かれます。

• authority: imageId, journal と、任意の receipt, electionManifest, closeStatement
• presentation: 得票数、ビットマップルート、入力コミットメント、検証状態などの表示用データ
• voterEvidence: state=available または state=verification-gated
• artifactAvailability: bundle, report, includedBitmap, seenBitmap ごとの available / unavailable。ビットマップの available は、現在の集計に結び付く別ファイルが検査済みで保存されていることを示す

スキーマは、ジャーナルと表示用データに重複する値、Image ID、公開監査ファイル、レポートと状態、投票者の証拠、シナリオ、ファイル取得可否の整合性を検査します。表示の得票数と証明の得票数が違う場合は、改ざんシナリオの証拠として保持できます。ただし、シナリオや検証結果の説明もその差と一致している必要があります。

POST /api/sessions/:sessionId/finalizations

集計と証明生成を開始します。

要求本文:

• scenarioId: S0-S5
• turnstileToken（環境により必須）

応答:

• 200: 同期処理後の集計リソース
• 202: 受け付けた非同期集計のリソース

どちらも { data: FinalizationResource, meta } の形で返します。

主な固有エラー:

• CAPTCHA_FAILED (403)
• USER_NOT_VOTED (400)
• VOTING_NOT_COMPLETE (400)
• SESSION_ALREADY_FINALIZED (400)
• INVALID_IMAGE_ID (400)
• VERIFICATION_FAILED (400)
• ZKVM_RATE_LIMIT_EXCEEDED (429)
• GLOBAL_LIMIT_EXCEEDED (503)
• INVALID_FINALIZATION_ARTIFACT (500)

GET /api/sessions/:sessionId/finalizations/current

現在の保存済み集計を返します。まだ集計がない場合も成功応答となり、data は null です。存在する場合は上記の集計リソースを返します。

AWS の失敗・timeout の照合は閲覧に依存せず、定期的に起動する writer が担います。 未保存の失敗状態を GET の表示用に投影しません。

POST /api/sessions/:sessionId/finalizations/:finalizationId/cancel

URL のパスで指定した実行中の集計 をキャンセルします。

要求本文:

• reason（任意、最大 256 文字）
• 本文に executionId や finalizationId は置きません

応答 (200) はキャンセル後の集計リソース です。

主な固有エラー:

• ASYNC_FINALIZATION_DISABLED (404)
• FINALIZATION_NOT_CANCELLABLE (409)
• GLOBAL_LIMIT_EXCEEDED (503)

検証 API

GET /api/sessions/:sessionId/finalizations/:finalizationId/verification

指定した集計の検証データ を返します。

クエリー:

• include=journal（任意）

応答 (200) の data は availability=available です。

• finalizationId
• proofAuthority: 選挙の識別情報、掲示板ルート、Image ID、証明内の集計、ビットマップルート、入力コミットメントなど
• presentation: 表示集計、シナリオ、改ざん情報、表示可否の判定
• verifierResult: status と任意の公開 report
• verification: checks と steps
• voterEvidence: availability=available または availability=unavailable
• journal: representation=included の value、または representation=omitted

available の応答は、チェックと段階の構成、証明に結び付く値、レポートと状態、投票者の証拠、付属ジャーナル、シナリオ、表示判定の相互整合性も検査します。表示の得票数と証明の得票数の差は検証対象として保持できますが、その差を無視したチェック成功や Verified 表示を許すデータは受理しません。

検証データ全体の読み取り準備で unavailable / corrupt と判定された場合、現在の API は INTERNAL_ERROR (500) を返します。これは、取得できた応答の中で投票者の証拠だけが voterEvidence.availability=unavailable になる場合とは異なります。

主な固有エラー:

• SESSION_NOT_FINALIZED (400)
• USER_NOT_VOTED (400)
• INTERNAL_ERROR (500、検証データの読み取り準備に失敗した場合を含む)

POST /api/sessions/:sessionId/finalizations/:finalizationId/verification

実行中の応答は再送も 202、終端結果は 200 です。古い集計 ID への要求は 409 FINALIZATION_NOT_CURRENT で拒否します。受付成功だけでは Verified を意味しません。

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

• 要求本文: 追加フィールドを許さない空オブジェクト {}
• 応答 (200) の data:
  • verificationStatus
  • finalizationId
  • estimatedDurationMs
  • idempotent

主な固有エラー:

• SESSION_NOT_FINALIZED (400)
• ZKVM_RATE_LIMIT_EXCEEDED (429)
• GLOBAL_LIMIT_EXCEEDED (503)

POST /api/sessions/:sessionId/finalizations/:finalizationId/verification/observations

ブラウザで確認した Cast チェックの結果を観測記録として保存します。最終判定やサーバー側チェックの結果は、クライアントから指定できません。

要求本文の castChecks は次の 4 キーをすべて含み、他のキーを許しません。各値は success / failed / not_run のいずれかです。

• cast_receipt_present
• cast_choice_range
• cast_random_format
• cast_commitment_match

集計 ID は URL のパスで指定するため、本文には含めません。

応答 (200) の data.status:

• recorded: 初回記録
• idempotent: 同一内容の再送

主な固有エラー:

• VERIFICATION_OBSERVATION_CONFLICT (409; 異なる内容による再送)
• SESSION_NOT_FINALIZED (400)
• USER_NOT_VOTED (400)

Artifact 取得 API

二つの API とも X-Session-Capability を要求し、セッションと集計 ID を確認してからファイルを返します。S3 の保存先 URL や署名付き URL を返してそちらから取得させる方式ではありません。

GET /api/sessions/:sessionId/finalizations/:finalizationId/artifacts/bundle

秘密データを含まない配布対象 bundle.zip を返します。

• 200: ZIP のバイト列
• 206: Range で要求した部分のバイト列
• S3 に保存した大きい ZIP は範囲を指定した取得が必須

主な固有エラー:

• INVALID_BUNDLE_REFERENCE (400)
• BUNDLE_NOT_FOUND (404)
• BUNDLE_DOWNLOAD_FAILED (500)
• BUNDLE_REQUIRES_RANGE_DOWNLOAD (413)
• INVALID_RANGE (416)

GET /api/sessions/:sessionId/finalizations/:finalizationId/artifacts/report

認証付きで取得するレポート verification.json を JSON 本文として返します。これは配布対象 bundle.zip には 含まれません。

主な固有エラー:

• INVALID_BUNDLE_REFERENCE (400)
• REPORT_NOT_FOUND (404)
• REPORT_DOWNLOAD_FAILED (500)
• REPORT_DOWNLOAD_TOO_LARGE (413)

掲示板と証明 API

GET /api/sessions/:sessionId/bulletin

セッション所有者に、その掲示板の内容を返します。

クエリー:

• offset（任意、数値のクエリー・パスパラメーター の非負整数）
• limit（任意、1-1000）

応答 (200):

• data.commitments
• data.bulletinRoot
• data.treeSize
• data.generatedAtMs
• data.rootHistory（任意）
• meta.page.nextOffset, meta.page.hasMore（ページを指定した要求時）

主な固有エラー:

• INVALID_OFFSET (400)

そのほかの不正なクエリー は INVALID_REQUEST (400) です。

GET /api/sessions/:sessionId/bulletin/consistency-proof

RFC 6962 の整合性証明 を返します。

クエリー:

• fromTreeSize（必須、数値のクエリー・パスパラメーター の非負整数）
• toTreeSize（必須、同じ数値契約の非負整数）

応答 (200) の data:

• fromTreeSize
• toTreeSize
• rootAtFromTreeSize
• rootAtToTreeSize
• proofNodes
• oldSubtreeHashes / appendSubtreeHashes（任意）
• generatedAtMs

主な固有エラー:

• INVALID_SIZE (400)

GET /api/sessions/:sessionId/votes/:voteId/inclusion-proof

指定した投票の包含証明を返します。セッションの集計が完了している必要があり、証明の所有者と現在の集計との対応を検査します。

応答 (200) の data:

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

主な固有エラー:

• INVALID_VOTE_ID (400)
• VOTE_NOT_FOUND (404)
• VERIFICATION_FAILED (400; 掲示板の証明を取得できない)
• SESSION_NOT_FINALIZED (400)

GET /api/sessions/:sessionId/finalizations/current/bitmap-proofs/:kind/:voteIndex

成功した現在の集計に結び付くビットマップから、証明を作る材料を返します。

パスパラメーター:

• kind: included / seen
• voteIndex: 数値のクエリー・パスパラメーター の非負整数。セッションの利用者自身の投票位置に限定し、他の位置 は INVALID_BITMAP_PROOF_REQUEST (400) で拒否する

応答 (200) の data:

• leafChunk
• auditPath[]: hash, position (left / right)

If-None-Match を受理し、一致時は 304 を返します。

主な固有エラー:

• INVALID_BITMAP_PROOF_REQUEST (400)
• USER_NOT_VOTED (400)

GET /api/sessions/:sessionId/bulletin/sth

集計済みセッションの STH を返します。

クエリー:

• auditorId（任意、1-64 文字の英数字、.、_、-）

ブラウザからの要求は同一オリジンである必要があります。CLI やサーバー間の要求でもセッション capability は必須です。

応答 (200) の data.sth:

• sthDigest
• bulletinRoot
• treeSize
• timestamp
• logId

主な固有エラー:

• SESSION_NOT_FINALIZED (404)
• SAME_ORIGIN_REQUIRED (403; 同一オリジン 検証失敗)

GET /api/sessions/:sessionId/finalizations/current/input-commitment

現在の集計の入力コミットメントだけを返します。投票先や乱数などの秘密入力は含みません。

応答 (200) の data:

• inputCommitment

主な固有エラー:

• SESSION_NOT_FINALIZED (400)
• CT_PROOF_UNAVAILABLE (400)
• INTERNAL_ERROR (500; コミットメントの検査やハンドラー処理の失敗)

セッションの保存と継続

投票から証明の検証までは、複数の画面を移動します。再読み込みで投票時の情報を失うことも、別タブで作ったセッションの結果を今の票と取り違えることも避ける必要があります。

ブラウザとサーバーに残すもの

ブラウザとサーバーの対応は、URL の sessionId と X-Session-Capability で確認します。集計・検証のデータでは finalizationId も照合します。

保存されたブラウザの値も無条件には信用しません。admitStoredSessionData() が識別情報、期限、進行段階、投票の秘密情報とレシートの組、集計結果を検査します。未知のフィールドや必要な組の欠落、段階と集計状態の矛盾があれば拒否します。

読み取りで不正な値が見つかった場合は、starkBallotSession、stark-ballot-knowledge、starkBallotSessionLock を消去します。書き込みであれば保存せず Invalid browser session state として失敗します。情報の一部を削って、整合しているように見せる修復は行いません。

投票から検証へ進む条件

ブラウザの進行段階は次の三つです。集計の pending や succeeded とは別に、画面を継続するために保存します。

Result から Verify へ進むときは、検証を要求した時刻 verificationRequestedAt を保存し、必要なら STARK 検証を先に開始します。Verify は次の条件で継続を判断します。

1. 正しい finalizeResult と verificationRequestedAt が揃っていれば継続できる。
2. それらが揃わなくても、サーバーの STARK 検証が not_run 以外なら進める。
3. どちらも満たさなければ、検証を始める根拠がないため停止する。

ここで受け入れる finalizeResult は、現行のデータ形式と整合条件を満たす集計結果です。verifying 段階では必須であり、要求時刻は非負の整数だけを許します。

投票の応答を受け取れなかった場合

送信前に選択・乱数・コミットメントの組を保存します。応答が不明な間はその組を固定し、 再試行や再読み込みで新しい乱数を生成しません。同じ内容の再送でサーバーに残る票のレシートを回収し、 不足するボット票の保存を完了させます。Turnstile が必要な環境では、再試行用のトークンを改めて取得します。

サーバーは再送で票 ID や投票時刻を更新しません。異なる内容の再投票と、集計開始後の票の追記は拒否します。 DynamoDB の競合再試行でも保存時の票数上限を検査するため、同時にボット補完が走っても63票を超えて追記しません。

再読み込みと別タブ

同じオリジンのタブは localStorage を共有します。片方で新しいセッションを作ると、もう片方の画面に残る情報と保存値が食い違う可能性があります。タブごとのロックを比較し、古いセッションを見ている aggregate、result、verify、bot progress の画面は進行を止めます。

同じセッションへの二重操作はサーバーでも拒否します。投票済みなら ALREADY_VOTED、集計完了後の再集計なら SESSION_ALREADY_FINALIZED を返します。

クライアントの期限は、保存や活動時刻の更新でその段階に応じて延長します。Verify では 60 秒ごとにローカルの活動時刻を更新します。これはブラウザ内の更新であり、サーバーの期限を延長する heartbeat API ではありません。期限切れを検出すると clearSession() で保存状態を消去します。

サーバーでは状態ごとに記録する

サーバーは、セッションのすべてを一つの可変オブジェクトとして保存するのではなく、意味の異なる記録を分けます。

読み出す際は必要な記録を SessionReadModel にまとめられますが、その合成結果を保存用の正本にはしません。必要な記録の欠落や内部の集計 ID の不一致を見つけた場合は、値を作り足さずエラーとして扱います。

集計の状態は pending、running、succeeded、failed、timeout です。現在の状態と操作から、更新するか、同じ操作の再送か、古い操作として拒否するかを application 層で決めます。Mock・File・DynamoDB の各保存実装は、その判断をロックや条件付きトランザクションで反映します。

検証画面からの観測を保存する

検証シーケンスが完了すると、ブラウザは Cast チェックの観測を送ります。サーバーは最初の観測を finalizationId、内容の fingerprint、observedAt で記録し、同じ集計と同じ内容の再送を受け入れます。集計や内容が競合する送信は拒否します。

この記録は、利用者にどの状態が見えたかを調べ、観測イベントの重複を防ぐためのものです。送信や保存に失敗しても、証明、集計結果、検証結果、画面の判定は変更しません。

保存期間とセッション数の制限

クライアントの期限と、サーバーにデータが残る期間は別です。

DynamoDB では、作成時に SESSION_LIVE_TTL_SECONDS を使います。その後の投票や活動では、識別情報、投票状態、各票の期限を「現在の期限」と「現在時刻に live TTL を加えた値」の大きい方に揃え、条件付きトランザクションで更新します。競合や欠落で一部だけを更新することはありません。

集計状態の更新が適用されると、セッションの記録を VERIFICATION_ARTIFACT_TTL_SECONDS の期限へ移し、後の活動で短縮しません。検証結果、観測、保存・配送情報にもこの証拠用の TTL を使います。

一方、セッション作成上限を判定する際は、最終活動から 5 分以内かを調べます。この活動判定は DynamoDB の物理的な削除時刻とは別です。作成数が MAX_SESSIONS に達すると、POST /api/sessions は SESSION_LIMIT_EXCEEDED を返します。

チェック一覧

検証画面で示す四段階は、22 個のチェックで構成します。結果や実装で見かけた ID を調べられるよう、ここに全定義と個別の判定条件をまとめます。全体の表示は Verified の表示条件で決まります。

チェックの属性

チェックの定義には ID、所属段階、証拠種別、重要度、他のチェックから派生する場合の元 ID があります。結果には、その時点の評価状態を付けます。

証拠種別

定義が持つのは local / public / zk です。demo は実行時の証拠を示し、本番用 STARK 証明の成功には数えません。

重要度

required は必須確認です。optional は補助確認ですが、その失敗・未実行があれば最終表示は Warning になります。recorded_sth_third_party はソース設定時に必須へ昇格します。

全チェック早見表

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

ブラウザは、保存した electionId / myVote / myRand と、検証応答の voterEvidence が available の場合に得られる voteReceipt を使います。API 上の Cast は not_run で、ブラウザの計算後に置き換えます。

cast_receipt_present

voteReceipt に voteId と commitment が存在することを確認します。このチェック単体では UUID や hex の形式まで検査しません。

cast_choice_range

保存した選択肢が A〜E のいずれかであることを確認します。範囲外は failed です。

cast_random_format

乱数が 32 バイト、すなわち 64 文字の hex であることを確認します。0x プレフィックスは正規化して扱います。

cast_commitment_match

選挙 ID、選択肢、乱数から投票コミットメントを再計算し、レシートと照合します。

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

包含証明と整合性証明は、投票時の voteReceipt と userVote.proof を使います。まず leafIndex、treeSize、bulletinRootAtCast がレシートと整合することを確認します。完全な投票時証跡が取得できない場合は not_run です。部分的に壊れた証跡の受理を意味するものではありません。

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 の Merkle パスから投票時のルートを再計算し、レシートの bulletinRootAtCast と照合します。証明の treeSize は voteReceipt.bulletinIndex + 1 と一致しなければなりません。

recorded_consistency_proof

投票時と集計時のツリーサイズ・ルートが期待値と一致し、RFC 6962 の整合性証明が成立することを確認します。投票時の証明の treeSize は包含証明と同じ条件です。

証拠取得が unavailable なら not_run、malformed または transport_failed なら failed です。取得と形式検査を行った後の証拠を評価器へ渡すので、評価器自身は URL や認証情報を扱いません。

recorded_sth_third_party

設定したソースから取得した比較可能な STH 応答について、matchingSources >= minMatches（既定値 2）と、比較対象間の全会一致を要求します。単なる多数決ではありません。

各応答の sthDigest をジャーナルの期待値と照合します。応答に bulletinRoot / treeSize がある場合は、それも照合します。設定済みソースの取得失敗、不正な応答、利用不能が一つでもあれば成功にしません。未設定なら not_run、設定した場合は必須確認です。

外部 HTTPS 応答は sthDigest を必須とする flat object で、任意キーは bulletinRoot / treeSize / timestamp / logId だけです。指定された値は形式を検査し、未知キー、別名キー、API の wrapper を受理しません。同一オリジンの API テンプレートと外部 HTTPS の取得形式・独立性の違いは STH ダイジェストに示します。

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

公開入力は、形式検査を通した後、評価に必要な要約へ変換します。以下の「公開入力」は、この内部の確認済み要約を指します。検証 API がそのまま配布する値ではありません。

counted_input_sanity

公開入力があり、スキーマ検査に成功し、treeSize が正の整数、votesCount <= treeSize、bulletinRoot がゼロではない 32 バイト hex であることを要求します。

counted_unique_indices

公開入力の各票のインデックスが重複していないことを確認します。入力が取得できなければ not_run です。

counted_unique_commitments

公開入力の各コミットメントが重複していないことを確認します。入力が取得できなければ not_run です。

counted_tally_consistent

表示する tally.counts と verifiedTally を候補ごとに比較し、後者の合計が表示側の tally.totalVotes と一致することを確認します。ジャーナルが存在して totalVotes = 0 なら、一票も処理していないため failed です。

表示集計を持たない評価入力では、ジャーナル内の verifiedTally の合計と validVotes の整合を確認します。必要な値もなければ not_run です。この内部の合計確認だけで、表示集計との比較を済ませたことにはなりません。正式な公開リソースの成功条件は、表示と証明側の両方を照合します。

counted_missing_indices_zero

除外スロット数がゼロであることを確認します。ジャーナルがある場合は、その excludedSlots を使い、先に excludedSlots / missingSlots / invalidPresentedSlots / validVotes が非負整数であることも検査します。

ジャーナルを省略した評価入力では、明示的な excludedSlots、次に missingSlots + invalidPresentedSlots の順で値を求めます。解決できないときはゼロを仮定せず not_run にします。正の除外数や異常なジャーナルカウントは、STARK の待機状態より先に失敗と判定します。

rejectedRecords はスロットの除外数を求める計算には使いません。ただし、公開リソースの Verified 条件では、この値もゼロを要求します。現行ジャーナルの形式は厳密に検査し、別のフィールド名から修復して評価することはありません。

counted_expected_vs_tree_size

totalExpected と treeSize の一致を確認します。明示的に渡された値を優先し、なければジャーナルの対応値を使います。必要な値がない、または整数でなければ not_run、不一致なら failed です。

counted_election_manifest_consistent

マニフェストから electionConfigHash を再計算し、宣言値と照合します。そのうえで electionId と設定ハッシュが、セッション、公開入力、ジャーナルの対応値と矛盾しないことを確認します。マニフェストがなければ not_run です。

counted_close_statement_consistent

締切ステートメントから sthDigest を再計算して宣言値と照合し、timestamp が公開入力と一致することを確認します。logId / treeSize / bulletinRoot / sthDigest も検証入力やジャーナルと照合します。必要なステートメントや公開入力の時刻がなければ not_run、再計算できない値や不一致は failed です。

counted_my_vote_included

includedBitmapRoot に対する Merkle 証明を検証し、自票のインデックスのビットが 1 であることを確認します。証明に必要なレシート、ルート、ツリーサイズ、証明材料がなければ not_run です。

seenBitmapRoot と対応する証明も利用できれば、「提示されて計上された」「提示されたが計上されなかった」「提示されなかった」を区別して説明します。証明を取得する API は GET /api/sessions/:sessionId/finalizations/current/bitmap-proofs/:kind/:voteIndex で、kind は included または seen、インデックスは当該セッションのユーザー票に限定します。

counted_input_commitment_match

公開入力から再計算した値を、ジャーナルの inputCommitment と比較します。ジャーナルが省略された評価入力では、別途渡された同名の値を使います。入力、比較値、再計算値がなければ not_run です。対象フィールドと正準エンコーディングが一致することを確認し、JSON 全体のハッシュとして扱いません。

STARK Verification（2 チェック）

stark_image_id_match

STARK の成功後、期待 Image ID、検証サービスが確認したレシートの Image ID、ホストの主張値が整合することを確認します。ホストの JSON に書かれた値だけを、検証済み ID とみなしません。レポートに必要な値がない場合を含む条件は Image IDに示します。

stark_receipt_verify

Rust 検証サービスが Receipt::verify(expectedImageId) を実行した結果を反映します。dev_mode の正規化と最終表示の制限は STARK 検証のゲーティングに従います。

STARK 結果への依存

次の六つは、STARK が未開始・実行中・失敗なら、個別の照合に先立ってそれぞれ not_run・pending・failed になります。

• counted_tally_consistent
• counted_expected_vs_tree_size
• counted_election_manifest_consistent
• counted_close_statement_consistent
• counted_my_vote_included
• counted_input_commitment_match

counted_missing_indices_zero も STARK に依存しますが、異常カウントや正の除外数が分かれば先に failed にします。公開入力の形式と二つの重複確認は、STARK の完了前に評価できます。

チェックステータスの解決

各チェックは独立した永続状態機械ではなく、その時点の証拠から再評価する結果です。証拠や STARK の状態が更新されると、not_run / pending から success / failed へ直接変わることがあります。

用語集

本文で使う言葉を、証拠や処理との関係から引けるようにまとめています。

暗号プリミティブ

コミットメント（総称）

内容を決めた後で取り替えていないかを確かめるための値です。本書では、一票の選択肢と乱数に結び付く「投票コミットメント」と、集計へ渡す公開入力の一部に結び付く「入力コミットメント」を区別します。

投票コミットメント（Vote Commitment）

選挙 ID、選択肢、乱数を定めた形式で SHA-256 に入力して得る値です。公開された値から投票先を推測しにくくし、後から別の選択肢へ開き直すことを困難にします。このデモのサーバーは投票先と乱数を受け取ります。符号化と性質。

Merkle ルート（Bulletin Root）

掲示板上のコミットメントを Merkle ツリーにまとめた、頂点のハッシュです。票の内容や順序を変えると通常は値が変わるため、保持したルートとの比較で変更を検出できます。

Merkle パス（Audit Path）

葉からルートを計算し直すために必要な、兄弟ノードのハッシュ列です。全票を受け取らずに自票の包含を確かめるために使います。

包含証明（Inclusion Proof）

ある位置の票が、指定したルートとツリーサイズの掲示板に含まれることを確かめる証拠です。位置と Merkle パスからルートを再計算します。掲示板の証明。

整合性証明（Consistency Proof）

古いツリーが新しいツリーの先頭部分として残っていることを確かめる証拠です。比較する二つのルートとサイズを基準に、追記以外の変更がないかを検査します。RFC 6962 の整合性証明。

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

ゲストへ渡した公開入力のうち、選挙 ID、掲示板のルートとサイズ、期待数、票数、各票の位置・コミットメント・Merkle パスをハッシュした値です。public-input.json 全体のハッシュではありません。正確な対象フィールド。

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

ログ ID、ツリーサイズ、時刻、ルートをハッシュした値です。比較対象が同じ掲示板の状態を指しているかを調べます。このデモのダイジェスト照合は STH の署名検証ではありません。照合方法。

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

各位置が集計に採用されたかを表すビットマップの Merkle ルートです。位置に対応するビットが 1 かを、区画と Merkle 証明で確かめます。ビットマップ。

提示ビットマップルート（Seen Bitmap Root）

ゲストに提示された範囲内の位置を表すビットマップの Merkle ルートです。採用済みビットマップと比べて、未提示と提示後の不採用を区別します。ビットマップ。

正準エンコーディング（Canonical Encoding）

フィールドの順序、整数の幅、バイト順、並べ替え規則などを固定したバイト列表現です。同じ意味の入力から同じハッシュを計算するために使います。

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

ハッシュするデータの用途を区別する先頭の値です。投票コミットメントと入力コミットメント、Merkle ツリーの葉と内部ノードなどが、同じバイト列の意味を取り違えないようにします。

投票レシート（Vote Receipt）

投票を受理したサーバーが返す記録です。voteId、commitment、bulletinIndex、bulletinRootAtCast、castAtMs を含みます。投票時の選択肢と乱数から再計算した値を、このコミットメントと照合します。計算の証明を含む STARK レシートとは別です。

STARK 証明

STARK（Scalable Transparent ARgument of Knowledge）

計算が定めた規則に従ったことを検証する暗号証明の方式です。このデモでは RISC Zero の STARK 証明を使い、秘密の初期設定値を必要とする trusted setup は行いません。zkVM の基礎。

RISC Zero zkVM

RISC-V のプログラムを実行し、その実行に対する証明を作る仮想マシンです。このデモのゲストは Rust で投票の検査・集計を実装しています。構成。

レシート（Receipt）

zkVM の計算の証明と公開出力を運ぶオブジェクトです。別途選んだ期待 Image ID を Receipt::verify に渡して検証します。

ジャーナル（Journal）

ゲストが公開する出力です。得票数、位置の欠落・不採用数、入力コミットメント、ビットマップルートなどを含み、レシートの証明に結び付きます。別ファイルの journal.json は、検証済みレシートから取り出した値と照合して使います。フィールドの定義。

Image ID

実行するゲストのメモリーイメージを識別する 256 ビットの値です。検証者が期待値を指定し、別のプログラムの証明を受け入れないようにします。コンテナイメージのダイジェストとは別です。選択方法。

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

zkVM 内で投票を検査・集計し、ジャーナルを出力するプログラムです。証明は、この指定プログラムの実行と出力を結び付けます。処理順序。

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

zkVM の外で入力を読み、ゲスト実行と証明生成を進め、レシートなどのファイルを書き出すプログラムです。証明生成。

検証サービス（Verifier Service）

STARK レシートを検証する Rust バイナリ verifier-service です。期待 Image ID とレシートから結果を計算し、レポートを出力します。終了コードとレポート。

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

RISC Zero の開発モードで作る、production STARK の暗号学的保証を持たないレシートです。開発モードを扱える検証ビルドは dev_mode として区別し、production feature のビルドは開発モードを無効にします。検証サービス。

ジャーナル契約（Journal Contract）

ゲストが出すフィールドと意味を定める仕様です。現行は methodVersion=14。バージョンだけでプログラムを信用せず、レシート検証では期待 Image ID も指定します。

レシートラッパー JSON

ホストが出力する { "receipt": ..., "image_id": "0x..." } という形式です。ファイル名は receipt.json。添えられた image_id は、検証者が別途選ぶ期待 Image ID の代わりにはなりません。

検証パイプライン

fail-closed

証拠の不足やデータの不整合を、推測で成功として扱わない方針です。状況に応じて待機、証拠不足、失敗を表示し、必要な条件が満たされるまで Verified にしません。表示条件。

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

意図した票が記録され、その記録が集計されたことを確かめられる投票の考え方です。このデモの画面は Cast をブラウザで確認し、その他のチェックはサーバーの報告を使います。実行場所と信頼関係。

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

手元の選択肢と乱数から投票コミットメントを作り直し、投票レシートと一致するかをブラウザで確かめる段階です。第1段階。

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

投票時の包含証明と、その後の整合性証明を使い、送った票が掲示板に残っているかを確かめる段階です。第2段階。

cast-time 証跡（Cast-Time CT Artifact）

投票受理時のレシートと、その時点の掲示板ルートに対する包含証明です。最終掲示板への包含とは確認する時点が違います。証拠の取得。

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

全位置の採用、自票の採用、公開入力と証明の一致、表示集計と証明の出力の一致などを確かめる段階です。第3段階。

STARK 検証（STARK Verification）

期待するゲストの実行に、レシート内の公開出力が結び付くことを暗号学的に確かめる段階です。この成功だけで四段階全体の成功にはなりません。第4段階。

検証チェック（Verification Check）

検証の中で個別に結果を持つ項目です。ID、段階、証拠種別、必須・補助の区分を定義します。全22チェック。

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

チェック結果、証拠、実行状態を合わせて最終表示を決める規則です。必須成功に加えて、全体の整合条件と補助チェックの状態も評価します。判定の優先順位。

公開監査アーティファクト

選挙設定の election-manifest.json と、締切時点の掲示板を示す close-statement.json です。公開入力・ジャーナルと照合します。バンドル構造。

締切ステートメント（close-statement.json）

集計締切時点のログ ID、ツリーサイズ、ルート、時刻、STH ダイジェストをまとめたファイルです。本文では「締切宣言」とも呼びます。照合条件。

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

投票の秘密を含めず、第三者へ渡せるようにした証拠ファイルです。「公開可能」は内容の分類であり、ダウンロード時にはセッション認証が必要です。公開境界。

配布対象アーカイブ（bundle.zip）

公開を許可した証拠だけをまとめた ZIP です。秘密入力、検証レポート、完全なビットマップは同梱しません。同期・非同期の構成。

保護された検証レポート（verification.json）

検証サービスの結果を記録したファイルです。ZIP とは別に、セッション認証が必要な report API から取得します。取得 API。

無認証公開

セッションの鍵などを提示せず取得できる状態です。公開可能な bundle.zip も、通常の取得 API は認証を要求します。

zkGate

STARK の検証状態に応じて、一部の Counted チェックを待機・失敗・デモ用評価へ切り替える処理です。対象と優先順位。

証拠種別

チェックの入力元の分類です。local は投票者の手元の情報、public は公開可能な検証データ、zk はゲストの公開出力、demo は開発用レシートを許した際のデモ用評価を示します。チェック一覧。

重要度（Criticality）

チェックを required（必須）と optional（補助）に分ける属性です。補助でも失敗や未実行があれば完全成功ではなく制限付きになり、実行中なら待機します。第三者 STH のチェックは、照合先の設定によって必須になります。表示条件。

掲示板と透明性

掲示板（Public Bulletin Board）

投票コミットメントを順に追記するログです。Merkle ルートと証明を使って、特定の記録の包含や追記前後の関係を検査できます。掲示板。

RFC 6962

Certificate Transparency の仕様です。このデモは、その Merkle ツリーのハッシュ規則と包含・整合性証明を利用します。CT の署名や監視の仕組み全体を実装したという意味ではありません。利用している規則。

STH（Signed Tree Head）

ログ ID、ツリーサイズ、時刻、ルートで表す掲示板の状態です。名前は CT に由来しますが、このデモはそれらのダイジェストを比較し、STH 署名そのものは検証しません。STH ダイジェスト。

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

相手によって異なる掲示板を見せる攻撃です。それぞれの掲示板の中だけで包含・整合性を調べても見逃し得るため、独立した観測先と状態を照合します。照合の条件。

ルート履歴（Root History）

追記に伴う掲示板のルート、サイズ、時刻の記録です。投票時から最終時点までの追記関係を検証するために使います。

改ざんシナリオ

改ざんシナリオ（Tamper Scenario）

検出の仕組みを観察するための操作です。S0 は正常、S1・S3・S5 は一票の入力除外、S2・S4 は表示集計の変更を行います。シナリオ一覧。

投票除外（Vote Exclusion）

掲示板上の票を集計入力へ渡さないなど、集計に採用しないことです。未提示や不採用の位置は excludedSlots に残ります。

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

表示用の得票数だけを、証明内の集計と違う値に変える操作です。入力と証明が正常でも、counted_tally_consistent で不一致を検出します。

excludedSlots

集計に採用されなかった掲示板上の位置数です。missingSlots + invalidPresentedSlots に等しく、ゼロでなければ Verified にはできません。拒否レコード数 rejectedRecords とは異なります。位置とレコード。

インフラストラクチャ

ECS Fargate

サーバーを直接管理せずコンテナを実行する AWS のサービスです。このデモの重い証明生成を担当します。実行資源。

Step Functions

処理の順序、待機、失敗時の分岐を管理する AWS のサービスです。署名検証、プローバー起動、結果の通知などをつなぎます。非同期処理。

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

集計要求に受付結果を返した後、別のジョブで証明を生成する方式です。ブラウザは進捗を問い合わせて完了を待ちます。非同期プローバー。

同期証明モード（Sync Proving）

要求を処理するローカルプロセスからホストを起動し、結果を待つ方式です。使うレシートの種類は実行プロファイルによって異なります。

Prover semaphore

同時に証明を生成するジョブ数を制限する仕組みです。DynamoDB に利用中の枠を記録し、通常は Step Functions が解放します。残った枠は専用の清掃処理が終了確認後に回収します。非同期プローバー。

Quiesced phase

DynamoDB の復旧・切替の途中で、新規セッションと非同期キューの処理を停止する状態です。復旧時の段階。

Develop operator gate

開発環境のページと API への入口を制限する CloudFront の署名付き Cookie です。環境へのアクセスと、個々のセッションへの capability 認証を別々に確認します。入口の認証。

Saved-plan lane

Terraform が作成して保存した計画を承認し、その同じ計画を適用する変更経路です。通常変更とロールバックで承認条件を定めます。計画と承認。

Release authority

どのビルド済みイメージやアプリ成果物を採用できるかを決める、検査済みの記録と、それを選ぶポインターです。イメージの選択と受入記録を参照できます。

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

起動するコンテナのダイジェストに対し、許可した署名元の署名が有効かを確認する処理です。ゲストの Image ID とレシートの検証とは別に行います。イメージ署名。

証明バンドル（Proof Bundle）

証明生成・検証に関わるファイル群を指す語です。秘密入力や保護対象のファイルも含めて述べるときに使います。配布する ZIP を指す場合は bundle.zip と明記します。ファイルの配置。

隣接オブジェクト（Sibling Object）

S3 で ZIP と同じ集計用の接頭辞の下に保存する、ZIP 外のファイルです。完全なビットマップや検証レポートなどを保存します。保存構造。

セッションと API

セッション（Session）

作成から投票、集計、検証までの一連の操作を管理する単位です。sessionId で識別し、capability token でアクセスを保護します。保存と継続。

選挙（Election）

候補や期待票数などの設定に結び付く投票の単位です。electionId を投票コミットメントにも含め、別の選挙の票と取り違えないようにします。

集計確定（Finalization）

票を集めた後、集計入力を作り、ゲストを実行して証拠を生成し、結果を保存する作業です。STARK レシートを検証する作業とは別の状態を持ちます。

X-Session-Capability

セッションへのアクセス権を示す署名付きトークンを送る HTTP ヘッダーです。トークンは POST /api/sessions の成功応答で受け取ります。API の共通仕様。

capability 保護 API

セッションの鍵を X-Session-Capability で提示して呼び出す API です。URL のセッション ID だけでは取得できません。API の共通仕様。

Turnstile

自動化された不正アクセスを抑えるための Cloudflare の仕組みです。セッション作成、投票、集計要求でトークンを使い、必須条件は実行環境の設定に従います。要求の条件。

定数

ハッシュに使うタグとバイト列は、投票コミットメント、入力コミットメント、掲示板で定義します。

参考文献

本システムの設計に関連する主要文献を掲載します。

[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, 2025（First Online 2024）. https://doi.org/10.1007/978-3-031-69231-4_4

STARK 証明を投票集計の検証に適用する設計根拠を示した論文です。 本システムの Counted-as-Recorded 段階における zkVM 証明設計と関連が深い文献です。

[3] V. Farzaliyev, J. Willemson. “End-To-End Verifiable Internet Voting with Partially Private Bulletin Boards,” in Electronic Voting: E-Vote-ID 2025, LNCS, vol. 16028, Springer, 2026（First Online 2025）. https://doi.org/10.1007/978-3-032-05036-6_5

[2] の研究を拡張し、STARK ベースの E2E 検証可能投票において Cast-as-Intended 検証と掲示板のプライバシー設計を統合した論文です。 本システムの掲示板構成と検証パイプライン設計に関連するテーマを扱っています。

[4] B. Laurie, A. Langley, E. Kasper. “Certificate Transparency,” RFC 6962, IETF, 2013. https://datatracker.ietf.org/doc/html/rfc6962

追記専用 Merkle ツリーの包含証明と整合性証明を定義した Experimental RFC です（現在は RFC 9162 により置き換えられています）。 本システムの掲示板は、この仕様のハッシュ規則（0x00 リーフ / 0x01 ノード）と証明アルゴリズムに基づく CT スタイル実装を採用しています。

ライセンス

STARK Ballot Simulator は Apache License 2.0 の条件で提供されています。

• SPDX: Apache-2.0
• ライセンス本文: 公開リポジトリの LICENSE

依存ソフトウェアには、それぞれのパッケージ定義に記載されたライセンスが適用されます。 第三者ライセンス情報は公開リポジトリの THIRD_PARTY_NOTICES.md と、生成済みメタデータ docs/licenses/ にまとめています。