Circomspect新增分析通道！
我们发布了Circomspect 0.8.0版本，这是我们为Circom设计的静态分析器和linter工具。自2022年9月首次发布以来，我们新增了五项分析通道，支持标签、元组和匿名组件，为每个识别的问题提供详细描述链接，并修复了多个bug。请下载新版本并告诉我们您的想法！
新增分析通道
新增的分析通道（初始工具已有九项）检查Circom代码中可能出现的多种问题：
- 未能正确约束中间信号
- 在实例化模板中未能约束输出信号
- 在除法操作中未能约束除数为非零值
- 将Circomlib中特定于BN254的模板用于不同曲线
- 未能正确约束Circomlib的LessThan电路的输入
除了发现下面讨论的与Circomlib LessThan电路相关的问题外，这些分析通道还可以捕获Veridise最近在circom-pairing库中发现的“百万美元ZK bug”。
GF(p)中的有符号算术
Circom程序操作称为信号的变量，这些变量表示有限域GF(p)中的元素，其中p是一个素数。通常，我们将GF(p)中的元素与半开区间[0, p)中的无符号整数识别。然而，有时使用域元素表示有符号量是方便的，就像我们可能使用[0, 2^32)中的元素表示有符号32位整数一样。镜像用于表示有符号整数值的二进制补码定义，我们定义val(x)如下：
然后，如果val(a) < val(b)作为有符号整数，我们说a在GF(p)中小于b。这意味着q = floor(p/2)是GF(p)中可表示的最大有符号值，而-q = q + 1是最小的有符号值。这也意味着，可能有些令人惊讶的是，q + 1实际上小于q。这也是Circom编译器实现比较运算符<的方式。
通常，如果a > 0，我们说a是正的；如果a < 0，我们说a是负的。确保值a非负的一种方法是限制a的二进制表示的大小（以位为单位）。特别是，如果a的大小严格小于log(p) - 1位，那么a必须小于或等于q，因此是非负的。
Circomlib的’LessThan’模板
有了这个基础，让我们将注意力转向Circomlib定义的LessThan模板。这个模板可用于约束两个输入信号a和b，确保a < b，其实现如下：
查看实现，我们看到它接受一个输入参数n和两个输入信号in[0]和in[1]，并定义一个输出信号out。此外，模板使用Circomlib的Num2Bits模板来约束输出信号out。
Circomlib的Num2Bits模板接受单个参数n，可用于将域元素转换为其n位二进制表示，由大小为n的数组out给出。由于二进制表示的大小受参数n的限制，Num2Bits的输入也隐式约束为n位。在上面的LessThan实现中，表达式(1 « n) + in[0] - in[1]作为输入传递给Num2Bits，这将绝对值|in[0] - in[1]|约束为n位。
为了理解LessThan模板实现的微妙之处，让我们首先考虑预期用例，当LessThan的两个输入最多为n位，其中n足够小以确保两个输入都是非负的。
我们有两种情况需要考虑。如果in[0] < in[1]，那么in[0] - in[1]是一个负的n位值，而(1 « n) + in[0] - in[1]是一个正的n位值。因此，Num2Bits输入二进制表示中的第n位是0，因此out必须等于1 - 0 = 1。
另一方面，如果in[0] ≥ in[1]，那么in[0] - in[1]是一个非负的n位值（因为两个输入都是正的），而(1 « n) + in[0] - in[1]是一个正的(n + 1)位值，最高位等于1。因此，Num2Bits输入二进制表示中的第n位是1，out必须由1 - 1 = 0给出。
这一切都有意义，如果我们想在自己的电路中使用LessThan进行范围证明，这会给我们一些信心。然而，如果我们忘记约束传递给LessThan的输入的大小，事情就会变得复杂。
使用信号表示无符号量
为了描述可能影响使用LessThan定义的电路的第一类问题，考虑信号用于表示无符号值（如货币金额）的情况。假设我们想允许用户从我们的系统中提取资金，而不透露敏感信息，如单个用户的总余额或用户提取的金额。我们可以使用LessThan来实现电路的部分，验证提取金额是否小于总余额，如下所示：
ValidateWithdrawal模板应确保用户不能提取超过其总余额的金额。
现在，假设一个余额为零的恶意用户决定从系统中提取p - 1个代币，其中p是底层素域的大小。显然，这不应该被允许，因为p - 1是一个荒谬的大数字，而且无论如何，用户没有可用的代币用于提取。然而，查看LessThan的实现，我们看到在这种情况下，Num2Bits的输入将由(1 « 64) + (p - 1) - (0 + 1) = (1 « 64) - 2（所有算术都是模p完成的）给出。因此，输入二进制表示的第64位将是0，LessThan的输出将是1 - n2b.out[64] = 1 - 0 = 1。这也意味着ValidateWithdrawal将识别提取为有效。
这里的问题是p - 1也代表GF(p)中的有符号量-1。显然，-1小于1，我们没有约束提取金额为非负。添加一个约束，限制金额的大小小于log(p) - 1位，将确保金额必须是正的，从而防止这个问题。
更一般地说，由于LessThan的输入参数n只限制差值|in[0] - in[1]|的大小，我们通常不能使用LessThan来防止溢出和下溢。这是一个许多开发人员忽略的微妙点。例如，考虑0xPARC维护的零知识（ZK）bug跟踪器中关于算术溢出和下溢的部分。在早期版本中，0xPARC建议使用LessThan来约束相关信号，在一个几乎与上面定义的有漏洞的ValidateWithdrawal模板相同的例子中！
Daira Hopwood在ZK太空征服游戏Dark Forest的早期版本中发现了另一种此类漏洞。这里，漏洞允许用户在游戏场地之外很远的地方殖民行星。开发人员通过添加基于Num2Bits模板的范围证明来解决这个问题，将坐标的大小限制为31位。
使用信号表示有符号量
现在，假设信号用于表示有符号量。特别是，让我们考虑如果我们将q = floor(p/2)和q + 1作为输入传递给LessThan会发生什么。我们将证明，尽管根据Circom编译器q + 1 < q，但根据LessThan，q实际上小于q + 1。回到LessThan定义中Num2Bits的输入，我们看到如果in[0] = q和in[1] = q + 1，Num2Bits的输入由以下表达式给出：
(1 « n) + in[0] - in[1] = (1 « n) + q - (q + 1) = (1 « n) - 1
因此，该值二进制表示中的第n位是0，LessThan的输出是1 - n2b.out[n] = 1 - 0 = 1。因此，根据LessThan，q < q + 1，尽管根据编译器q + 1 < q！
这里值得重申的是，LessThan的输入参数n不限制输入的大小，只限制它们的差值的绝对值。因此，我们可以自由地将非常大（或非常小）的输入传递给LessThan。同样，如果LessThan模板的两个输入的大小都被限制为小于log(p) - 1位，则可以防止这个问题。
Circomspect来救援（第一部分）
为了找到此类问题，Circomspect识别使用LessThan的位置。然后，它尝试查看LessThan的输入是否使用Circomlib的Num2Bits模板约束到小于log(p) - 1位，如果没有找到此类约束，则发出警告。这允许开发人员（或审查员）快速识别代码库中需要进一步审查的位置。
最新版本的Circomspect在上面定义的ValidateWithdrawal模板上运行的输出。
如上图所示，Circomspect的每个警告现在通常还包含一个指向潜在问题描述的链接，以及如何解决它的建议。
Circomspect来救援（第二部分）
我们还想提到我们的另一个新分析通道。最新版本的Circomspect识别实例化模板但未约束模板定义的输出信号的位置。
例如，考虑上面介绍的ValidateWithdrawal模板。假设我们重写模板以包括输入信号amount和total的范围证明。然而，在重写过程中，我们意外地忘记包括确保LessThan输出为1的约束。这意味着用户可能能够提取大于其总余额的金额，这显然是一个严重的漏洞！
我们重写ValidateWithdrawal以包括两个输入amount和total的范围证明，但意外地忘记约束输出信号lt.out为1！
有一些例子（如Num2Bits），其中模板约束其输入，不需要对输出进行进一步约束。然而，忘记约束模板的输出通常表示错误，需要进一步审查以确定是否构成漏洞。Circomspect将标记输出信号未约束的位置，以确保每个位置都可以手动检查正确性。
如果Circomspect发现模板定义的输出信号未正确约束，它现在会生成警告。
让我们谈谈！
我们Trail of Bits对为ZK不断增长的工具和库范围做出贡献感到兴奋，这些工具和库在最近几年出现。如果您正在使用ZK构建项目，我们很乐意与您交谈，看看我们是否能以任何方式提供帮助。如果您有兴趣让我们审查您的代码，或者如果您想将部分开发外包给可信的第三方，请与我们经验丰富的密码学家团队联系。
如果您喜欢这篇文章，请分享： Twitter LinkedIn GitHub Mastodon Hacker News