Optimizing homomorphic evaluation circuits by program synthesis and term rewriting
書き換えベースでBoolean FHE回路最適化
synthesis baseな方法よりも高速かつ優れている
- synthesis baseな方法とは?
- SMT使うこと?
CCS Concepts: Theory of computation > Circuit complexity; Cryptographic primitives
Abstract
- FHE Compilerは最適化ルールを手動で作成するので最適とはいい難い結果を生成ｓる
- 本手法はFHE Compilerの先行研究に基づいてFHE回路の最適化ルールを自動で学習する
- プログラム合成と項書き換えを用いて, mult depth を削減する
- 小さな学習回路群から書き換え規則を学習する
- 等式一致に基づく学習則を最大限に一般化する(?)
- x1.18-3.71(avg: 2.05) fasterな回路を生成
- 本手法は既存の分野別最適化手法と直交している(?)
1. Introduction
- 実用に耐えるFHEアプリケーションの計算コストの削減が重要な課題の一つ
Existing Approaches
domain-specific approatch
基盤となるFHEスキームの専門的な知識が必要
- rescaling [23]
- data movement [38]
- batching [39]
- パラメータ選択のヒューリスティック [23], [25]
は - 画像認識 [23]
- 統計解析 [38]
- ソート [17]
- バイオインフォマティクス [19]
- データベース [8]
- 静的プログラム解析 [37]
optimizing FHE compiler
FHE compilerはこのハードルを下げることが出来ていて
ex.
- Ramparts [4]
- Cingulata [15]
- Alchemy [22]
ユーザーはFHEスキームの詳細を知る必要はないが, FHEに適したアルゴリズムを書く必要があり, [16], [17], [19], [38] これに専門知識を必要とする.
最新のFHE compilerは手書きの最適化ルールに依存していて, そのルールを考案するには専門知識が必要なので最適でない可能性が高い.
Our Approarch
- 既存のFHE自動最適化技術を凌駕するFHE boolean回路の最適化手法を提案
- より低いコスト(= 乗算深さが小さい)回路に変換する最適化
depicts: 示す
-
学習回路群で書き換えを学習した後, その規則を使って書き換えをする
-
syntactic matching の代わりに equational matching を用いることで書き換えを最大限に一般化
-
本手法は 健全性 があり, terminating が保証される.
-
本手法を Armadillo A Compilation Chain for Privacy Preserving Applications 上に実装して
- 統計解析
- ソート
- mediacal diagnosis
- low-level アルゴリズム
の18の回路で評価
-
この手法は arithmetic circuits にも適用できる.
2. Problem Definition
2.1 Homomorphic Encryption
バイナリ が平文のFHE schemeは
は暗号文の空間(i.e )
- よってこのshcemeはすべてのブール回路を評価可能
HEの仕組み
Lattice based Somewhat Homomorphic Encryption とかでみた
2.2 Boolean Circuit and Multiplicative Depth
Boolean circuit
ブーリアン回路 は
- : 入力変数
Multiplicative Depth
let は回路の mult depth を表す.
Critical Path
入力から出力までの間に最もANDが多いパスを critical path と呼び, と書く
フォーマルに書いている
critical positions は文字列 のすべての部分前置文字列
ex.