使用标签分析检测零知识电路中的回旋镖值 - ZKSECURITY

zksecurity
发布于 2023-08-26 15:24
阅读 18

zkApps开发中，从电路中取出值并在电路外使用后重新插入电路，会产生被称为“回旋镖值”的问题，可能导致安全漏洞。文章介绍了如何在Rust中使用MIRAI的标签分析功能来检测这种问题，并简要提及了使用fuzzing来查找电路中的bug。

zkApps（零知识应用）是指计算机程序的可证明转换。也就是说，它们应该像它们旨在代表的计算机程序一样运行，同时提供正确的执行证明，这些证明可以伴随程序输出。但是，正如[我们之前讨论过的](https://learnblockchain.cn/article/17884/)，将程序转换为可证明的程序并不是一个简单的过程。为了证明执行，zkApps 尝试“见证”执行跟踪的所有重要部分。它们试图断言原始应用程序中指定（显式或隐式）的每个角落。这里的关键词是“所有”和“每个”，因为如果 zkApp 的断言中缺少原始程序的哪怕是最微小的部分，也可能发生错误。

![回旋镖](https://i.imgur.com/nDbPGGb.png)

在本文中，我们想讨论 **回旋镖值**，这是编写 zkApp 时出现的一种陷阱的例子。什么是回旋镖值？它们会产生什么样的错误？我们能用它们做什么？继续阅读！

### 混合电路内和电路外逻辑

开发者编写 zkApps 是为了用更高级的语言编码他们想要见证的逻辑。这些更高级的语言可以采取不同的形式（正如我们在[这篇文章中描述的](https://learnblockchain.cn/article/17846/noname/)），并且它们中的许多通常会将非电路（或电路外）逻辑与电路（或电路内）逻辑混合在一起。

为什么有人甚至想要这样的东西的典型例子（或者混合电路外和电路内逻辑意味着什么）是**除法例子**，在这种情况下，更容易在电路外计算除法的结果，然后像它从天而降一样提供它。

这是除法函数通常在 zkApps 中编写的方式，在一些 python 伪代码中：

```python
def divide(a_var, b_var):
	# 在电路外计算除法
	c = a_var.value() / b_var.value()

# 见证 / 将电路外值插入电路中
	c_var = new_var(c)

# 约束它为除法的正确结果
	assert(c_var * b_var == a_var)

return c

```

如果这不能立即让你理解，请这样考虑：zkApp 在编译时编码了对**变量**的一些断言。这里它将编码这样一个事实，即存在一个变量 `c_var`，只要它满足 `c_var * b_var == a_var`，它就可以取任何值。

在运行时（或证明时），当我和你想要执行程序并为其创建证明时，我们将为 `a_var` 和 `b_var` 提供实际值，并基于此创建证明。类似地，将为 `c_var` 提供一个值，该值将基于上面的电路外逻辑计算。

重要的是，`divide` 函数 **定义了编译时逻辑和运行时逻辑**。虽然编译时是证明者和验证者都做的事情，但运行时逻辑是只有证明者运行的东西，因此**恶意证明者可以决定做他们想做的任何事情**。特别是，他们不必像程序中描述的那样将 `c` 计算为 `a / b`！

### 变量的生命周期和链接问题

在我们上面的程序中，一个试图将 `c` 计算为除 `a / b` 之外的任何东西的恶意证明者将会失败，因为电路检查除法是否正确。删除断言，你将得到一个约束不足的电路（这是一个错误）。在本文中，我们对属于此类约束不足电路错误的一类问题感兴趣。

电路中的变量有一个生命。它首先被创建（并在运行时被赋予一个值），然后它将被改变并以各种方式使用。是的，就像普通程序中的变量一样。从某种意义上说，变量被连接到电路逻辑的不同部分。

**但是这根线可以被切断**。例如，想象一下下面的伪代码：

```python
## 创建一个新的电路变量
a_var = new_var(some_value);

## 用它做一些事情...

## 从电路外获取值
a_val = a_var.value()

## 潜在地用这个值做一些重要的事情...

## 将该值重新插入电路中
b_var = new_var(a_val)

```

这是一个相当笼统和模糊的例子，但它应该足以说明我的观点。在这里，你应该能够判断出有些不对劲。如果不能，可以花几分钟思考一下。

问题在于上面的程序向证明者发出了以下指令：“观察`a_var`的运行时值，然后将其重新插入程序中的其他位置（在`b_var`下）”。如果你是一个恶意的证明者，你可能会听到的是“添加你想要的任何东西作为`b_var`”。

线被切断了，链接断开了。我们将这些称为 **回旋镖值**，因为它们离开电路并在稍后重新插入。它们几乎总是不好的。

有趣的是，凭直觉来看，似乎只有 `b_var` 现在受到约束不足的影响，但实际上它是双向的！也许你想要保持正确的值作为 `b_var`，但现在你可以使用一个不同的值作为 `a_var`，因为它不再与 `b_var` 的正确值相关联。

换句话说，如果 `a_var` 和 `b_var` 的正确值是数字 `5`，那么一个恶意的证明者可以决定保持 `b_var.value() = 5` 并将 `a_var` 的值更改为其他值，或者他们可以决定保持 `a_var.value() = 5` 的值并将 `b_var` 更改为其他值。

有关这种类型的错误可能产生的影响的示例，你可以查看我们对 Penumbra 的[公开审计](https://penumbra.zone/blog/2023-audits/)，我们在其中发现了一个导致双重支出攻击的回旋镖值。今天，我们将研究如何在 Rust 堆栈中检测此类错误，特别是使用 Arkworks 的 R1CS 库 [r1cs-std](https://github.com/arkworks-rs/r1cs-std) 的堆栈。

### R1CS-std 的 ABC

当使用 [r1cs-std](https://github.com/arkworks-rs/r1cs-std) 编写电路时，我用来创建新变量以及获取变量运行时值的上述伪函数是通过使用两个函数 `new_variable()` 和 `value()` 实现的。这两个函数位于开发者可以在他们自己的自定义类型上实现的两个不同的 trait 中。

这是 `new_variable`：

```rust
pub trait AllocVar<V, F: Field>
where
    Self: Sized,
    V: ?Sized,
{
    /// 在 `ConstraintSystem` `cs` 中分配一个新的 `Self` 类型的变量。
    /// 分配模式由 `mode` 决定。
    fn new_variable<T: Borrow<V>>(
        cs: impl Into<Namespace<F>>,
        f: impl FnOnce() -> Result<T, SynthesisError>,
        mode: AllocationMode,
    ) -> Result<Self, SynthesisError>;

```

正如你所看到的，它没有接受一个值，而是接受一个函数/闭包 `f`，它产生该值（但这只是一个细节）。

这是 `value()`：

```rust
/// 这个 trait 描述了一些核心功能，这些功能对于高级
/// 变量是通用的，例如 `Boolean`s、`FieldVar`s、`GroupVar`s 等。
pub trait R1CSVar<F: Field> {
    /// `Self` 在约束系统中表示的“原生”值的类型。
    type Value: core::fmt::Debug + Eq + Clone;

/// 返回在底层 `ConstraintSystem` 中分配给 `self` 的值。
    fn value(&self) -> Result<Self::Value, ark_relations::r1cs::SynthesisError>;

```

因此，如果我们使用 arkworks 的 r1cs-std 库来编写回旋镖示例，它将如下所示：

```rust
// 创建一个新的电路变量
let a_var = MyType::new_variable(cs, || Ok(some_value), AllocationMode::Witness);

// 用它做一些事情...

// 从电路外获取值
let a_val = a_var.value().unwrap_or_default();

// 潜在地用这个值做一些重要的事情...

// 将该值重新插入电路中
let b_var = OtherType::new_variable(cs, || Ok(a_val), AllocationMode::Witness);

```

#### 标签分析来救援

众所周知，形式验证方法通常过于复杂，无法用于大多数项目。因此，它们的发展主要用作公司吸引新客户、获得政府资助和吸引研究人员为他们工作的营销工具。

然而，有一种趋势是使安全工具对开发者真正有用。这个想法是在开发者所在的地方与他们见面。你可以在 [Towards making formal methods normal: meeting developers where they are](https://alastairreid.github.io/papers/hatra2020.pdf) 中阅读更多关于这方面的内容。这方面的例子包括更易于使用的形式验证工具（如 [Verifpal](https://verifpal.com/)）或集成分析工具（如 [模糊测试如何直接集成到 Golang 中](https://go.dev/security/fuzz/)，或 [Rust 中用于属性测试的良好库](https://github.com/proptest-rs/proptest)）。

[MIRAI](https://github.com/facebookexperimental/MIRAI/tree/main) 是另一个例子，它最初是 Herman Venter 创建的一个工具，用于在 libra/diem 区块链中强制执行不变量。虽然 MIRAI 提供了各种功能，但我今天感兴趣的是它的 **标签分析** 功能。

让我用下面的例子来解释什么是标签分析：想象一下你的程序接受用户输入，它希望在这些输入被清理或正确验证之前被认为是危险的。使用标签分析，我们可以将用户输入标记为 **脏的**，然后在程序的重要位置验证它们操作的值是否没有 **脏的** 标签。相反，我们可以验证重要的函数是否只对具有 **干净的** 标签的值进行操作，这些标签将在清理/验证函数中添加。

（有人可能会争辩说，在类型语言中，你可以通过为脏值和干净值创建不同的类型来做同样的事情，但这仍然不够。代码中的更改或人为错误仍然可能允许有效的程序在脏值上执行。如果正确实施，标签分析将以详尽的方式传播标签。如果你复制、克隆，甚至基于一个值做一些事情，标签将被传播到新值。）

使用 MIRAI，我们可以通过将标签放置在 `R1CSVar::value()` 函数中，将“电路外”标签添加到任何从电路中出来的值：

```rust
##![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

##[macro_use]
extern crate mirai_annotations;

use mirai_annotations::{TagPropagation, TagPropagationSet, TAG_PROPAGATION_ALL};

struct OutOfCircuitTaintKind<const MASK: TagPropagationSet> {}

/// 我们的标签带有所有传播集
type OutOfCircuitTaint = OutOfCircuitTaintKind<TAG_PROPAGATION_ALL>;

impl R1CSVar<Fq> for MyVar {
    type Value = MyValue;

fn value(&self) -> Result<Self::Value, SynthesisError> {
        // 已截断...

add_tag!(&res, OutOfCircuitTaint);
        Ok(res)
    }
}

```

另一方面，我们可以通过检测 `AllocVar::new_variable()` 函数中的标签来检测何时这样的值重新进入电路：

```rust
impl AllocVar<MyValue, Fq> for MyVar {
    fn new_variable<T: std::borrow::Borrow<MyValue>>(
        cs: impl Into<ark_relations::r1cs::Namespace<Fq>>,
        f: impl FnOnce() -> Result<T, SynthesisError>,
        mode: ark_r1cs_std::prelude::AllocationMode,
    ) -> Result<Self, SynthesisError> {
        verify!(does_not_have_tag!(&f, OutOfCircuitTaint));

// 已截断...

```

#### 为其他人进行模糊测试

为了完整起见，我应该提到 **模糊测试**，它也是在电路中查找错误的一个很棒的工具。模糊测试是生成奇怪的输入，将它们提供给一个函数，然后看看我们是否可以用它来使该函数崩溃的过程。反复进行。因此，模糊测试是一种动态分析工具——它运行代码来查找错误——并且与我们一直在谈论的静态分析工具截然不同。你永远无法保证你的代码是正确的，你可以运行模糊测试器多久都可以，但仍然找不到一个错误，即使你知道它存在。然而，令人惊讶的是，模糊测试器在查找现实世界代码中的错误方面取得了惊人的成果。

不过，对我们来说，似乎模糊测试对于查找完整性问题（某些输入应该有效但无效）更有用，但不一定对于查找健全性问题（某些输入在不应该有效时有效）有用。

我不会过多地谈论模糊测试，因为它不是这篇文章的主要主题，但我会给你一些指导，如果你有兴趣自己运行一些模糊测试。在 Rust 中，使用 [cargo fuzz](https://rust-fuzz.github.io/book/cargo-fuzz/guide.html) 编写模糊测试器相对容易。我建议不要使用 libfuzzer，而是使用 [AFL++](https://rust-fuzz.github.io/book/afl.html) 作为其后端的模糊测试器。由于证明是一个相对较慢的过程，因此应该尝试通过检查电路可满足性来进行模糊测试。可以使用以下代码来完成此操作（给定一个 `circuit` 变量）：

```rust
let cs = ark_relations::r1cs::ConstraintSystem::<Fq>::new_ref();
cs.set_optimization_goal(ark_relations::r1cs::OptimizationGoal::Constraints);

let satisfied1 = circuit.generate_constraints(cs.clone()).is_ok();
let satisfied2 = cs.is_satisfied().is_ok();
if should_work {
    assert!(satisfied1 && satisfied2);
} else {
    assert!(!satified1 || !satisfied2);
}

```

在大多数情况下，你将不得不使用 [结构化模糊测试](https://rust-fuzz.github.io/book/cargo-fuzz/structure-aware-fuzzing.html) 以指导 cargo fuzz：因为它只了解如何生成“随机”字节串，因此它需要一些关于如何将其转换为私有和公共输入的指导，以便正确地模糊测试电路。

当然，这些不是我们可以使用的唯一工具。请继续关注，以便在下一篇博文中了解更多关于我们内部工具的信息！

>- 原文链接： [blog.zksecurity.xyz/post...](https://learnblockchain.cn/article/17846/boomerang)
>- 登链社区 AI 助手，为大家转译优秀英文文章，如有翻译不通的地方，还请包涵～

zkApps（零知识应用）是指计算机程序的可证明转换。也就是说，它们应该像它们旨在代表的计算机程序一样运行，同时提供正确的执行证明，这些证明可以伴随程序输出。但是，正如我们之前讨论过的，将程序转换为可证明的程序并不是一个简单的过程。为了证明执行，zkApps 尝试“见证”执行跟踪的所有重要部分。它们试图断言原始应用程序中指定（显式或隐式）的每个角落。这里的关键词是“所有”和“每个”，因为如果 zkApp 的断言中缺少原始程序的哪怕是最微小的部分，也可能发生错误。

在本文中，我们想讨论 回旋镖值，这是编写 zkApp 时出现的一种陷阱的例子。什么是回旋镖值？它们会产生什么样的错误？我们能用它们做什么？继续阅读！

混合电路内和电路外逻辑

开发者编写 zkApps 是为了用更高级的语言编码他们想要见证的逻辑。这些更高级的语言可以采取不同的形式（正如我们在这篇文章中描述的），并且它们中的许多通常会将非电路（或电路外）逻辑与电路（或电路内）逻辑混合在一起。

为什么有人甚至想要这样的东西的典型例子（或者混合电路外和电路内逻辑意味着什么）是除法例子，在这种情况下，更容易在电路外计算除法的结果，然后像它从天而降一样提供它。

这是除法函数通常在 zkApps 中编写的方式，在一些 python 伪代码中：

def divide(a_var, b_var):
    # 在电路外计算除法
    c = a_var.value() / b_var.value()

    # 见证 / 将电路外值插入电路中
    c_var = new_var(c)

    # 约束它为除法的正确结果
    assert(c_var * b_var == a_var)

    return c

如果这不能立即让你理解，请这样考虑：zkApp 在编译时编码了对变量的一些断言。这里它将编码这样一个事实，即存在一个变量 c_var，只要它满足 c_var * b_var == a_var，它就可以取任何值。

在运行时（或证明时），当我和你想要执行程序并为其创建证明时，我们将为 a_var 和 b_var 提供实际值，并基于此创建证明。类似地，将为 c_var 提供一个值，该值将基于上面的电路外逻辑计算。

重要的是，divide 函数 定义了编译时逻辑和运行时逻辑。虽然编译时是证明者和验证者都做的事情，但运行时逻辑是只有证明者运行的东西，因此恶意证明者可以决定做他们想做的任何事情。特别是，他们不必像程序中描述的那样将 c 计算为 a / b！

变量的生命周期和链接问题

在我们上面的程序中，一个试图将 c 计算为除 a / b 之外的任何东西的恶意证明者将会失败，因为电路检查除法是否正确。删除断言，你将得到一个约束不足的电路（这是一个错误）。在本文中，我们对属于此类约束不足电路错误的一类问题感兴趣。

但是这根线可以被切断。例如，想象一下下面的伪代码：

## 创建一个新的电路变量
a_var = new_var(some_value);

## 用它做一些事情...

## 从电路外获取值
a_val = a_var.value()

## 潜在地用这个值做一些重要的事情...

## 将该值重新插入电路中
b_var = new_var(a_val)

这是一个相当笼统和模糊的例子，但它应该足以说明我的观点。在这里，你应该能够判断出有些不对劲。如果不能，可以花几分钟思考一下。

问题在于上面的程序向证明者发出了以下指令：“观察a_var的运行时值，然后将其重新插入程序中的其他位置（在b_var下）”。如果你是一个恶意的证明者，你可能会听到的是“添加你想要的任何东西作为b_var”。

线被切断了，链接断开了。我们将这些称为 回旋镖值，因为它们离开电路并在稍后重新插入。它们几乎总是不好的。

有趣的是，凭直觉来看，似乎只有 b_var 现在受到约束不足的影响，但实际上它是双向的！也许你想要保持正确的值作为 b_var，但现在你可以使用一个不同的值作为 a_var，因为它不再与 b_var 的正确值相关联。

换句话说，如果 a_var 和 b_var 的正确值是数字 5，那么一个恶意的证明者可以决定保持 b_var.value() = 5 并将 a_var 的值更改为其他值，或者他们可以决定保持 a_var.value() = 5 的值并将 b_var 更改为其他值。

有关这种类型的错误可能产生的影响的示例，你可以查看我们对 Penumbra 的公开审计，我们在其中发现了一个导致双重支出攻击的回旋镖值。今天，我们将研究如何在 Rust 堆栈中检测此类错误，特别是使用 Arkworks 的 R1CS 库 r1cs-std 的堆栈。

R1CS-std 的 ABC

当使用 r1cs-std 编写电路时，我用来创建新变量以及获取变量运行时值的上述伪函数是通过使用两个函数 new_variable() 和 value() 实现的。这两个函数位于开发者可以在他们自己的自定义类型上实现的两个不同的 trait 中。

这是 new_variable：

pub trait AllocVar&lt;V, F: Field>
where
    Self: Sized,
    V: ?Sized,
{
    /// 在 `ConstraintSystem` `cs` 中分配一个新的 `Self` 类型的变量。
    /// 分配模式由 `mode` 决定。
    fn new_variable&lt;T: Borrow&lt;V>>(
        cs: impl Into&lt;Namespace&lt;F>>,
        f: impl FnOnce() -> Result&lt;T, SynthesisError>,
        mode: AllocationMode,
    ) -> Result&lt;Self, SynthesisError>;

正如你所看到的，它没有接受一个值，而是接受一个函数/闭包 f，它产生该值（但这只是一个细节）。

这是 value()：

/// 这个 trait 描述了一些核心功能，这些功能对于高级
/// 变量是通用的，例如 `Boolean`s、`FieldVar`s、`GroupVar`s 等。
pub trait R1CSVar&lt;F: Field> {
    /// `Self` 在约束系统中表示的“原生”值的类型。
    type Value: core::fmt::Debug + Eq + Clone;

    /// 返回在底层 `ConstraintSystem` 中分配给 `self` 的值。
    fn value(&self) -> Result&lt;Self::Value, ark_relations::r1cs::SynthesisError>;

因此，如果我们使用 arkworks 的 r1cs-std 库来编写回旋镖示例，它将如下所示：

// 创建一个新的电路变量
let a_var = MyType::new_variable(cs, || Ok(some_value), AllocationMode::Witness);

// 用它做一些事情...

// 从电路外获取值
let a_val = a_var.value().unwrap_or_default();

// 潜在地用这个值做一些重要的事情...

// 将该值重新插入电路中
let b_var = OtherType::new_variable(cs, || Ok(a_val), AllocationMode::Witness);

标签分析来救援

然而，有一种趋势是使安全工具对开发者真正有用。这个想法是在开发者所在的地方与他们见面。你可以在 Towards making formal methods normal: meeting developers where they are 中阅读更多关于这方面的内容。这方面的例子包括更易于使用的形式验证工具（如 Verifpal）或集成分析工具（如模糊测试如何直接集成到 Golang 中，或 Rust 中用于属性测试的良好库）。

MIRAI 是另一个例子，它最初是 Herman Venter 创建的一个工具，用于在 libra/diem 区块链中强制执行不变量。虽然 MIRAI 提供了各种功能，但我今天感兴趣的是它的 标签分析 功能。

让我用下面的例子来解释什么是标签分析：想象一下你的程序接受用户输入，它希望在这些输入被清理或正确验证之前被认为是危险的。使用标签分析，我们可以将用户输入标记为脏的，然后在程序的重要位置验证它们操作的值是否没有脏的标签。相反，我们可以验证重要的函数是否只对具有 干净的 标签的值进行操作，这些标签将在清理/验证函数中添加。

使用 MIRAI，我们可以通过将标签放置在 R1CSVar::value() 函数中，将“电路外”标签添加到任何从电路中出来的值：

##![cfg_attr(mirai, allow(incomplete_features), feature(generic_const_exprs))]

##[macro_use]
extern crate mirai_annotations;

use mirai_annotations::{TagPropagation, TagPropagationSet, TAG_PROPAGATION_ALL};

struct OutOfCircuitTaintKind&lt;const MASK: TagPropagationSet> {}

/// 我们的标签带有所有传播集
type OutOfCircuitTaint = OutOfCircuitTaintKind&lt;TAG_PROPAGATION_ALL>;

impl R1CSVar&lt;Fq> for MyVar {
    type Value = MyValue;

    fn value(&self) -> Result&lt;Self::Value, SynthesisError> {
        // 已截断...

        add_tag!(&res, OutOfCircuitTaint);
        Ok(res)
    }
}

另一方面，我们可以通过检测 AllocVar::new_variable() 函数中的标签来检测何时这样的值重新进入电路：

impl AllocVar&lt;MyValue, Fq> for MyVar {
    fn new_variable&lt;T: std::borrow::Borrow&lt;MyValue>>(
        cs: impl Into&lt;ark_relations::r1cs::Namespace&lt;Fq>>,
        f: impl FnOnce() -> Result&lt;T, SynthesisError>,
        mode: ark_r1cs_std::prelude::AllocationMode,
    ) -> Result&lt;Self, SynthesisError> {
        verify!(does_not_have_tag!(&f, OutOfCircuitTaint));

        // 已截断...

为其他人进行模糊测试

为了完整起见，我应该提到 模糊测试，它也是在电路中查找错误的一个很棒的工具。模糊测试是生成奇怪的输入，将它们提供给一个函数，然后看看我们是否可以用它来使该函数崩溃的过程。反复进行。因此，模糊测试是一种动态分析工具——它运行代码来查找错误——并且与我们一直在谈论的静态分析工具截然不同。你永远无法保证你的代码是正确的，你可以运行模糊测试器多久都可以，但仍然找不到一个错误，即使你知道它存在。然而，令人惊讶的是，模糊测试器在查找现实世界代码中的错误方面取得了惊人的成果。

我不会过多地谈论模糊测试，因为它不是这篇文章的主要主题，但我会给你一些指导，如果你有兴趣自己运行一些模糊测试。在 Rust 中，使用 cargo fuzz 编写模糊测试器相对容易。我建议不要使用 libfuzzer，而是使用 AFL++ 作为其后端的模糊测试器。由于证明是一个相对较慢的过程，因此应该尝试通过检查电路可满足性来进行模糊测试。可以使用以下代码来完成此操作（给定一个 circuit 变量）：

let cs = ark_relations::r1cs::ConstraintSystem::&lt;Fq>::new_ref();
cs.set_optimization_goal(ark_relations::r1cs::OptimizationGoal::Constraints);

let satisfied1 = circuit.generate_constraints(cs.clone()).is_ok();
let satisfied2 = cs.is_satisfied().is_ok();
if should_work {
    assert!(satisfied1 && satisfied2);
} else {
    assert!(!satified1 || !satisfied2);
}

在大多数情况下，你将不得不使用结构化模糊测试以指导 cargo fuzz：因为它只了解如何生成“随机”字节串，因此它需要一些关于如何将其转换为私有和公共输入的指导，以便正确地模糊测试电路。

当然，这些不是我们可以使用的唯一工具。请继续关注，以便在下一篇博文中了解更多关于我们内部工具的信息！