Sonobe 2026 更新第一部分:审计报告
本文总结了Sonobe加密库的审计结果,该库实现了折叠方案和IVC。审计由人类和AI审计员共同进行,覆盖了Nova、CycleFold等核心模块。发现了两项严重漏洞(C-01和C-02),可能导致IVC验证完全被绕过。其他严重程度的问题包括R1CS结构不检查、错误的状态绑定等。审计表明人类和AI在发现不同类型漏洞上互补。文章详细描述了每个bug及其修复。
Winderica
本文最初发布于 github.com
在 Sonobe 首个版本发布之前,我们委托了一位人类审计师和一位 AI 审计师对折叠方案和 IVC 库进行了审计。本文总结了他们的发现。
概述
Sonobe 是一个用于折叠方案和 IVC 的密码学库,由 0xPARC 和 PSE 开发,目前由 @winderica 维护。
在过去的一年里,该库进行了重构,以改善模块化和用户体验,现在我们计划发布第一个 crates.io 版本。我们相信折叠方案将成为未来可扩展和隐私区块链的基础设施,并希望确保我们的库足够安全,能够支持各种应用。
为此,我们与人类审计师 Aleph_v(Twitter:https://twitter.com/alpeh_v)和 AI 审计师 V12(https://v12.sh/)合作,以发现 Sonobe 中的潜在漏洞。首次审计的范围有限,以便我们专注于现有下游项目使用的核心方案和功能。具体来说,审计涵盖了以下模块。
- 折叠方案
- Nova
- 折叠到 IVC 的编译器
- CycleFold
- 原语
- 模拟域和群的 Gadget
- 关系与约束系统
- 承诺方案
- 转录本
- 工具函数
此外,AI 审计师还报告了某些超出范围方案中的发现。
我们感谢两位审计师的全面审查,他们在代码库中识别出了多个漏洞和需要改进的领域。本报告汇总了人类和 AI 审计的发现,总结了它们的影响和修复状态,并对根本原因进行了事后分析。我们还比较了两种审计方法,突出了它们的重叠之处以及各自优势的差异,旨在为考虑采用 AI 辅助审计工具的团队提供有用的背景信息。
发现汇总
下表总结了范围内的发现。每个错误都被分配了一个形式为 <严重性>-<索引> 的稳定标签,使用其最终分类。
| 严重性 | 已分类的错误 | 人类发现 | AI 发现 | 双方共同发现 |
|---|---|---|---|---|
| 严重 | 2 | — | — | C-01, C-02 |
| 高 | 2 | — | H-02 | H-01 |
| 中 | 4 | M-01, M-02, M-03, M-04 | — | — |
| 低 | 4 | L-01, L-04 | L-03 | L-02 |
| 无效 | 6 | I-02, I-04, I-05 | I-01, I-03, I-06 | — |
以下对报告中两位审计师表现、重叠之处以及失败模式差异进行综合分析。
关键数据
仅统计范围内的发现(AI 提交的超出范围发现将在末尾单独说明):
| 指标 | 人类 | AI | 双方 |
|---|---|---|---|
| 贡献的有效发现 | 10 / 12 (83%) | 6 / 12 (50%) | 4 / 12 (33%) |
| 提交的无效发现 | 3 | 3 | 0 |
| 总提交数 | 13 | 9 | 4 |
| 精确率 (有效/总计) | 77% | 67% | 100% |
| 独特有效发现 (唯一报告者) | 6 | 2 | — |
加上 6 个 AI 提交的超出范围发现(根据报告自身评估,5 个有效,1 个无效),AI 的整体精确率提升至约 73% (11/15)。共同发现的错误 100% 有效——每个共同报告的错误确实存在。
对审计方法的启示
- 两位审计师相辅相成。
人类审计师与 AI 审计师的组合取得了回报:8 个有效发现仅来自一方。这种差异很重要。如果我们只使用一位审计师:
- 仅使用人类: 会漏掉 H-02(一个 R1CS 恐慌/API 边界的可靠性泄露)和 L-03(一个 Poseidon 拒绝服务/恐慌问题)。两者都面向下游,不在 IVC 关键路径上。
- 仅使用 AI: 会漏掉所有四个中等问题和四个低等问题中的两个:模拟算术和 RLC 集群,以及 Fiat-Shamir 域分隔符。
单一审计师的审查会留下重大缺口。除了严重类别外,两位审计师发现了大致不同类型的错误。
- 认真对待共同报告的错误。
重叠正好落在最需要冗余的地方:两个严重发现。这些错误会破坏协议的整体流程,因此独立确认非常有价值。
每个共同报告的发现都是有效的。当两位审计师独立标记同一个表面时,它确实存在问题。这是在未来的审查中并行运行两条流水线的一个很好的理由。
- 人类审查在数学密集的原语和电路错误方面更强。
中等和低等类别往往是微小的完备性和可靠性错误藏身之处。在这个快照中,AI 漏掉了许多此类错误。人类审计师发现了需要更深层次数学或密码学推理的问题:
- M-02: ${\rm gcd}(\alpha, p-1) \neq 1$ 使得 S 盒不是双射。这需要理解 Poseidon 的安全性论证。
- M-03:
enforce_congruent使用了错误的商边界:x/m而不是(x−y)/m。这需要追踪一个带符号算术的不变量。 - M-04: 域元素零在包含上界的情况下有两种表示,削弱了 Fiat-Shamir 挑战的采样。这需要将一个差一错误与可靠性联系起来。
- L-04:
enforce_not_equal应该要求至少一个 limb 不同,而不是所有 limb。这是一个量词反转错误,只有在理解该 gadget 要证明什么时才会显现出来。
- AI 扫描在公共 API 边界处有用。
H-02 和 L-03 是真正的信任边界错误,以数学为重点的审查很容易低估它们。AI 捕获了接口层面的问题,表现为恐慌或未检查的输入处理:
- H-02:
R1CS::new接受格式错误的矩阵,因此列索引超出赋值向量范围会通过z[*col]触发 Rust 恐慌。 - L-03:
poseidon_custom_config将未经检查的rate、capacity和full_rounds值转发给 arkworks,导致assert_eq!恐慌或无限分配。
- 人类的误报仍然有用。
人类审计师发现的无效发现是合理的担忧,而非噪音。关闭它们需要真正的密码学或协议层面的理由。
- I-02, 曲线 cofactor: 审计师合理地标记了一个看起来缺失的子群检查。解决它需要一个非平凡的 Hasse 界论证,证明在此设置下 cofactor 被迫为 1。
- I-04, 平凡 $<2,0>$ 实例: 对平凡运行实例可能满足松弛 R1CS 的担忧是合理的。协议设计者必须排除这种情况;基于折叠的 IVC 确实排除了它。
- I-05, 128 位挑战: 生日攻击的担忧足够合理,以至于在与原作者讨论后才关闭。
- 当协议范围的上下文重要时,AI 的误报更可能发生。
AI 在发现局部错误方面有效,但在跨多个模块和协议层推理方面较弱。
这体现在 I-03 中。AI 报告称 CycleFold 电路的运行实例被视为不透明。实际上,可靠性是由电路内约束与电路外逻辑共同保证的:它由增广步骤电路吸收到公共输入 x 中,然后由 IVC 验证器检查,但 AI 漏掉了这个跨模块的连接。
范围内的错误
Sponges 和 Transcripts
在 Sonobe 中,我们使用自己的 Sponge 和 Fiat-Shamir Transcript 实现。事实证明,我们的实现不够健壮,如果处理不当会存在一些漏洞。虽然我们已经修补了这些漏洞,但我们的长期计划是迁移到
Transcript 库以获得更好的安全性。
[H-01] [高] (人类, AI) 不同形状的状态产生相同摘要
人类审计师和 AI 审计师(在 F-48560 中)都发现,由于前像的形状信息未被吸收到 Sponge/Transcript 中,两对具有不同形状的初始和当前状态可能产生相同的摘要。这使得攻击者可以获取一个已接受状态转换的证明,并通过
为另一个语义上不同的转换(该转换扁平化为相同的吸收域序列)生成通过验证的证明。
fn verify<FC: FCircuit<Field = Self::Field>>(
Key(dk1, dk2, (hash_config, pp_hash)): &Self::VerifierKey<FC>,
i: usize,
initial_state: &FC::State,
current_state: &FC::State,
Proof(W, U, w, u, cf_W, cf_U): &Self::Proof<FC>,
) -> Result<(), Error> {
// ...
let u_x = sponge
.add(&i)
.add(initial_state)
.add(current_state)
.add(U)
.add(cf_U)
.get_field_element();
if u.public_inputs() != [u_x] {
return Err(Error::IVCVerificationFail);
}
// ...
}
当用户以天真的方式实现步骤电路 trait
时,可以利用此漏洞,使得关联类型 State 和 StateVar 是动态数据结构(例如向量),其大小在步骤电路的多次调用中无法保证相同。
pub trait FCircuit {
// ...
type State: Clone + PartialEq + Absorbable;
type StateVar: GR1CSVar<Self::Field, Value = Self::State>
+ AllocVar<Self::State, Self::Field>
+ AbsorbableVar<Self::Field>;
// ...
}
例如,以下状态对具有不同的形状但产生相同的摘要:
initial_state = vec![1], current_state = vec![2, 3]initial_state = vec![1, 2], current_state = vec![3]
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/257
中修复,现在正确吸收和比较初始状态和当前状态的大小。
[L-01] [低] (人类) 不正确的域分隔符处理
人类审计师还发现了 Transcript 域分隔方法
中的一个错误。我们错误地使用 F::MODULUS_BIT_SIZE.div_ceil(8) 作为 8 位值的块大小,并从每个块派生出一个域元素。这意味着每个块可能包含比域容量更多的位。例如,给定一个 254 位的域阶,每个块有 $ \lceil 254/8 \rceil \times 8 = 256$ 位,可能导致溢出。
fn separate_domain(&self, domain: &[u8]) -> Self {
let mut new_sponge = self.clone();
let mut input = domain.len().to_le_bytes().to_vec();
input.extend_from_slice(domain);
let limbs = input
.chunks(F::MODULUS_BIT_SIZE.div_ceil(8) as usize)
.map(|chunk| F::from_le_bytes_mod_order(chunk))
.collect::<Vec<_>>();
new_sponge.add_field_elements(&limbs);
new_sponge
}
因此,不同的域分隔符可能产生相同的 Sponge/Transcript,导致潜在的碰撞。这不会影响 Sonobe 的 IVC 实现内部使用的域分隔符,但该方法本身是公开的,可能被下游代码调用。虽然 Transcript 碰撞本身不会造成危害,但如果吸收不同的元素,确实会使其他攻击更容易。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/252
中修复,将 div_ceil 替换为 div_floor 以计算正确的块大小。
zip
Sonobe 中有多个地方在不检查长度一致性的情况下对变长向量进行 zip 操作。这非常危险,因为在 Rust 中,zip 返回的迭代器长度取决于较短的输入,后续计算可能不会按预期对剩余项执行。
所有与 zip 相关的错误已在
https://github.com/privacy-ethereum/sonobe/pull/254
中修复,添加了显式的长度检查,并将 zip 替换为 itertools 提供的 zip_eq。
[C-01] [严重] (人类, AI) 松弛 R1CS 验证绕过
人类审计师和 AI 审计师(在 F-48685 中)都发现可以完全绕过对松弛 R1CS 的
。
fn check_evaluation(
w: &RelaxedWitness<&[F]>,
_u: &RelaxedInstance<&[F]>,
v: Self::Evaluation,
) -> Result<(), Error> {
cfg_iter!(w.e)
.zip(&v)
.all(|(e, v)| e == v)
.then_some(())
.ok_or(Error::UnsatisfiedAssignments(
"Evaluation does not match error term".into(),
))
}
这里,我们希望比较攻击者控制的松弛见证 w 中的误差项 e 与评估向量 v。然而,通过提供一个空的误差项 e,评估检查行 .all(|(e, v)| e == v) 可以被跳过,即使见证本身无效,也会产生 Ok(())。
check_evaluation 由折叠方案的判定器算法调用,然后由 IVC 的验证器调用。很明显,此错误使整个 IVC 验证路径不安全。
[L-02] [低] (人类, AI) 切片等价 Gadget 中的静默截断
人类审计师和 AI 审计师(在 F-48590 中)都发现
在不先检查两个切片长度是否相等的情况下进行 zip 操作:
impl<T: EquivalenceGadget<T>> EquivalenceGadget<[T]> for [T] {
fn enforce_equivalent(&self, other: &[T]) -> Result<(), SynthesisError> {
self.iter()
.zip(other)
.try_for_each(|(a, b)| a.enforce_equivalent(b))
}
}
当输入长度不同时,zip 静默地截断到较短的一侧,并且只在公共前缀上强制等价,而较长切片上的尾部元素完全不受约束。该错误目前不会在 Sonobe 内部触发,因为每个内部调用者传递的切片长度在电路综合时已确定。但是,该 gadget 是我们公共 API 的一部分,在动态大小输入的情况下会行为不正确。
[M-01] [中] (人类) 随机线性组合中的静默截断
人类审计师发现 RLC 辅助函数
和 slice_rlc 在不检查长度是否匹配的情况下对输入迭代器和系数切片进行 zip 操作:
fn scalar_rlc(self, coeffs: &[Coeff]) -> Self::Value {
self.zip(coeffs).map(|(v, c)| v * c).sum::<I::Item>()
}
fn slice_rlc(self, coeffs: &[Coeff]) -> Vec<Self::Value> {
let mut iter = self
.zip(coeffs)
.map(|(v, c)| v.iter().map(|x| x.clone() * c));
let first = iter.next().unwrap();
iter.fold(first.collect(), |acc, v| {
acc.into_iter().zip(v).map(|(a, b)| a + b).collect()
})
}
两个辅助函数都静默地截断到两个迭代器中较短的一个。它们目前不会在任何范围内的代码路径上被调用,但审计师出于谨慎考虑将其标记:随机线性组合经常用于在许多折叠方案的关键组合点将并行动作绑定在一起,因此静默的长度不匹配会擦除部分输入并引入可靠性缺口。在电路内上下文中,同样的不匹配会综合出一个欠约束的电路。
哈希函数
存在一些担忧,即 Sonobe 支持的哈希函数不安全,要么是由于对哈希函数本身的攻击,要么是由于潜在的配置错误导致。
[I-01] [无效] (AI) Griffin
AI 审计师(在 F-48679 中)报告说
被公开为一等 Transcript 后端,尽管 Griffin 排列已被破解。AI 担心下游用户可能选择 Griffin,并从不再像随机预言机一样运作的原语中获得 Fiat-Shamir 挑战。
我们认为这是无效的,因为
已经明确警告底层排列已被破解,不得在生产中使用:
//! Implementation of the Griffin circuit-friendly hash function and its
//! parameter generation, as well as out-of-circuit widgets and in-circuit
//! gadgets for permutation, hashing, sponges, and transcripts.
//!
//! According to the Griffin [paper], it is very efficient in terms of the
//! number of constraints, but later an [attack] on Griffin and similar hash
//! functions was discovered.
//! Therefore, it is recommended to avoid using Griffin in production.
该实现仅保留用于基准测试和研究目的,并且内部代码中没有路径将其用于证明或验证。
[L-03] [低] (AI) Poseidon 配置生成函数的未检查输入
AI 审计师(在 F-48670 中)发现
将 full_rounds、partial_rounds、rate 和 capacity 直接转发给 arkworks,未进行任何验证:
pub fn poseidon_custom_config<F: PrimeField>(
full_rounds: usize,
partial_rounds: usize,
alpha: u64,
rate: usize,
capacity: usize,
) -> PoseidonConfig<F> {
let (ark, mds) = find_poseidon_ark_and_mds::<F>(
F::MODULUS_BIT_SIZE as u64,
rate,
full_rounds as u64,
partial_rounds as u64,
0,
);
PoseidonConfig::new(full_rounds, partial_rounds, alpha, mds, ark, rate, capacity)
}
两个具体后果:
- 任何
capacity != 1都会在PoseidonConfig::new内部触发一个assert_eq!恐慌,因为find_poseidon_ark_and_mds硬编码了rate + 1的状态宽度,而PoseidonConfig::new随后断言一个rate + capacity的宽度。因此,只要调用者传递任何其他容量,该函数就变成了一个恐慌原语。 - 较大的
full_rounds、partial_rounds或rate值会导致find_poseidon_ark_and_mds急切地分配一个大小为(full_rounds + partial_rounds) * (rate + 1)的ark表和一个大小为(rate + 1)^2的方阵mds,提供了一个无界拒绝服务原语。
这仅当下游消费者将攻击者控制的值路由到配置构建器时才有影响。Sonobe 本身不依赖于任何特定配置,仅使用 poseidon_canonical_config 中的规范参数进行单元测试。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/256
中修复,现在通过遵循论文的参考实现来计算参数。
[M-02] [中] (人类) Poseidon 配置生成可能产生不安全的实例
人类审计师指出,
将 alpha 直接转发给 PoseidonConfig::new,而未验证它是否与 F::MODULUS - 1 互质:
pub fn poseidon_custom_config<F: PrimeField>(
full_rounds: usize,
partial_rounds: usize,
alpha: u64,
rate: usize,
capacity: usize,
) -> PoseidonConfig<F> {
// ... 没有 gcd(alpha, F::MODULUS - 1) 检查 ...
PoseidonConfig::new(full_rounds, partial_rounds, alpha, mds, ark, rate, capacity)
}
当 ${\rm gcd}(F:MODULUS-1, \alpha) \neq 1$ 时,S 盒 $x \mapsto x^\alpha$ 在 $F$ 中不是一个置换,结果产生的 Poseidon 实例不再具有抗碰撞性。Sonobe 使用的默认质数域(BN254 和 Grumpkin 标量)满足互质要求,但辅助函数是泛型于 F: PrimeField 的,如果使用不同的域实例化,则会静默地产生不安全的配置。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/256
中修复,现在在构建 Poseidon 配置时强制执行 alpha 和 F::MODULUS - 1 的互质性。
模拟域/群 Gadget
Sonobe 实现了用于模拟域和群元素的电路内 Gadget。CycleFold 实例的验证涉及模拟域元素及其操作,并且模拟群元素也需要用于在增广步骤电路中表达主实例。
因此,我们模拟 Gadget 的安全性直接影响增广步骤电路的安全性。审计师报告的大多数错误仅影响完备性,即阻止诚实的证明者为某些正确的见证生成有效证明。然而,也有一个可靠性错误,允许恶意证明者为不正确的见证生成有效证明。
[L-04] [低] (人类) 过度约束的 enforce_not_equal
人类审计师标记了我们在 crates/primitives/src/algebra/field/emulated.rs#L803-L817 中针对 LimbedVar 的自定义 enforce_not_equal 重写中的一个完备性错误:
fn enforce_not_equal(&self, other: &Self) -> Result<(), SynthesisError> {
if self.limbs.len() != other.limbs.len() {
return Err(SynthesisError::Unsatisfiable);
}
if self.bounds.len() != other.bounds.len() {
return Err(SynthesisError::Unsatisfiable);
}
for i in 0..self.limbs.len() {
if self.bounds[i] != other.bounds[i] {
return Err(SynthesisError::Unsatisfiable);
}
self.limbs[i].enforce_not_equal(&other.limbs[i])?;
}
Ok(())
}
该循环强制每个单独的 limb 不相等,而正确的关系是至少有一个 limb 必须不同。因此,像 [0, 1] 和 [0, 2] 这样的 limb 对在此 gadget 下不能被证明不同,尽管它们显然是不同的。该重写在现有代码库中未被调用,但暴露给原语 crate 的其他消费者。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/253
中修复,删除了过度约束的重写,并回退到默认的 EqGadget::enforce_not_equal 实现。
[M-03] [中] (人类) enforce_congruent 中的错误商边界
人类审计师在
中发现了另一个完备性错误,该 gadget 断言两个 limb 数模一个质数同余:
pub fn enforce_congruent<const RHS_ALIGNED: bool>(
&self,
other: &LimbedVar<Base, Target, RHS_ALIGNED>,
) -> Result<(), SynthesisError> {
let cs = self.cs();
let m = BigInt::from_biguint(Sign::Plus, Target::MODULUS.into());
// 提供商作为提示
let q = LimbedVar::new_variable_with_inferred_mode(cs.clone(), || {
let x = compose(self.limbs.value().unwrap_or_default());
let y = compose(other.limbs.value().unwrap_or_default());
Ok((
(x - y).div_floor(&m),
Bounds(self.lbound().div_floor(&m), self.ubound().div_floor(&m)),
))
})?;
// ...
}
诚实的商是 $q = (x - y) / m$,但提示变量的边界是 $({\rm self.lbound()} / m, {\rm self.ubound()} / m)$,即仅 $x / m$ 的范围,忽略了 $y$ 的减法。举一个简单的例子,证明 $9 \equiv 2 \pmod{7}$ 需要见证 $q = (2 - 9) / 7 = -1$,而从 ${\rm self} = 2$ 推导出的边界坍缩为 $(0, 0)$ 并拒绝任何负值。因此,这个(真实的)陈述是不可证明的。该 gadget 用于参与判定器证明的相等性检查类,但不在核心折叠方案/IVC 路径上。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/253
中修复,现在商边界从 $(x - y) / m$ 而非仅从 $x / m$ 推导。
[M-04] [中] (人类) 域元素的错误上界
当通过 AllocVar for LimbedVar 在定义于域 $F$ 上的电路中
到域 $G$ 时,limb 值的上界是包含 $G:MODULUS$ 的:
impl<F: SonobeField, G: SonobeField, Cfg> AllocVar<G, F> for LimbedVar<F, Cfg, true> {
fn new_variable<T: Borrow<G>>(
cs: impl Into<Namespace<F>>,
f: impl FnOnce() -> Result<T, SynthesisError>,
mode: AllocationMode,
) -> Result<Self, SynthesisError> {
Self::new_variable(
cs,
|| {
f().map(|v| {
(
BigInt::from_biguint(Sign::Plus, (*v.borrow()).into()),
Bounds(Zero::zero(), G::MODULUS.into().into()),
)
})
},
mode,
)
}
}
人类审计师观察到,这允许域元素零有两种不同的 limb 表示:规范的 $0$ 和 $G:MODULUS \equiv 0 \pmod{G::MODULUS}$。当该 limb 变量随后被吸收到 Transcript 中时,这两种表示序列化为不同的位串,因此恶意证明者可以在每个允许零的位置选择两种不同的 Fiat-Shamir 挑战。这打破了 Fiat-Shamir 变换的单挑战假设,允许证明者采样多个多项式打开点而不是一个,并将可靠性界限按 Transcript 中允许零的位置数量比例降低。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/253
中修复,现在在分配模拟 $G$ 元素时使用 $G:MODULUS - 1$ 作为上界,使得域元素零具有唯一表示。
[I-02] [中 -> 无效] (人类) 缺失曲线点的素数阶检查
人类审计师指出,Sonobe 的电路从未断言传递给承诺相关 Gadget 的曲线点位于配置曲线的素数阶子群中。对于具有非平凡 cofactor 的曲线,攻击者可以提供位于小阶子群中的承诺;随后的标量乘法将返回微小范围内的值,攻击者可以使用小阶子群大小(而非素数阶操作的全 128 位代价)搜索能够补偿先前无效承诺的 $\rho$ 抵消。
我们认为这对于范围内的配置是无效的:我们总是要求 CycleFold 基于 IVC 的曲线循环,这是由 Rust 编译器强制执行的。某些曲线链的 cofactor 确实大于 1,但曲线循环具有非平凡 cofactor 在数学上是不可能的,这是 Hasse 界的直接推论。
一个 2-循环由椭圆曲线 $E_1/ \mathbb{F}{p_1}$ 和 $E_2/ \mathbb{F}{p_2}$ 组成,其中每条曲线的素数阶子群阶等于另一条曲线的基域:
$r_1 = p_2, \quad r_2 = p_1$
且 $#E_i = h_i \cdot r_i$ (cofactor $h_i$)。根据 Hasse 定理,$#E_i = p_i + 1 - t_i$ 且 $|t_i| \le 2\sqrt{p_i}$。代入得:
$h_1 \cdot p_2 = p_1 + 1 - t_1$
$h_2 \cdot p_1 = p_2 + 1 - t_2$
从第一个方程消去 $p_2$ 并代入第二个方程得:
$p_1 (h_1 h_2 - 1) = 1 - t_1 + h_1 (1 - t_2)$
左侧随 $p_1$ 线性增长(当 $h_1 h_2 \ge 2$ 时)。
右侧有界:
$|1 - t_1 + h_1 (1 - t_2)| \le 1 + 2\sqrt{p_1} + h_1 + 2 h_1 \sqrt{p_2} \approx O(\sqrt{p_1})$
对于大的 $p_1$,$p_1 \gg O(\sqrt{p_1})$,因此方程无解,除非 $h_1 h_2 = 1$,即 $h_1 = h_2 = 1$。
即使是最小的非平凡情况 ($h_1 = 2, h_2 = 1$),我们可以计算出解仅当 $p_1 \lesssim 23$ 时存在。对于密码学规模的任何东西(128 位以上质数),非单位 cofactor 是不可能的。
R1CS
作为一种流行的约束系统,R1CS 受大多数折叠方案支持。通常 R1CS 结构是诚实生成的,例如由可信方或验证者生成。然而,在它们可能由恶意证明者指定的场景中,我们必须仔细检查 R1CS 矩阵。
[H-02] [高] (AI) 未检查的 R1CS 结构
AI 审计师(在 F-48681 中)发现
接受一个 R1CSConfig 加上稀疏矩阵,但未验证存储的行计数和列索引是否满足声明的算术化维度:
pub fn new(cfg: R1CSConfig, [A, B, C]: [Matrix<F>; 3]) -> Self {
Self { cfg, A, B, C }
}
AbstractNova::generate_keys 的两种变体都将格式错误的 R1CS 保留在生成的密钥材料中。随后在 R1CS::evaluate_at 中的评估信任列元数据,并使用直接的 z[*col] 索引:
self.evaluate_rows(|((a, b), c)| {
let az = a.iter().map(|(val, col)| z[*col] * val).sum::<F>();
let bz = b.iter().map(|(val, col)| z[*col] * val).sum::<F>();
let cz = c.iter().map(|(val, col)| z[*col] * val).sum::<F>();
// ...
Ok(az * bz - z[0] * cz)
})
两个不同的下游症状:
- 原生和电路内评估路径信任实际存在的行,因此缩短的矩阵被静默截断,强制的关系弱于
R1CSConfig所声明的。结合基于zip的check_evaluation,格式错误的运行实例可以擦除尾部的误差项。 - 赋值向量范围之外的列索引会通过索引表达式
z[*col]产生恐慌,而不是类型化错误。格式错误的R1CS在密钥生成后仍然存在,恐慌会在后续的decide_*、sample或prove调用中出现。
Sonobe 自己的预处理管道仅从合成的 arkworks 电路构造 R1CS 实例,这保证了良好形成的维度。该错误主要影响公共 API 边界,当下游消费者反序列化插件提供或攻击者控制的电路时才会触发。推荐的修复方法是在 R1CS::new 中验证行计数和列索引,然后再存储矩阵。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/260
中修复,我们默认添加了对 R1CS 结构创建的有效性检查。
IVC
重新设计后,Sonobe 现在基于 CycleFold 提供了一个编译器,可以自动将支持的折叠方案转换为 IVC,而无需手动实现逻辑。
因此,一个安全的编译器对于它生成的所有 IVC 方案的安全性至关重要。
[C-02] [严重] (人类, AI) 基础案例未能锚定声称的初始状态
人类审计师和 AI 审计师(在 F-48689 中)都发现,增广电路没有将已执行的转换绑定到步骤 $i = 0$ 时声称的起始状态。在
AugmentedCircuit::compute_next_state
中,initial_state 和 current_state 都作为普通见证分配,并且唯一的基础案例处理包括交换为虚拟运行实例:
let initial_state = FC::StateVar::new_witness(cs.clone(), || Ok(initial_state))?;
let current_state = FC::StateVar::new_witness(cs.clone(), || Ok(current_state))?;
let U_dummy = AllocVar::new_constant(cs.clone(), FS1::RU::dummy(self.arith1_config))?;
// ...
// 1.d. 如果这是基础案例 (`i = 0`),则应该改用虚拟运行实例作为下一个运行实例。
let actual_UU = is_basecase.select(&U_dummy, &UU)?;
// ...
// 2.d. 如果这是基础案例 (`i = 0`),则应该改用虚拟运行实例作为下一个运行实例。
let actual_cf_UU = is_basecase.select(&cf_U_dummy, &cf_UU)?;
// 3. 通过调用步骤电路更新状态。
let (next_state, external_outputs) =
self.step_circuit
.generate_step_constraints(i, current_state, external_inputs)?;
步骤电路始终针对 current_state 见证执行,并且约束系统从未断言 current_state == initial_state,即使当 is_basecase 为真时也是如此。由于 initial_state 仅作为自由见证进入公共哈希 $u.x = H(i, initial_state, current_state, U, cf_U)$,证明者可以在 $i = 0$ 时提供任何隐藏的 current_state,从中运行一个诚实步骤,然后仍将对结果声明与不相关的已宣传 initial_state 进行哈希处理。因此,第一个证明仅证明 $H(1, initial_state, next_state, dummy, dummy)$ 以及折叠关系,而不证明产生 next_state 的实际前驱状态。验证者检查相同的公共哈希和递归一致性条件,因此它接受其初始状态从未被绑定的执行轨迹。
人类审计师用一个具体测试用例演示了这一点,该测试用例执行 $x_i^3 + x_i + 5 = x_{i+1}$ 的步骤,声称初始状态 $x = 0$,但实际上从 $x = 2$ 开始。两步后,系统达到 $3395$ 而不是正确的 $135$,而验证者仍然接受该证明。
此问题已在
https://github.com/privacy-ethereum/sonobe/pull/255
中修复,现在在 $i = 0$ 时有条件地强制 initial_state 和 current_state 之间的相等性。
[I-03] [无效] (AI) 验证者接受错误的次要实例
AI 审计师(在 F-48635 中)报告说
没有从主要证明重新推导 cf_U。相反,它仅通过 FS2::decide_running 检查可满足性,因此恶意调用者可以替换任何有效的次要见证-实例对,而验证者仍会接受该证明。
我们认为这是无效的,因为 cf_U 实际上通过公共哈希链绑定到主要证明。
将 cf_U 与其余公共状态一起吸收:
let u_x = sponge
.add(&i)
.add(initial_state)
.add(current_state)
.add(U)
.add(cf_U)
.get_field_element();
if u.public_inputs() != [u_x] {
return Err(Error::IVCVerificationFail);
}
因此,替换一个不相关的 cf_U 会改变 u_x,验证者在 u.public_inputs() == [u_x] 检查时会拒绝该证明。AI 声称 cf_U 被验证者“视为不透明”是错误的。
[I-04] [中 -> 无效] (人类) $<2, 0>$ 折叠中的平凡实例
人类审计师指出,Nova 的
(该电路折叠两个运行实例,而非一个运行实例和一个传入实例)没有强制要求如果任一输入实例的 u = 0,则 cm_e = O 和 cm_w = O:
fn verify_hinted(
_vk: &Self::VerifierKey,
transcript: &mut impl TranscriptGadget<CM::ConstraintField>,
[U1, U2]: [&Self::RU; 2],
_: [&Self::IU; 0],
proof: &Self::Proof<2, 0>,
) -> Result<(Self::RU, Self::Challenge), SynthesisError> {
let rho_bits = transcript.add(&(U1, U2))?.add(proof)?.challenge_bits(B)?;
let rho = CM::ScalarVar::from_bits_le(&rho_bits)?;
Ok((
Self::RU {
u: (U2.u.clone() * &rho + &U1.u).try_into()
.map_err(|_| SynthesisError::Unsatisfiable)?,
cm_e: /* ... 与 rho^2 折叠 ... */,
cm_w: /* ... 与 rho 折叠 ... */,
x: /* ... 与 rho 折叠 ... */,
},
rho_bits.try_into().unwrap(),
))
}
在松弛 R1CS 中,方程 $Az \circ Bz - u \cdot Cz = e$ 可以通过设置 $u = 0$ 和 $e = Az \circ Bz$ 对任意赋值平凡地满足,因此允许此类平凡松弛实例进入折叠会破坏累加器的可靠性。在默认的 $<1, 1>$ 折叠模式下,这被隐式阻止:一个 $u = 0$ 的松弛实例会破坏增广电路中的哈希链,并且不能作为运行实例传入。而 $<2, 0>$ 验证者电路(折叠两个松弛实例)没有等效的防护。
然而,我们认为这是无效的,原因如下。
- 一个有效的运行实例完全有可能 $u = 0$ 但 $cm_e \neq O$ 和 $cm_w \neq O$,因为这些组件只是通过随机线性组合计算得出的。$u = 0$ 看起来确实是松弛 R1CS 方程的一个平凡情况,但类似地,对于加密方案,一个恰好是明文的密文看起来也是一个平凡情况。然而,我们不应该拒绝此类平凡情况,因为这会给对手一个提示,即明文必须与密文不同,在我们的场景中也是如此。
- IVC 总是需要 $<1, 1>$ 折叠,其中运行实例通过累积传入实例来更新,并且永远不会由对手直接提供。我们公开 $<2, 0>$ 折叠 API,因为一些高级用例可能需要基于折叠的 PCD,就像我们在 PlasmaBlind 中所做的那样。然而,PCD 中的运行实例最终也应来自传入实例,而不是来自对手。我们假设下游集成者有足够的经验来确保这一点,这是一个合理的假设,因为此类用例已经需要对 IVC 和 PCD 协议有深入理解。
- 对基于折叠的 PCD 的原生支持已计划,但目前超出范围。在实现此功能时,我们将确保 $<2, 0>$ 折叠得到妥善处理。
挑战大小
存在关于 Nova 挑战大小的担忧,该大小由 AbstractNova 中的常量泛型 CHALLENGE_BITS 配置。
pub struct AbstractNova<CM, TF, const CHALLENGE_BITS: usize = 128> {
_t: PhantomData<(CM, TF)>,
}
[I-05] [无效] (人类) 默认挑战大小太小
人类审计师提出担忧,默认挑战大小 CHALLENGE_BITS = 128 可能太小,由于生日攻击仅提供 64 位安全性。
我们认为这是无效的,在与 Nova 的作者之一 Srinath Setty 讨论后。他提到,如果挑战位是通过在 256 位域中采样 Fiat-Shamir 挑战并将其位分解截断为 128 位获得的,那么安全级别仍应为 128 位,而这正是我们正在做的。
[I-06] [无效] (AI) 用户可控的挑战大小
AI 审计师发现了两个与用户可控挑战大小相关的潜在问题。具体来说,CHALLENGE_BITS 可由用户控制,但代码未检查任何错误配置,可能导致以下攻击:
- (F-48613) 当
CHALLENGE_BITS = 0时,攻击者可以伪造从未发生过的历史的递归证明。 - (F-48510) 当
CHALLENGE_BITS大于或等于主曲线的基域大小时,同一个挑战可以对应多个因整个域模数而不同的位串。
我们认为两种攻击都无效,因为我们提供了安全的默认值,并假设如果用户更改默认值,这是他们的责任。尽管如此,我们将改进文档,并明确告知用户他们应优先使用默认配置,除非他们知道自己在做什么。
范围外的错误
无界验证者分配
AI 审计师(在 F-48642 中)发现 Mova 和 HyperNova 证明和实例中的向量具有攻击者可控制的无界大小,需要在后续 Transcript 操作中进行过多分配。例如,Mova::verify 在算术配置的任何大小不变量被强制执行之前,就消耗了攻击者控制的 proof.h1_coeffs 和 U.r_e.len():
let h1 = DensePolynomial::from_coefficients_vec([&U.v[..], &proof.h1_coeffs].concat());
transcript.add(U);
transcript.add(u);
transcript.add(&proof.cm_w);
let r_e = transcript.challenge_field_elements(U.r_e.len());
transcript.add(&proof.h1_coeffs);
r_e 和密集多项式 h1 的大小直接来自反序列化的证明,因此单个过大的请求会驱使验证者进行过多的挑战挤压和多项式分配。相同的模式影响 MovaProof.h1_coeffs、NIMFSProof.sc_proof / sigmas / thetas 以及跨 Mova::verify 和 HyperNova::verify 的 mova::RunningInstance.r_e。因此,一个将不受信任的证明反序列化到这些公共结构中的服务可能被迫进行无界的内存和 CPU 工作。Mova 和 HyperNova 不在本次审计范围内。
在带符号剩余 limb 边界下的和为零检查不可靠
AI 审计师(在 F-48657 中)发现 crates/primitives/src/algebra/field/emulated.rs 中的 enforce_equal_unaligned 方法通过求和尾部 limb 并强制其和为零来处理 limb 长度不匹配:
// Enforce the remaining limbs to be zero.
// Instead of doing that one by one, we check if their sum is
// zero using a single constraint.
// This is sound, as the upper bounds of the limbs and their sum
// are guaranteed to be less than `F::MODULUS_MINUS_ONE_DIV_TWO`
// (i.e., all of them are "non-negative"), implying that all
// limbs should be zero to make the sum zero.
remaining_limbs[1..]
.iter()
.sum::<FpVar<F>>()
.enforce_equal(&FpVar::zero())?;
Bounds::add_many(remaining_bounds)
.filter_safe::<F>()
.ok_or(SynthesisError::Unsatisfiable)?;
内联注释声称这是可靠的,因为尾部 limb 是非负的,但唯一执行的检查是 Bounds::add_many(remaining_bounds).filter_safe::<F>(),它仅确保总和在带符号域范围内,并接受负下界 (${\rm lb} >= -{\rm MODULUS_MINUS_ONE_DIV_TWO}$)。因此,在 sub_unaligned 或 mul_unaligned 之后,针对带符号的商,恶意证明者可以产生抵消的正负 limb(例如 $(+X, -X, 0, \ldots)$),其域和为零,但表示的整数非零。这绕过了 LimbedVar::modulo 和 LimbedVar::enforce_congruent,它们是 EmulatedFieldVar 背后的归约和等价原语。
此错误仅存在于
中,而不存在于 842b45a 中,因为它已通过 https://github.com/privacy-ethereum/sonobe/commit/7af1d5b2809ae7b2ea473195983c3eeb25529073 修复。
公共参数未绑定到 Transcript
AI 审计师(在 F-48688 中)发现 CycleFoldBasedIVC::generate_keys 将 pp_hash 硬编码为 Zero::zero():
let pp_hash = Zero::zero(); // TODO
该常量贯穿证明者和验证者密钥、T::new_with_pp_hash Transcript 构造以及 AugmentedCircuit::compute_next_state 中的电路内 Sponge。结果,证明和累加器状态没有通过实际公共参数进行域分隔,即使 API 暗示它们应该这样做。因此,只要底层关系仍然可以验证,调用者就可以跨不同参数生成重放或替换证明。
此错误仅存在于
中,而不存在于 842b45a 中,因为它已通过 https://github.com/privacy-ethereum/sonobe/commit/19c220fea449e361173c67e24f8b694a314ac170 修复。
空输入导致 Pedersen Gadget 恐慌
AI 审计师(在 F-48672 中)发现 crates/primitives/src/commitments/pedersen.rs 中的 PedersenGadget::msm 在不检查 $n == 0$ 的情况下立即索引 $g[n - 1]$(在偶数分支中还索引 $g[n - 2]$):
fn msm(g: &[C::Var], v: &[Vec<Boolean<CF2<C>>>]) -> Result<C::Var, SynthesisError> {
let mut res = C::Var::zero();
let n = v.len();
if n % 2 == 1 {
res += g[n - 1].scalar_mul_le(v[n - 1].to_bits_le()?.iter())?;
} else {
res += g[n - 1].joint_scalar_mul_be(
&g[n - 2],
v[n - 1].to_bits_le()?.iter(),
v[n - 2].to_bits_le()?.iter(),
)?;
}
// ...
}
当 $v$ 为空时,$n - 1$ 会使 usize 下溢,并且切片访问立即导致恐慌。两个 CommitmentOpsGadget 实现都调用了 msm,因此电路内 open 路径在综合时遇到空承诺向量时会恐慌。电路外 PedersenKey::commit 静默地接受相同的空向量,因为 ark_ec::VariableBaseMSM::msm_unchecked 截断到较短的切片。因此,一个电路内/电路外信任边界的不匹配使得一个综合攻击者控制的公开路径的下游服务可以被可靠地崩溃。Pedersen Gadget 目前不在 Sonobe 的关键路径上,但公共 API 表面仍然暴露给下游消费者。Pedersen 承诺方案在本审计范围内,但具体的电路内 Gadget 不在范围内,因为它不在 IVC 路径上。
HyperNova 中缺失的维度检查
AI 审计师(在 F-48687 中)发现 HyperNova 的多个验证路径信任攻击者控制的向量长度,而不是强制执行 CCS 形状。例如,HyperNova::verify 直接从 proof.sc_proof.len() 推导出 sumcheck 维度:
let d = V::degree();
let s = proof.sc_proof.len();
let t = V::n_matrices();
// ...
let beta = transcript.challenge_field_elements(s);
// ...
let vp_aux_info = VPAuxInfo {
max_degree: d + 1,
num_variables: s,
};
// ...
let (claimed_eval, r_x_prime) =
SumCheck::verify(sum_v_j_gamma, &proof.sc_proof, &vp_aux_info, transcript)?;
HyperNova2::verify 和 HyperNovaGadget::verify_hinted 镜像了相同的模式,并且在运行实例路径上,HyperNovaKey::check_relation 调用了 eval_relation,后者读取 mle.fix_variables(&u.r_x)[0] 而不检查 u.r_x.len() 是否匹配 log_constraints(),而 check_evaluation 使用 zip 比较预期值与 u.v,因此尾部坐标被静默丢弃。一个 s = 0 的证明可以绕过有意义的 sumcheck 验证。HyperNova 不在本次审计范围内。
MLE 中的空评估恐慌
AI 审计师(在 F-48598 中)报告说 MLEHelper::from_evaluations 直接从 evaluations.len() 计算 log2(l),并在空输入向量上引发恐慌,为任何将攻击者控制的数据转发到该辅助函数的调用者提供了拒绝服务原语。
我们认为这是无效的,因为 arkworks 的 log2 在输入为 0 时显式返回 0。
相关项目

模块化折叠库,支持多种方案和判定器后端
活跃
更多文章 查看全部
Discord Github Twitter Youtube RSS 招聘
- 原文链接: pse.dev/blog/sonobe-upda...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
