知識証明プロトコルSTARKの証明・検証ライブラリを試してみる

Table of Contents

概要

プログラミング言語Cairo[1]で証明したいプログラムを書いて、実行履歴(trace)を作成した後は、その実行履歴を使ってプログラムの証明・検証を行う必要があります。
証明・検証のためのライブラリ・ツールにはいくつかあり、依存や参照関係が存在します。
この記事では主要なライブラリ・ツールの関係や、今使うべきツールについて説明します。

ライブラリ・ツールの一覧

名前	URL	概要	言語
ministark	https://github.com/andrewmilson/ministark	winterfellを参考に作られたライブラリ	Rust
ethSTARK	https://github.com/starkware-libs/ethSTARK	STARKの論文を書いたチームによるライブラリ。セキュリティが80bitに限定されている	C++
winterfell	https://github.com/facebook/winterfell	cairo言語とは異なり、Rustで直接STARKの計算の内部状態をいじることができるライブラリ	Rust
sandstorm	https://github.com/andrewmilson/sandstorm	内部的にはministarkを使っているツール。cairoからstarkwareのライブラリを使って作られたプログラムに対しても、証明と検証が可能。	Rust
stone	https://github.com/starkware-libs/stone-prover	内部的にはethSTARKを使っているツール。	C++
giza	https://github.com/maxgillett/giza	内部的にはwinterfellを使っているツール	Rust

説明

STARKの証明・検証を行うライブラリ（ministark, ethSTARK, winterfell）と、それを内部的に使った証明・検証CLIのインターフェース提供や互換性を担保するツール(sandstorm, stone, giza)に大きく分けられます。

Cairo言語を実行した結果として得られる実行履歴ファイルを入力する点では、全てのツールが同じです。しかし、例えばministarkで作った証明をethSTARKに持ち込んでもそのままでは使えないため、ministarkで作った証明はministarkで検証する必要があります。

また、それぞれのライブラリにおいてCairo言語の利用は必須ではなく、直接ライブラリで使用している言語を使ってプログラムを書くことも可能です。例として [2]のbrainfuck実装はcairoを使わず直接Rustで書かれています。

ツールを使ったCairoプログラムの証明実行手順

Cairoでプログラムを書く。
cairo-compileコマンドでCairo言語によるプログラムをjson形式のプログラムにコンパイルする。
cairo-runコマンドでjson形式のプログラムを入力とともに実行し、実行履歴ファイル(trace)を作成する。また、このとき同時に公開入力(public input)と非公開入力(private input)も生成する。
実行履歴ファイルを始めとする生成されたファイルを sandstorm, giza, stone などのCLIツールに入力として渡す。CLIは証明ファイルを生成する。
証明ファイル、公開入力(※)、json形式プログラムをCLIへの入力として渡す。CLIは証明が正しいかどうかを検証する。

※: (5)で使用する「公開入力値の入ったjson」は(3)の cairo-run コマンドを実行しなくても取り出せる形式になっている必要がある。しかしながら、cairo v0系において「公開入力」はループ内部等でも記述されているので、 cairo-run を実行せずに「公開入力値の入ったjson」を取り出すことが現時点では不可能であり、検証者側が効率的にプログラム入力まで検証することができないという問題がある。

セキュリティ

secp256k1のセキュリティパラメータ強度が128ビットであることから、ビットコインに関連したソフトウェアのセキュリティパラメータも128ビットを基準とすることが多いです。ministark, ethSTARK, winterfell はそれぞれ異なるセキュリティパラメータの基準を持っています。

ethSTARK

[3]にあるとおり、最大80ビットのセキュリティをサポートしています。

winterfell

[7] にあるとおり、当初は ethSTARKライブラリのドキュメントに沿って予想されるセキュリティパラメータを有限体のサイズやハッシュ関数の強度から計算していたようです。しかし、その後、 [5][6]のように基準がethSTARKの元論文の値になるように変更されています。

ministark

[4]にあるとおり、winterfellのセキュリティパラメータと同様の基準です。証明で使われる有限体のサイズやハッシュ関数の強度に依存しています。
sandstormのverifyコマンドでは --required-security-bits で必要なセキュリティ強度を指定することができます。
なお sandstormのデフォルトの設定では256ビットの強度があるハッシュ関数のblake2sとkeccak256を使っているようですが、一部をマスクして意図的に強度を落としているように見えます。
これについては再帰STARKの中で大きすぎるハッシュ値の計算が大変だからか、テスト用だからなのか不明ですが、ソース中でN_UNMASKED_BYTESを32バイト分に設定すれば回避できるようにも見えます。

検証用プログラム・入力値の指定

ツールを使って証明の検証を実際に行うにあたっては、どのプログラムに対して、どんな入力が与えられたかを明確にした上で検証可能かを判断する必要があります。
しかし、現状この機能を持っているのは sandstormのみに限られるようです。stone, gizaでは検証の際に入力をCLIから指定して実行することができません。

その他

[8]のようなJavaScript実装もあるようですが、こちらはCairoが使えなさそうなので未検証です。

結論

検証者が公開入力(public input)をcairoから自分でコンパイルしたプログラムに対して与えるような一般的なユースケースでは、ministark-sandstormを使うのが現状でのベストな選択肢と思われます。ただし、公開入力の検証は現時点ではできないことに注意が必要です([9]を参照)。
いずれのツールも目下開発中であり、機能追加やアップデートによって今後の状況は変わる可能性が大きいです。