从零开始学习 zk-SNARK(四)——多项式的约束

SECBIT实验室
SECBIT实验室 机构得得号

Jan 17, 2020 聚焦智能合约安全审计和形式化验证。

该文章已上链

摘要: 从零开始学习 zk-SNARK(四)——多项式的约束

从零开始学习 zk-SNARK(四)——多项式的约束
00:00
25:33

even@安比实验室: 上一篇文章中我们学习了如何将程序转换为多项式进行证明。到这里似乎已经有点晕了,本文将对协议执行进一步的约束,并对协议展开优化。

作者:Maksym Petkus

翻译 & 注解:even@安比实验室

校对:valuka@安比实验室

本系列文章已获作者中文翻译授权。

结构性质

上文中的修改额外带来了一些其它有用的性质。

静态系数

在上文的构造中,我们通过对 未赋值的变量多项式 的计算得到0 或者 1 ,以此表示在运算中是否要用到这个变量。自然地想,我们也可以使用其它系数值,包括负数值,因为我们可以插值 计算出经过任何必要的点(前提是没有两个计算使用了同一个 x)的多项式。如下是这种运算的一些例子:

2a×1b=3r

-3a×1b=-2r

现在我们的程序就可以使用静态系数了,例如:

Algorithm 2: Constant coefficients
————————————————————————————————————————————————————————————

function calc(w, a, b)
  if w then
      return 3a × b
  else
      return 5a × 2b
  end if
end function

在 setup 阶段这些系数类似于 0 或者 1 将被“硬编码”进去,之后就不能再修改了。现在我们将运算形式修改为:

或者更正式得用参数 vn ∈ {v1, v2, …, vn} 表示:

其中下标 lro 表示变量在运算中的位置。

注意:在不同的运算和操作数/输出中,同一个变量的常量系数可以是不同的。

没有成本的做加法

看一下这个新结构,很显然在多项式的表示中,每一个不同 x 所要代表的操作数都是所有操作数变量多项式 的总和,其中只有一个被用到的变量是非零值而其它都为 0,下图就很好得表达了这个意思:

我们可以利用这一个结构,加任何数量必要的变量 到每一个运算的操作符/输出中。例如在第一个运算中,我们可以首先做加法 a+c,然后就只需要用别的操作数与之相乘了,即 (a+ c) × b = r,可以表示为下图:

因而也可以将这些变量中任意个,对它们先乘以任意的系数再一并加入到一起作为单个操作数中,以此来根据相应程序的需要构造一个操作数值。这个特性实际上就允许将运算结构改为:

注意 :每一个运算的操作数都有自己的一组系数 c。

even@安比实验室:乘法运算是关键,而加法运算都可以被合并到一个更大的乘法运算里面。

加法,减法和除法

到目前为止,我们一直专注于乘法操作。但是为了能够执行通用计算,真实环境下的程序也需要加法,加法和除法。

加法 在前面的章节中,我们已经确定了可以在单个操作数的内容中将变量加起来,然后和另一个操作数相乘,即(3a + b) × d = r ,但是如果我们只是想做加法,没有乘法,例如一个程序中需要做 a + b 的计算,我们可以按照下面的方式来表示: (a+b) × 1 = r​

@Maksym(作者):因为我们的结构中对于每一个操作数我们既需要常量系数也需要变量 (c ⋅ v) ,1 这个值可以表示为 c ⋅ v,其中 c = 1 可以被“硬编码”到对应的多项式中, v 是一个变量可以给它分配任何值,那么我们就必须通过一些约束来限制 v 的值,这个在后面的章节中将会讲到。

减法 减法与加法几乎一致,唯一的不同就是负系数, a-b也就是:

除法 如果我们检查除法运算

可以看到除法的结果是就是我们要得到一个结果值使其乘以 divisor 能够得到 factor。所以我们也可以用乘法来表示出同一个意思:divisor × result = factor。这样就是说如果我们想要去证明除法运算 a / b= r,我们就可以把它表示为:

