秘密进行,公开断言:不要在ZK程序中过度约束Prover的witness计算 - ZKSECURITY

本文深入探讨了零知识证明(ZK)应用开发中常见的安全漏洞,重点强调了在构建ZK应用时,开发者必须充分约束证明者的计算,否则验证者可能会验证无意义的内容。文章通过具体例子,例如除法和平方根运算,展示了如何避免因Prover/Verifier阶段分离不清而引入的约束不足问题,并强调了代码审查和安全审计在保障ZK应用安全性的重要性。

约束不足的 Bug

现在是学习和深入研究 ZK 应用开发的好时机。如果不小心,在开始构建 ZK 应用程序时,可能会出现大量的安全错误。这些问题通常源于头脑中错误的参考框架,以及对错误细节的关注。阅读本文,了解你需要的思维模式,以及使用零知识证明进行编程时需要注意的陷阱。

背景

2017 年秋天我开始研究 Mina 协议时,在生产环境中使用零知识编写应用程序还非常罕见。然而,今天在加密/web3 领域,ZK 编程正在蓬勃发展,而且我相信,很快 web2 领域也会迎来繁荣。早期,为了管理大型 ZK 应用程序的复杂性,开发人员需要构建自己的 DSL 和 SDK,但现在有很多选择:包括我在内的一些 zkSecurity 审计员目前在 O(1) Labs 维护 SnarkyJS。像 SnarkyJS 或 Noir 或 Cairo1.0 这样的工具,以及像 Mina 协议或 Aleo 这样的执行运行时,使开发人员更容易开始编写 ZK 应用程序 —— 并且他们已经开始了!现在有 ZK 聚会、会议、播客、研讨会、黑客之家和公司、团队,以及目前无数的开发人员开始将这项技术首先用于娱乐,然后在生产中使用。如果你好奇,现在是你开始的好时机!

正如 David 在ZK programmability adds a whole new layer to worry about中提到的,在开发 ZK 应用程序的许多方面,安全问题可能会破坏你的应用程序。我想重点分享一个理解,即 prover 的计算必须在你的 ZK 应用程序中完全约束,否则你将证明无意义的东西,因为这正是我五年前刚开始使用 ZK 编程时努力理解的东西。

预备知识

在我们深入研究这些约束不足的问题之前,让我们先用一些非正式的定义来确保我们达成共识:

一个真实的 ZK application 是指在至少两个参与方(即 proververifier)之间的计算过程中包含阶段分离的应用程序。通常,prover 会做额外的工作,并且为了可扩展性或隐私目的,会创建、操作和处理私有数据。verifier 可以检查一个 ZK proof,如果定义和构造正确,则可以有效地验证计算,而无需观察私有数据。verifier 将私有变量视为 存在量化 的变量,换句话说,verifier 认为“存在一些数据 w,prover 知道但 verifier 不知道,并且 w 满足某些属性”。有时,与私有变量对应的值被称为 witness,因为它们充当 witness,这是一种通过证据证明存在量化变量存在的形式。请注意,prover 和 verifier 之间互不信任,我们必须以对抗性的思维来考虑问题 —— 即,如果 prover 能够欺骗 verifier,他们就会这样做。

由于 verifier 的计算不直接处理私有数据,因此,你的应用程序规则是通过引入关于数据某些属性的断言或约束来施加的。这些约束的实现细节在不同的证明系统中会以不同的方式实现,但是如果你正在使用一个抽象了这些细节的不错的 SDK,那么大多数时候你只需要考虑你需要哪些断言。

最后,约束不足私有数据 描述了一类安全错误,当这些存在量化的变量没有足够的断言来让 verifier 正确地强制执行应用程序所需的数据形式时,就会出现这类错误。

在构建 ZK 应用程序时,你必须不断地在 prover 和 verifier 世界之间跳转。不同的工具包采用不同的方法来向其开发人员公开这些领域。例如,Noir 假设 prover 的计算发生在其他地方,而 Noir 代码只描述了计算的 verifier 端。

