CirC: Compiler infrastructure for proof systems, software verification, and more

@misc{alex2020circ,
      author = {Alex Ozdemir and Fraser Brown and Riad S.  Wahby},
      title = {CirC: Compiler infrastructure for proof systems, software verification, and more},
      howpublished = {Cryptology ePrint Archive, Paper 2020/1586},
      year = {2020},
      note = {\url{https://eprint.iacr.org/2020/1586}},
      url = {https://eprint.iacr.org/2020/1586}
}

実装: circify/circ

Abstract

Proof System, MPC, FHE はコンパイラを必要とする
- これは新しいものではなく, software verification commu には論理回路へのコンパイルに関する知見ある
これらは存在的定量化回路を共通の抽象化として持っているのでコンパイラ基盤が構築できる
R1CS, SMT, ILPを使って2000LoCで構築
暗号言語用のコンパイラを1week, 900LoCで構築した
- 何年もかけて書かれた24000LoCより良い性能
組み合わせたアプリケーション作れる
- プログラムのバグを自動で特定し, バグの存在を暗号で証明する(???)パイプラインを構築した