@Maksym(作者):运算的结构也称为 “约束” ,因为多项式结构代表的运算,并非是为了计算出结果,而是在 prover已经知晓的变量赋值的情况下,检验这个运算的过程是否正确。换句话说,即约束 prover 必须提供一致的值,无论这些值是什么。

所有的算术计算(加减乘除)都已经有了,于是运算结构不再需要修改。

even@安比实验室: 约束和运算有一定的关联性。算术电路的目的是为了实现「计算的验证」,而非「计算的过程」。

上一篇文章中,我们提出了一种方法:把构造多项式的工作交给 setup 环节,prover 只要填上对应的数值就可以了。 这个方法不仅解决了同一个操作数运算符中不一致的问题,同时还带来了额外的便利:

1)允许执行计算的表达式中包含静态系数。

2)虽然l(x)·r(x)=o(x)的关系中只有乘法,但利用这个方法也可以轻松的执行加法操作,继而也就解决了减法和除法的问题。

计算示例

有了一组通用的运算结构,我们就可以将我们原始的程序(上一篇文章中的例子)转换成一组运算,然后再转换成多项式的形式。我们先来想一下算法的数学形式(用变量 v 表示运算结果):

这里有三个乘法,但是由于运算结构只支持一个乘法操作,所以这里至少就要做三次运算。但是,我们可以将它简化为:

现在要包含同样的关系只需要两个乘法。这种运算的完整形式就是:

我们还可以再增加一条约束使 w 必须为二进制数,否则 prover 就可以代入任何值去执行一个错误的运算了:

要了解为什么 w 只能为 0 或者 1,我们可以把等式表示为 w² – w = 0,也就是 (w – 0)(w – 1) = 0 这里 0 和 1 是唯一解。

现在一共有 5 个变量,以及 2 个左操作符, 4 个右操作符和 5 个输出。操作符多项式为:

在三次运算中必须为每个*变量多项式 都分别算出一个对应的系数或者如果这个多项式在计算的操作数或者输出中没有被用到的话系数就置为 0。

$\begin{align*} \textcolor{green}{l_a(1)}=1; \textcolor{green}{l_a(2)}=0; \textcolor{green}{l_a(3)}=0;\textcolor{blue}{r_m(1)}=0; \textcolor{blue}{r_m(2)}=\ \ \, 1;\textcolor{blue}{r_m(3)}=0;\textcolor{red}{o_m(1)}=1; \textcolor{red}{o_m(2)}=\ \ \; 0;\textcolor{red}{o_m(3)}=0; \ \textcolor{green}{l_w(1)}=0;\textcolor{green}{l_w(2)}=1;\textcolor{green}{l_w(3)}=1;\, \textcolor{blue}{r_a(1)}=0;\, \textcolor{blue}{r_a(2)}=-1;\ \textcolor{blue}{r_a(3)}=0;\; \textcolor{red}{o_v(1)}=0;\ \textcolor{red}{o_v(2)}=\ \ \; 1;\;\textcolor{red}{o_v(3)}=0; \ \textcolor{blue}{r_b(1)}=1;\ \textcolor{blue}{r_b(2)}=-1;\; \textcolor{blue}{r_b(3)}=0;\, \textcolor{red}{o_a(1)}=0;\ \textcolor{red}{o_a(2)}=-1;\; \textcolor{red}{o_a(3)}=0; \ \textcolor{blue}{r_w(1)}=0; \textcolor{blue}{r_w(2)}=\ \ \, 0; \, \textcolor{blue}{r_w(3)}=1;\, \textcolor{red}{o_b(1)}=0;\ \, \textcolor{red}{o_b(2)}=-1; \; \textcolor{red}{o_b(3)}=0; \ \textcolor{red}{o_w(1)}=0;\, \textcolor{red}{o_w(2)}=\ \ \; 0; \textcolor{red}{o_w(3)}=1;\end{align*}$