// 我当前的年龄是我账户创建时的年龄加上账户创建以来的年数
// 在其他地方:首先查找账户信息并检查签名,然后返回,将该值传递到此函数调用

struct AccountInfo { startAge: Field, yearsSince: Field }

fn getMyAgeIfNotChild(retrievedAccountInfo : AccountInfo) -> Field {
   let age = retrievedAccountInfo.startAge + retrievedAccountInfo.yearsSince;
   assert(age >= 18);
   age
}

另一方面,SnarkyJS 通过要求开发人员 证明存在量化变量 来交错这些世界,以便同时定义 prover 和 verifier 的计算。

// 我当前的年龄是我账户创建时的年龄加上账户创建以来的年数

class AccountInfo extends Struct({ startAge: Field, yearsSince: Field }) {}

function getMyAgeIfNotChild(userid: String, serverPk: PublicKey): Field {
  const accountInfo = Provable.witness(AccountInfo, () =>
     const accountInfo = loadAccount(userid);
     if (!accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature])) {
       throw new Error("my account database is busted");
     }
     return new AccountInfo({ ...accountInfo });
  );

  const age = accountInfo.startAge.add(accountInfo.yearsSince);
  age.assertGreaterThanOrEqual(18);
  return age;
}

常见错误:未能认识到 prover/verifier 阶段的分离

在任何一种情况下,我们都不能假设数据具有任何属性,而没有对其进行检查!对于刚开始使用 ZK 的开发人员来说,我所见过的导致约束不足错误的最大错误是未能认识到这种阶段分离,并认为 verifier 端将继承计算的 proving 端的属性。认识到这种差异!你是否发现我们忘记在上面的例子中约束签名在验证阶段是有效的?

// 我当前的年龄是我账户创建时的年龄加上账户创建以来的年数
// 在其他地方:查找账户信息并检查签名,然后返回,将该值传递到此函数调用

struct AccountInfo { startAge: Field, yearsSince: Field, signature: [u8;64] }

fn getMyAgeIfNotChild(retrievedAccountInfo : AccountInfo, serverPkX : pub Field, serverPkY : pub Field) -> Field {
   let chunk1 = retrievedAccountInfo.startAge.to_be_bytes(2);
   let chunk2 = retrievedAccountInfo.yearsSince.to_be_bytes(2);
   let data = combine_arrays(chunk1, chunk2); // 假设 combine_arrays 存在
   verify_signature(serverPkX, serverPkY, retrievedAccountInfo.signature, data);

   let age = retrievedAccountInfo.startAge + retrievedAccountInfo.yearsSince;
   assert(age >= 18);
   age
}
// 我当前的年龄是我账户创建时的年龄加上账户创建以来的年数

class AccountInfo extends Struct({ startAge: Field, yearsSince: Field, signature: Signature }) {}

function getMyAgeIfNotChild(userid: String, serverPk: PublicKey): Field {
  const accountInfo = Provable.witness(AccountInfo, () =>
     const accountInfo = loadAccount(userid);
     if (!accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature])) {
       throw new Error("my account database is busted");
     }
     return accountInfo;
  );

  accountInfo.signature.verify(serverPk, [accountInfo.yearsSince, accountInfo.signature]).assertTrue();

  const age = accountInfo.startAge.add(accountInfo.yearsSince);
  age.assertGreaterThanOrEqual(18);
  return age;
}

最终,这是所有与约束不足相关的错误的根源。而且,不幸的是,即使有了良好的 prover/verifier 阶段分离的思维模式,仍然有空间让更微妙的错误溜进来:使用私有数据的计算可能会污染未来的断言。这最好通过几个例子来演示。

除法

除法运算通常作为 ZK 语言中的一个原语提供给你。但是,如果我们自己实现它,它就是一个很好的例子:在电路中进行除法的一种方法是构造逻辑,以便 prover 私下计算除法,然后通过验证该值是否相乘来断言正确性。

