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 を使い、この数学的検証を独自に実装しません。