结果因式多项式就是 t(x) = (x – 1)(x –2)(x –3),它必须确保这三个运算都能被正确计算。

接下来,我们利用多项式插值法来找到每个变量多项式:

$\begin{align*}\textcolor{green}{l_a(x)}=\ \ \ \frac{1}{2}x^2-\frac{5}{2}x+3; \qquad \qquad \textcolor{blue}{r_m(x)}=-x^2+4x-3; \qquad \qquad \textcolor{red}{o_m(x)}=\ \, \ \frac{1}{2}x^2 - \frac{5}{2}x +3; \ \textcolor{green}{l_w(x)}=- \frac{1}{2}x^2+\frac{5}{2}x-2; \qquad \qquad \textcolor{blue}{r_a(x)}=\ \, \ x^2-4x + 3; \qquad \qquad \ \\textcolor{red}{o_v(x)}=-x^2 + 4x - 3; \quad \ \textcolor{blue}{r_b(x)}=\ \, \ \frac{3}{2}x^2-\frac{13}{2}x+6; \qquad \quad\textcolor{red}{o_a(x)}=\ \, \ x^2 -4x + 3; \quad\ \textcolor{blue}{r_w(x)}=\ \, \ \frac{1}{2}x^2-\frac{3}{2}x+1; \qquad \quad \ \\textcolor{red}{o_b(x)}=\ \, \ x^2 - 4x + 3; \quad\ \textcolor{red}{o_w(x)}=\ \ \frac{1}{2}x^2 - \frac{3}{2}x + 1; \end{align*}$

绘制出来就是:

我们准备通过多项式去证明计算,首先,选择函数的输入值,例如: w = 1, a = 3, b= 2。其次,计算过程中的中间变量值为:

m=a × b =6

v = w(m-a-b)+a+b=6

然后,我们把所有计算结果中的值赋值到 变量多项式 中,然后相加得到操作数或者输出多项式的形式:

在图中就表示为:

把他们相加成对应运算中的操作数和输出值:

我们需要去证明 L(x) × R(x) – O(x) = t(x)h(x),因而我们先找出 h(x):

这里很明显多项式 L(x) × R(x) – O(x) 的解为 x= 1, x= 2 和 x= 3,因而 t(x) 是它的因式,假如使用了和它不一致的变量值,情况就不是这样了。

这就是一组能够正确计算的变量值,如何在多项式层面上证明出来的。下面 prover 还要再继续处理协议的密码学部分。

可验证计算协议

我们基于前文中多项式知识协议 做了很多重要的修改使它变得更通用,我们再来看一下它现在的定义。假定函数 f(*) 是要证明的问题中的计算结果,其中操作数的数量为 d ,变量的数量 n ,以及它们对应的系数为:

虽然协议足够健壮,可以进行常规的计算验证,但这里依然还有两个安全考虑需要去解决。

操作数和输出的不可交换性

因为在 变量多项式约束检查 中的所有操作数上我们使用了同一个 α,所以就没有办法阻止 prover 做下面的欺骗行为:

  • 使用其它的操作数中的可变多项式,即 L′(s) = o₁(s) + r₁(s) + r₁(s) +

  • 完全交换 操作数多项式, 也就是把 O(s) 和 L(s) 换成 O(s) × R(s) = L(s)

  • 复用相同的操作数多项式,即 L(s) × L(s) = O(s)

可交换性就是指 prover 可以修改计算过程,并有效证明一些其它无关的计算结果。防止这种行为的一个很显然的方式就是在不同的操作数上使用不同的 αs ,具体协议就可以修改为:

这样就不能在一个操作数中使用其它操作数的变量多项式了,因为 prover 没有办法去获知 来满足 变换关系。