// dividend / divisor = quotient (在伪代码中)
function unsafeDivide(dividend: Field, divisor: Field): Field {
  let quotient = witness { dividend / divisor };
  constraint(quotient * divisor == dividend);
  return quotient;
}

但是,如果是零呢!除法在零处应该是未定义的。但是如果我们传递零作为除数,我们可以证明任何东西都是商!这种错误通常会导致灾难性的安全问题。

为了解决这个问题,我们可以确保除数不能为零:

// dividend / divisor = quotient (在伪代码中)
function safeDivide(dividend: Field, divisor: Field): Field {
  let quotient = witness { dividend / divisor };
  constraint(quotient * divisor == dividend);
  constraint(quotient != 0);
  return quotient;
}

平方根

平方根运算也很有趣。与除法类似,我们通过逆运算进行计算。但是,这一次,平方根在零处是定义良好的。由于我们不会在这篇文章中讨论的细微差别,让我们假设我们已经确保平方根在呈现的输入处是定义的。

// sqrt(x) = root (在伪代码中)
function unsafeSqrt(x: Field): Field {
  let root = witness { sqrt(x) };
  constraint(root * root == x);
  return root;
}

更一般地,当使用 ZK 时,任何具有单一确定性输出的可逆运算都可以安全地以这种方式表示。但是等等,平方根没有确定性的输出!正值和“负”值都是有效的!

“负”值在域中是什么意思?我们在实践中使用的域通常是 Z_p,其中 p 是某个素数。本质上,正整数值在 p 处环绕。因此 -root 等于 p - root。由于 p 是素数,它必须是奇数,这意味着 -root 将具有与 root 不同的奇偶性(奇数与偶数)。检查输入的奇偶性是否与根的奇偶性相同,就足以找到一个合理的规范平方根。

// sqrt(x) = root (在伪代码中)
function saferSqrt(x: Field): Field {
  let root = witness { sqrt(x) };
  constraint(root * root == x);
  constraint(parity(x) == parity(root));
  return root;
}

审查和审计

为了发现这些约束不足的错误,必须建立一个强大的审查和审计流程。例如,在我从事 Mina 的日常工作中,我不仅依赖第三方审计,还敦促我的同事和我自己投入工程时间来审计我们自己的 ZK 计算,寻找这类约束不足的错误。

在 zkSecurity,我们在现实世界的场景中遇到了许多这类问题,我们有能力帮助你防止此类 Bug 影响你的应用程序。有时,拥有一个新鲜和经验丰富的视角可以对识别潜在问题产生很大的影响。如果你对我们的专业知识感兴趣,请随时通过 hello@zksecurity.xyz 与我们联系。

结论

随着越来越多的开发人员冒险构建 ZK 应用程序,他们必须深入了解 prover 和 verifier 的世界。通过认识到它们之间的区别,并记住“做”是秘密的,而断言是 verifier 看到的唯一东西,开发人员可以避免常见的陷阱。

即使有了这种心态,重要的是对某些局部运算如何污染未来的断言保持警惕。接受即使是最勤奋的个人也可能犯错误是保持强大开发流程的关键。始终进行代码审查,并认真考虑进行审计,以确保你的 ZK 应用程序的安全性和正确性。我们在 zkSecurity 的团队非常乐意协助你构建安全高效的 ZK 应用程序。

随着 ZK 编程世界的不断发展,开发人员必须牢记可能出现的潜在安全问题。通过理解 ZK 编程的细微差别,利用正确的工具和库,并投入到强大的审查和审计流程中,开发人员可以创建安全的应用程序,最大限度地发挥零知识证明的潜力。

  • 原文链接: blog.zksecurity.xyz/post...
  • 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
点赞 0
收藏 0
分享
本文参与登链社区写作激励计划 ,好文好收益,欢迎正在阅读的你也加入。

0 条评论

请先 登录 后评论
zksecurity
zksecurity
Security audits, development, and research for ZKP, FHE, and MPC applications, and more generally advanced cryptography.