プログラムに脆弱性があることをゼロ知識証明で示せるようにする、という研究。

https://dl.acm.org/doi/10.1145/3747589

LLVM中間コードやRISC-Vコードを元に、プログラムがある入力に対してある性質(未参照メモリの参照や、機密情報が公開された領域に置かれていることなど)を満たすことをゼロ知識証明で証明する。

まず、実行トレースのウィットネスを検証する検証器を作る(これは脆弱性を引き起す入力無しで作れるので、検証者側で作れる)。

次に、脆弱性を引き起す入力を使って、証明者が実行トレースのウィットネスを作成する。

そして検証者は実行トレースのウィットネスを検証する。

LLVM中間コードやRISC-VコードはMicroRAMという中間コードに変換してからゼロ知識証明の回路に変換する。

最適化のためにシンボリック実行などを活用する。

ゼロ知識証明でメモリ安全性侵害、情報流出、インタラクティブなネットワーク攻撃、DoSなどを表す方法を工夫している