even@安比实验室: 这里通过对l(x),r(x)和o(x) 进行分开 KEA 检查,就解决了上篇文章中提出的第二个缺陷问题——由于 prover 生成的证明中只有计算结果,左操作数,右操作数,输出在计算中混用也不会被发现。

同样下面一节也解决了上篇文章中提出的第三个缺陷问题——由于左操作数,右操作数,输出是分开表示的,互相之间的关系无法进行约束。

跨操作数的变量一致性

对于任意的变量 vᵢ ,我们都必须将它的值 分配 到每个相应操作数中的一个与之对应的变量多项式 上,即:

因为每一个操作数运算符 的有效性是分开校验的,并不强制要求我们在对应的变量多项式 中使用相同的变量值。这就意味着在左操作数中变量 v₁ 的值可以与右操作数或输出中的变量值 v₁不同。

我们可以通过熟悉的限制多项式的方法(也就是限制变量多项式的方法)在操作数之间强制变量值相等。如果我们能够在所有的操作数之间创造一个作为“变换的校验和”的变量多项式,那么就可以限制 prover 使其只能够赋予相同的值。verifier 可以将这些每个变量的多项式加起来,即:

然后乘以一个额外的随机数 β,即

提供这些变换后的多项式给 prover,与变量多项式一起给它赋上变量值:

这个构造中同一个变量值就无法乱用了,因为不同的 βs 使得相同多项式无法兼容,但是这里还存在与 remark 4.1 相同的缺陷,由于gβlgβr gβo 是公开可见的,攻击者可以修改任意变量多项式的零索引系数,因为它并不依赖于 s,即,gβls0= gβl

even@安比实验室: 回忆一下,上文中我们提出了在 setup 阶段设置数学表达式的约束关系来解决了一些问题,但这里似乎有引入了一个问题:如果保证 prover 构造的证明是用遵循这些约束关系计算出来的呢?

KEA 其实已经解决了这个问题,但似乎并不完美,这就是我们下面要讨论的变量延展性问题。

变量非延展性和变量一致性多项式

变量多项式的延展性

举一个 remark 4.1 有关的例子,看一下下面的两个运算:

预期的结果 b = ac = 3a , 再进一步就是 c = 3b。这就是说左操作数的变量 多项式的计算结果为 la(1) = 1 和 la(2) = 3。先不管 la(x) 的形式, prover 都可以不按照上述的比例用另一个修改了的多项式 lₐ′(x) = ala(x) + 1 来给 a 赋值。这样运算就变成了 la′(1) = a+ 1 和 la′(2) = 3a+ 1, 结果也就是 b = a + 1c = 3a + 1,其中 c≠3b,这意味着 a 的取值的实际意义在不同运算中是不一样的。

但是因为 prover 已经拿到了 gαlgβl ,所以他依然能够通过正确的操作符多项式* 和变量值一致性 的校验:

变量一致性多项式的延展性

而且 gβl,gβr,gβo的存在允许我们在不同操作数的相同变量上使用不同的值。例如,如果我们有一个运算:

a×a=b

可以用多项式表示:

尽管我们期待的输出是 b= a²,但我们可以设置不同的 a 值,例如:设置 a= 2 (左操作数中), a= 5 (右操作数中)如下:

注意:多项式 oa(x),lb(x),rb(x) 其实可以被忽略掉的,因为这几项对于任何 x 的取值,计算结果都为 0,但是为了保持完整性我们依然要保留这几项。

even@安比实验室:这种能力会危害到协议的可靠性。很显然,加密的 βs不应该对 Prover 可见。

非延展性

解决延展性问题的一个方法就是,在 setup 阶段将 verification key 中加密的 βs 项与随机秘密值 γ(gamma) 相乘使其与加密值 Z(s) 不兼容:

相应的这种被修饰过的加密值,就能阻止使得修改加密值 Z(s) 变得不可行了,因为 Z(s) 中没有 γ,即:

因为变值 γ 是随机的 prover 并不知道它的值。所以这个修改就需要我们用 Z(s) 乘以 γ 来平衡协议中的变量值一致性校验* 等式:

这里很重要的一点是我们排除了变量多项式为 0-阶的例子(即, l₁(x) = 1x⁰),否则就可以从 proving key变量一致性多项式 中揭露出加了密的 β

这个例子中当操作数/输出中的任意两项为 0 时,即,对于 l₁(x) = 1, r₁(s) = 0, o₁(s) = 0 的例子,结果就是

我们同样也可以通过修饰 αs 项来解决变量多项式 的延展性问题。但是这就没有必要了,因为对于变量多项式 的任何修改,都需要被映射到变量的一致性多项式 中,而一致性多项式是无法修改的。

变量值一致性检查的优化

现在变量值一致性 检查是有效的,但是这里在 verification key 中增加了 4 个昂贵的配对操作和 4 个新的项。文献 [Par+13] 中的 Pinocchio 协议用了一个很聪明的方法优化,通过选择不同的生成元 g ,从而对每个操作数实行“移位”:

生成元的这种随机化进一步增加了安全性,使得如 remark 4.1中描述的可变多项式 延展性无效。因为对于故意的修改,它必须要么是ρl, ρr 或者ρo 原始值的倍数要么就是不可直接用的加密值的倍数(假定,如上文所述我们不去处理可能曝光加密后的值的 0 阶可变多项式)。

这个优化使得 verification key 减少了两个项,并且去除了 verification 步骤中的两个配对运算。

注意:在 Jens Groth 2016年的 paper [Gro16] 中有更进一步的改进。

even@安比实验室:至此,通用 zk-SNARK 协议的已经几乎构造完成了,本文可以归纳为以下几点:

协议中是如何增加可变系数的和如何做加减乘除运算的

协议如何保证操作数和输出的不可替代性

协议如何保证跨操作数的可变一致性

协议如何处理非延展性变量和变量一致性

协议中变量值一致性检查优化

原文链接

https://arxiv.org/pdf/1906.07221.pdf

https://medium.com/@imolfar/why-and-how-zk-snark-works-5-variable-polynomials-3b4e06859e30

https://medium.com/@imolfar/why-and-how-zk-snark-works-6-verifiable-computation-protocol-1aa19f95a5cc

参考文献

[Par+13] — Bryan Parno, Craig Gentry, Jon Howell, and Mariana Raykova. Pinocchio: Nearly Practical Verifiable Computation. Cryptology ePrint Archive, Report 2013/279. https://eprint.iacr.org/2013/279. 2013.

[Gen+12] — Rosario Gennaro, Craig Gentry, Bryan Parno, and Mariana Raykova. Quadratic Span Programs and Succinct NIZKs without PCPs. Cryptology ePrint Archive, Report 2012/215. https://eprint.iacr.org/2012/215. 2012.

[Gro16] — Jens Groth. On the Size of Pairing-based Non-interactive Arguments. Cryptology ePrint Archive, Report 2016/260. https://eprint.iacr.org/2016/260. 2016. 

(1、 内容来自链得得内容开放平台“得得号”,稿件内容仅代表作者观点,不代表链得得官方立场。2、 凡“得得号”文章,原创性和内容的真实性由投稿人保证,如果稿件因抄袭、作假等行为导致的法律后果,由投稿人本人负责。3、 得得号平台发布文章,如有侵权、违规及其他不当言论内容,请广大读者监督,一经证实,平台会立即下线。如遇文章内容问题,请发送至邮箱:chengyiniu@chaindd.com)

链得得仅提供相关信息展示,不构成任何投资建议
本文系作者 SECBIT实验室 授权链得得发表,并经链得得编辑,转载请注明出处、作者和本文链接

更多精彩内容,关注链得得微信号(ID:ChainDD),或者下载链得得App

分享到:

相关推荐

    评论(0

    Oh! no

    您是否确认要删除该条评论吗?

    分享到微信