本文介绍了MOCA意大利黑客训练营CTF竞赛中一个名为“2+2=5”的密码学挑战,该挑战利用了修改后的Jolt zkVM。挑战要求参与者构造一个无效的RISC-V程序执行证明,利用Jolt库中的漏洞,使得程序输出错误的结果“5”,从而绕过服务器的验证并获得flag。
上周末,我参与了在 MOCA 意大利黑客训练营 期间为 CTF 活动创建一些挑战。 我编写的任务之一是一个名为 “2+2=5” 的密码学挑战,其中涉及到 Jolt zkVM:它涉及到为一个无效的 RISC-V 程序执行制作证明,该程序利用了 Jolt 库的修改版本。
这篇文章将介绍挑战声明和解决方案,如果你想自己尝试解决这个挑战,可以从这里下载原始附件!
Jolt 是一个以 RISC-V ISA 为目标的 zkVM。 要使用 Jolt,我们需要编写两个 Rust 程序:
访客程序被编译和模拟以计算其执行轨迹,这是一个保存所有已执行的有序指令的结构,以及指令执行、内存读取、内存写入等的具体值。 Jolt zkVM 接受执行轨迹,并为其有效性发出证明。 粗略地说,如果输入轨迹编码了访客程序的正确执行,且符合 RISC-V 语义,则证明将被 verifier 接受。
文档中给出了 Jolt 证明系统的架构概述。 Jolt zkVM 中有四个主要组件:
add
指令的执行结果是否真的是操作数的总和。该挑战允许用户与服务器交互,附件包含远程服务的源代码。
.
├── jolt # 修改后的 Jolt crate
├── server # 宿主服务器
│ └── guest # 访客程序
├── diff.patch # 应用于 Jolt 的补丁
├── Dockerfile # Dockerfile 用于运行服务器
└── readme.txt # Readme
要在本地运行它,只需构建 Docker 容器并运行它!
$ docker build . -t two_plus_two
$ docker run -p 5555:5555 -e FLAG="flag{some_secret_value}" -t two_plus_two
服务器是一个 Rust 程序,它将充当 Jolt zkVM 的宿主程序。 它构建访客程序,从用户那里获取访客程序的执行证明并验证它。 除了实际的验证之外,服务器还执行一些额外的检查:
5
,并且如果用户提供了满足这些检查的有效证明,服务器将返回 flag,挑战将被解决!
use jolt_sdk::RV32IHyraxProof;
pub fn main() {
let (_prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();
println!("Can you prove that 2+2=5?");
let line = std::io::stdin().lines().next().unwrap().unwrap();
if line.len() == 0 {
println!("k thx bye");
return;
}
let proof = RV32IHyraxProof::deserialize_from_bytes(
&hex::decode(line).unwrap()
).unwrap();
let inputs = &proof.proof.program_io.inputs;
println!("inputs: {:?}", inputs);
assert_eq!(inputs.len(), 0);
let outputs = &proof.proof.program_io.outputs;
println!("outputs: {:?}", outputs);
assert_eq!(outputs.len(), 1);
assert_eq!(outputs[0], 5); // 2+2 is 5!
let panics = &proof.proof.program_io.panic;
println!("panics: {:?}", panics);
assert!(!panics);
println!("Verifying the proof...");
let is_valid = verify_two_plus_two(proof);
if is_valid {
println!("The proof is valid!");
println!("FLAG: {}", std::env::var("FLAG").unwrap());
} else {
println!("The proof is invalid! :(");
}
}
访客程序是一个计算 2+2
并返回结果的 Rust 程序。
附加到 two_plus_two
函数的 #[jolt::provable]
属性指定此函数实现了一个我们想要证明其执行的访客程序。
此属性将自动生成一些在宿主中可见的附加函数(例如,build_two_plus_two
),这些函数将为宿主提供证明和验证函数。
two_plus_two
函数的主体可能看起来很复杂,它只是将值 2
加载到寄存器中,将其自身相加(即,计算 2+2
),然后返回结果。
访客程序是使用内联汇编编写的,以避免 Rust 编译器执行的优化。
目的是在最终的访客可执行文件中保留 add
指令,但这对挑战的核心影响很小,除了使预期的解决方案稍微容易一些之外。
##![cfg_attr(feature = "guest", no_std)]
##![no_main]
##[jolt::provable]
fn two_plus_two() -> u16 {
let mut n: u16 = 2;
#[cfg(any(target_arch = "riscv32", target_arch = "riscv64"))]
unsafe {
core::arch::asm!(
"li {n}, 2",
"add {n}, {n}, {n}",
n = inout(reg) n,
);
}
#[cfg(target_arch = "x86_64")]
unsafe {
core::arch::asm!(
"mov {n}, 2",
"add {n}, {n}, {n}",
n = inout(reg) n,
);
}
n
}
按照 ISA 语义,此程序将始终返回 4
,这是计算 2+2
的结果。
挑战的重点是制作一个输出为 5
的执行证明!
readme.txt
文件解释了获取修改后的 Jolt 库所采取的步骤。
git clone git@github.com:a16z/jolt.git
cd jolt
## just the latest commit at time of writing
git checkout 0cc7aa31981ff8503fe256706d2aa9c320abd1cd
git apply ../diff.patch
Jolt 存储库按原样获取自上次提交(在编写挑战时),并对其应用了一个补丁。
该补丁可以在 diff.patch
文件中找到:它从 jolt-core/src/r1cs/jolt_constraints.rs
文件中删除了一些行。
diff --git a/jolt-core/src/r1cs/jolt_constraints.rs b/jolt-core/src/r1cs/jolt_constraints.rs
index 5fb0d871..295dce32 100644
--- a/jolt-core/src/r1cs/jolt_constraints.rs
+++ b/jolt-core/src/r1cs/jolt_constraints.rs
@@ -289,13 +289,8 @@ impl<F: JoltField> R1CSConstraintBuilder<F> for UniformJoltConstraints {
// if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
// if (rd != 0 && is_jump_instr == 1) constrain(rd_val == 4 * PC)
-- let rd_nonzero_and_lookup_to_rd =
-+ let _rd_nonzero_and_lookup_to_rd =
+ cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_LookupOutToRd);
-- cs.constrain_eq_conditional(
-- rd_nonzero_and_lookup_to_rd,
-- JoltIn::RD_Write,
-- JoltIn::LookupOutput,
-- );
let rd_nonzero_and_jmp = cs.allocate_prod(JoltIn::Bytecode_RD, JoltIn::OpFlags_IsJmp);
let lhs = JoltIn::Bytecode_ELFAddress + (PC_START_ADDRESS - PC_NOOP_SHIFT);
let rhs = JoltIn::RD_Write;
要解决这个挑战,我们需要向服务器提供访客程序的执行证明,输出为 5。 为了做到这一点,我们需要利用 Jolt 已被修改并且可能不再健全的事实。
该补丁删除了 R1CS 组件中的一个约束,让我们仔细看看被删除的约束。
cs.constrain_eq_conditional(
rd_nonzero_and_lookup_to_rd,
JoltIn::RD_Write,
JoltIn::LookupOutput,
);
如果第一个参数设置为 1
,则 constrain_eq_conditional
函数会将第二个和第三个参数之间的相等约束添加到 R1CS 约束系统中。
粗略地说,发出的约束等效于以下等式。
cs.constrain_eq_conditional(condition, left, right);
// condition * (left - right) == 0
上面几行还有一个有用的注释,解释了约束。
// if (rd != 0 && update_rd_with_lookup_output == 1) constrain(rd_val == LookupOutput)
cs.constrain_eq_conditional(
rd_nonzero_and_lookup_to_rd,
JoltIn::RD_Write,
JoltIn::LookupOutput,
);
RD_Write
值来自读写内存组件,它表示写入输出寄存器的内存值。
相反,LookupOutput
值来自指令查找组件,它表示查找参数“返回”的输出值,该参数执行指令执行检查。
约束的目标是在这两个值之间提供粘合。
一个直观的解释如下。
如果指令应该将其结果写入寄存器,并且如果输出寄存器不为零,则写入输出寄存器的值应等于执行查找参数的结果。
删除了此约束后,利用思路很简单:制作一个执行轨迹,其中对 2 和 2 求和的 add
指令,不是将值 4 写回输出寄存器,而是写入值 5。
在生成的轨迹中:
add
且操作数值均为 2,但是由于删除了强制这两个值相等的约束,因此该轨迹将被接受。
然后,程序将继续正常运行并返回计算出的值,因此最终修改后的执行轨迹的输出将恰好为 5
!
一旦我们了解了所有活动的部件,实际的利用就非常容易:我们只需要在 tracer
模块中修补 Jolt,该模块是生成执行轨迹的模块。
我们修改了 jolt/tracer/src/emulator/cpu.rs
文件,更改了 ADD
操作仿真的语义:如果操作数均为 2,则将值 5 写回输出寄存器。
Instruction {
mask: 0xfe00707f,
data: 0x00000033,
name: "ADD",
operation: |cpu, word, _address| {
let f = parse_format_r(word);
// If the operands are both 2, then write 5 in the output register
// otherwise apply normal addition semantics
if cpu.x[f.rs1] == 2 && cpu.x[f.rs2] == 2 {
cpu.x[f.rd] = cpu.sign_extend(5);
} else {
cpu.x[f.rd] = cpu.sign_extend(cpu.x[f.rs1].wrapping_add(cpu.x[f.rs2]));
}
Ok(())
},
disassemble: dump_format_r,
trace: Some(trace_r),
},
我们可以打印出来的一个有趣的事情是在执行 add {n}, {n}, {n}
指令的确切步骤中的执行轨迹。
这里要注意的主要部分是内存操作:该指令是 ADD
,两个操作数都等于 2
,因此有两个读取操作,但是然后有一个写入操作到具有值 5 的同一寄存器!
Trace[5]
JoltTraceStep {
instruction_lookup: Some(ADD(ADDInstruction(2, 2))),
bytecode_row: BytecodeRow {
address: 2147483672,
bitflags: 17448304640,
rd: 10,
rs1: 10,
rs2: 10,
imm: 0,
virtual_sequence_remaining: None
},
memory_ops: [Read(10), Read(10), Write(10, 5), Read(0), Read(0), Read(0), Read(0)]
}
我们还可以直接打印 R1CS 系统的输入,这些输入存储在 R1CSInputs
结构中。
正如我们所看到的,查找正确返回 4
,但是写入输出寄存器的值是 5
。
pc[7] = 9
bytecode_a[7] = 9
bytecode_v[7] = 9
memreg_a_rw[7] = 0
memreg_v_reads[7] = 2
memreg_v_writes[7] = 5
chunks_x[7] = 0
chunks_y[7] = 0
chunks_query[7] = 0
lookup_outputs[7] = 4
circuit_flags_bits[7] = 0
instruction_flags_bits[7] = 1
总而言之,主要的求解器 Rust 程序非常简单(使用修改后的 Jolt 库)。 运行此程序将输出一个证明,该证明提供给服务器将返回 flag!
use jolt_sdk::RV32IHyraxProof;
pub fn main() {
let (prove_two_plus_two, verify_two_plus_two) = guest::build_two_plus_two();
let (output, proof_gen) = prove_two_plus_two();
println!("Proof generated! {}", output);
let proof_bytes = proof_gen.serialize_to_bytes().unwrap();
println!("{}", hex::encode(&proof_bytes));
}
这是一种解决挑战的方法,但实际上删除该特定约束提供了一个更强大的原语:我们可以为每个将其结果写回寄存器的指令将任意值写入寄存器!
编写和解决挑战本质上是解决明确的 假设 实验。 这种方法是获得对底层技术和库(如本例中的 Jolt zkVM)的安全导向理解的绝佳途径。 此外,编写求解器程序或脚本的实践经验迫使我们以具体的方式展示 bug 的影响,这是在密码学审计中进行日常工作时的一项关键技能。
- 原文链接: blog.zksecurity.xyz/post...
- 登链社区 AI 助手,为大家转译优秀英文文章,如有翻译不通的地方,还请包涵~
如果觉得我的文章对您有用,请随意打赏。你的支持将鼓励我继续创作!