안녕하세요, 헥사랩스의 암호학 연구원 김민순입니다.
최근 저희는 OtterSec이 공개한 zkVM 관련 취약점을 분석하고, 제공된 CTF 스타일의 이전 버전을 익스플로잇하는 Challenge를 해결하였습니다.
zkVM은 프로그램 실행의 정당성을 증명해 주는 강력한 도구로 주목받고 있습니다. 하지만 증명 시스템이 복잡해질수록, 구현 세부의 작은 실수 하나가 전체 가정을 무너뜨릴 수 있습니다.
OtterSec의 Challenge는 Jolt와 Nexus, 두 zkVM 시스템을 대상으로 진행되었습니다. 공통적으로 핵심 문제는 Fiat-Shamir transcript에 반드시 흡수되어야 할 값이 누락되어 있었고, 그 결과 검증자가 확인하는 식을 공격자가 유리한 방향으로 맞춰 버릴 수 있었다는 점입니다.
이번 글에서는 두 사례를 통해, transcript 설계가 왜 증명 시스템의 보안 경계 그 자체인지 살펴봅니다.
Fiat-Shamir 변환이란
Fiat-Shamir 변환은 원래 검증자와 상호작용하며 난수를 주고받아야 하는 인터랙티브 증명을, 해시 기반 transcript를 이용해 비대화형 증명으로 바꾸는 기법입니다. 증명 과정에서 등장하는 커밋먼트, 중간 claim, 공개 입력 등 검증에 영향을 주는 값들을 transcript에 순서대로 누적하고, 이후의 challenge는 이 transcript로부터 결정됩니다.
만약 어떤 값이 검증식에 영향을 주면서도 transcript에 포함되지 않는다면, 공격자는 challenge가 고정된 뒤에도 그 값을 유리하게 조정할 수 있게 되고, 그 순간 Fiat-Shamir가 제공해야 할 soundness 보장이 무너질 수 있습니다.
두 문제에서는 검증에 중요한 값이 transcript에 묶여 있지 않았고, 그 값이 선형적으로 검증식에 반영되었으며 공격자는 필요한 방향으로 값을 조정해 위조 증명을 만들 수 있었습니다. 두 문제에 대해서 임의의 틀린 witness들에 대해 증명을 생성하는 과정을 진행하겠습니다.
Jolt (a16z)
Jolt는 RISC-V 프로그램을 위해 만들어진 zkVM입니다. Jolt의 증명 형태는 대략 다음과 같습니다.
JoltProof {
commitments: Vec<Commitment>,
opening_claims: Map<OpeningId, Claim>,
proofs: Map<Stage, SumcheckProof>,
...
}
OtterSec 블로그에서는 opening_claims가 transcript에 흡수되지 않는 변수이고, 공격자는 이를 위조하여 생성되는 랜덤 값을 유지하면서도 체크되는 등식들을 성립시킬 수 있다고 설명합니다.
Jolt의 익스플로잇은 크게 두 단계로 진행되었습니다. 먼저 내부 검증 과정에는 총 다섯 개의 sumcheck 등식과 하나의 Dory check가 존재했는데, Dory 쪽은 transcript 상태만 적절히 맞춰 주면 비교적 쉽게 우회할 수 있었습니다. 이론적으로는 prover 측에서 실패를 무시하도록 수정하는 방식도 가능했지만, 저는 prover 로직을 크게 건드리기보다는 transcript 자체를 verifier가 기대하는 상태에 맞추는 쪽을 선택했습니다.
먼저 sumcheck 검증식이 opening_claims의 변화에 따라 어떻게 반응하는지를 관찰했습니다. 검증 코드에서 원래는 output_claim과 expected_output_claim이 다를 경우 즉시 에러를 반환하도록 되어 있었는데, 해당 부분을 잠시 출력 중심으로 바꾸어 두 값이 각각 어떤 식으로 움직이는지를 확인했습니다.
println!("a = {:?}", output_claim);
println!("b = {:?}", expected_output_claim);
if output_claim != expected_output_claim {
// return Err(ProofVerifyError::SumcheckVerificationError);
}
이렇게 하면 특정 opening_claims를 조정했을 때 어느 쪽 값이 고정되어 있는지, 또는 어떤 방향으로 선형적으로 변하는지를 직접 추적할 수 있습니다.
한 개의 예시를 확인해보겠습니다. 위의 output_claim, expected_output_claim 관련 체크 바로 직전 코드를 확인해보겠습니다.
let expected_output_claim = sumcheck_instances
.iter()
.zip(batching_coeffs.iter())
.map(|(sumcheck, coeff)| {
// If a sumcheck instance has fewer than `max_num_rounds`,
// we wait until there are <= `sumcheck.num_rounds()` left
// before binding its variables.
// So, the sumcheck *actually* uses just the last `sumcheck.num_rounds()`
// values of `r_sumcheck`.
let r_slice = &r_sumcheck[max_num_rounds - sumcheck.num_rounds()..];
if let Some(opening_accumulator) = &opening_accumulator {
// Cache polynomial opening claims, to be proven using either an
// opening proof or sumcheck (in the case of virtual polynomials).
sumcheck.cache_openings_verifier(
opening_accumulator.clone(),
sumcheck.normalize_opening_point(r_slice),
);
}
let claim = sumcheck.expected_output_claim(opening_accumulator.clone(), r_slice);
claim * coeff
})
.sum();
expected_output_claim을 계산하는 과정인데, claim * coeff을 선형적으로 더하여 계산되는 걸 알 수 있습니다. 이 claim들은 verify 과정에서 opening_claims로부터 추출되는 값들이고, 따라서 opening_claims의 한 값의 변화에 따라 선형적으로 expected_output_claim의 값을 조정할 수 있습니다. 이를 output_claim 값과 일치하게 만듬으로서 체크를 우회할 수 있습니다.
opening_claims는 여러 값으로 구성되어 있기 때문에, 충분한 횟수의 관찰을 통해 각 값들이 opening_claims에 대해 가지는 영향을 모은 뒤, 이를 유한체 위 선형방정식으로 정리하여 다섯 개의 sumcheck 조건을 동시에 만족하는 값을 계산했습니다. 이 과정에서는 필요한 곡선 필드 위에서 연립방정식을 풀기 위해 SageMath를 사용했습니다.
Jolt가 사용하는 타원곡선 필드인 bn128 커브의 order인
21888242871839275222246405745257275088548364400416034343698204186575808495617이 modulus인 필드 위에서 해를 찾으면 해결할 수 있습니다.
예를 들어 선형적으로 작용되는 opening_claims 변수 $o_1, o_2$에 대하여 다음과 같은 결과가 관측되었다고 가정합니다.
opening_claims$o_1, o_2$ → 다음과 같은 체크 실패 $a_1 = b_1, a_2 = b_2$opening_claims$o_1 + 1, o_2$ → 다음과 같은 체크 실패 $a_1 = c_1, a_2 = c_2$opening_claims$o_1, o_2 + 1$ → 다음과 같은 체크 실패 $a_1 = d_1, a_2 = d_2$
$o_1$의 1 증가로 인해 첫 체크의 우변은 $c_1 - b_1$만큼 증가하고, 두 번째 체크의 우변은 $c_2 - b_2$만큼 증가합니다. 마찬가지로 $o_2$의 1 증가로 인해 첫 체크의 우변은 $d_1 - b_1$만큼 증가하고, 두 번째 체크의 우변은 $d_2 - b_2$만큼 증가합니다.
이때 2개의 체크를 모두 만족시키기 위해서는 다음과 같은 선형식을 통해 해를 구할 수 있습니다.
$$\begin{bmatrix}c_1 - b_1 & d_1 - b_1 \\c_2 - b_2 & d_2 - b_2\end{bmatrix} \cdot\begin{bmatrix}o\_increment_1 \\o\_increment_2\end{bmatrix} = \begin{bmatrix}a_1 - b_1 \\a_2 - b_2\end{bmatrix}$$
여기서 구한 $o_increment_i$ 값들을 기존 $o_i$에 더함으로서 해를 구할 수 있습니다. 실제로는 5개의 체크가 있는 것을 감안하여 진행하면 됩니다. 그러나 모든 opening_claims의 값들이 식에 선형적이지 않음에 유의합니다.
Transcript를 맞추는 작업 자체는 생각보다 간단합니다. prover 측의 reduce_and_prove와 verifier 측의 reduce_and_verify는 같은 흐름을 따라 challenge를 생성하지만, 중간에 흡수되는 바이트열이 어긋나면 서로 다른 transcript 상태에 도달하게 됩니다. 따라서 verifier 쪽에서 특정 지점의 transcript 상태를 확인한 뒤, 그 상태가 prover 쪽에서도 재현되도록 해당 위치에 동일한 효과를 내는 바이트를 삽입하면 됩니다. 실제로는 verifier 쪽의 한 지점에서 만들어지는 transcript 상태를 확인해 prover 쪽의 대응 위치로 옮겨 주는 것만으로 Dory check를 일치시키는 데 충분했습니다.
pub fn reduce_and_prove<ProofTranscript: Transcript, PCS: CommitmentScheme<Field = F>>(
&mut self,
mut polynomials: HashMap<CommittedPolynomial, MultilinearPolynomial<F>>,
mut opening_hints: HashMap<CommittedPolynomial, PCS::OpeningProofHint>,
pcs_setup: &PCS::ProverSetup,
transcript: &mut ProofTranscript,
) -> ReducedOpeningProof<F, PCS, ProofTranscript> {
tracing::debug!(
"{} sumcheck instances in batched opening proof reduction",
self.sumchecks.len()
);
// 2. 이 부분에 덤프한 transcript로 다시 고정
...
pub fn reduce_and_verify<ProofTranscript: Transcript, PCS: CommitmentScheme<Field = F>>(
&mut self,
pcs_setup: &PCS::VerifierSetup,
commitment_map: &mut HashMap<CommittedPolynomial, PCS::Commitment>,
reduced_opening_proof: &ReducedOpeningProof<F, PCS, ProofTranscript>,
transcript: &mut ProofTranscript,
) -> Result<(), ProofVerifyError> {
#[cfg(test)]
if let Some(prover_openings) = &self.prover_opening_accumulator {
assert_eq!(prover_openings.len(), self.len());
}
// 1. 이 부분의 transcript 상태 덤프
이 문제에서 사용되는 Blake2bTranscript의 상태 구현은 다음과 같습니다.
pub struct Blake2bTranscript {
/// 256-bit running state
pub state: [u8; 32],
/// We append an ordinal to each invocation of the hash
n_rounds: u32,
#[cfg(test)]
/// A complete history of the transcript's `state`; used for testing.
state_history: Vec<[u8; 32]>,
#[cfg(test)]
/// For a proof to be valid, the verifier's `state_history` should always match
/// the prover's. In testing, the Jolt verifier may be provided the prover's
/// `state_history` so that we can detect any deviations and the backtrace can
/// tell us where it happened.
expected_state_history: Option<Vec<[u8; 32]>>,
}
32개의 8비트 정수로 이루어진 state와 n_rounds 값으로 Transcript의 상태가 결정되기 때문에 그 값들을 덤프하고 저장함으로서 조작 가능합니다.
정리하면, Jolt에서는 transcript에 바인딩되지 않은 opening_claims를 조정할 수 있었고, 각 sumcheck 검증식이 그 값들에 대해 선형적으로 반응한다는 점을 이용해 최종적으로 모든 검사를 만족하는 위조 proof를 구성할 수 있었습니다. Dory check는 transcript 상태를 수동으로 맞추는 방식으로 해결했고, 나머지 핵심 검증식들은 선형대수적으로 맞춰 나가는 방식으로 통과시켰습니다.
Nexus (StarkWare)
Nexus의 경우에는 Jolt보다 구조가 훨씬 단순했습니다. 여러 개의 검증식을 동시에 맞춰야 했던 Jolt와 달리, 여기서는 사실상 하나의 핵심 체크만 원하는 방향으로 맞추면 되는 형태였습니다. OtterSec의 설명에 따르면 claimed_sum은 전체 합이 0이어야 한다는 제약만 만족하면 되는데, 이 값 역시 transcript에는 흡수되지 않습니다. 따라서 공격자 입장에서는 한 항에 $k$를 더하고 다른 항에 $k$를 빼서 전체 합은 그대로 유지하면서, 검증식에 어떤 방향으로 영향을 주는지 관찰하는 방식이 자연스럽게 떠오릅니다.
올바른 witness가 존재하지 않는 상황에서의 증명을 생성하는 것이 목표이기에, 먼저 잘못된 witness에 대해서도 proof 생성을 끝까지 진행할 수 있도록 실행 결과를 맞춰 주는 작업이 필요했습니다. 이를 위해 vm/src/trace.rs의 k_trace 함수에 public output을 직접 채워 넣는 코드를 추가해, verifier가 기대하는 출력 형식과 동일한 값을 갖도록 만들었습니다.
// Must match verify_expected encoding exactly.
let mut out = postcard::to_stdvec_cobs(&Some(true)).expect("encode Some(true)");
let padded_len = (out.len() + 3) & !3;
out.resize(padded_len, 0x00);
if let Some(layout) = view.memory_layout {
view.output_memory = out
.iter()
.enumerate()
.map(|(i, b)| emulator::PublicOutputEntry {
address: layout.public_output_start() + i as u32,
value: *b,
})
.collect();
}
이렇게 하면 invalid witness를 사용하더라도 proving 단계가 완전히 중단되지는 않고, 최종적으로는 stwo의 ConstraintsNotSatisfied 오류만 남는 상태까지 끌고 갈 수 있습니다. 해당 에러가 raise되는 부분을 무시하면 틀린 witness들로부터도 우선 증명 생성이 완료됩니다.
{
// return Err(ProvingError::ConstraintsNotSatisfied);
}
생성된 증명 자체로 Verify를 시도하면 유일한 등식 체크인 다음 부분이 실패합니다. Proving 과정 중에는 여러 개의 등식이 실패하지만, Verify 과정에서는 여러 등식이 선형적으로 결합되어 최종적으로 하나의 검증만을 진행합니다. Jolt와 같이 a와 b가 같아야만 Verify가 완료되는 구조입니다.
let a = composition_oods_eval;
let b = components.eval_composition_polynomial_at_point(
oods_point,
&proof.sampled_values,
random_coeff,
);
println!("{}", a);
println!("{}", b);
Jolt에서는 여러 식을 동시에 맞춰야 했기 때문에 선형방정식을 모아 푸는 과정이 필요했지만, Nexus에서는 실질적으로 단일 체크만 다루면 되었기 때문에 그 정도까지 복잡한 계산은 필요하지 않았습니다. 이미 claimed_sum의 합이 0인 제약 조건은 만족되었기에, 한 값에 $k$를 더하고 한 값에 $k$를 빼는 과정으로 유일한 등식을 만족시키게 설정하면 해결 가능합니다.
다만 구현 과정에서 한 가지 까다로운 점은, Nexus가 일반적인 소수체가 아니라 다소 특이한 QM31 필드를 사용하고 있었다는 점입니다. 따라서 보정값을 계산하는 과정 역시 해당 필드 위에서 정확히 처리해야 했고, 이를 위해 별도로 SageMath 스크립트를 사용해 산술을 맞췄습니다. 즉, 공격의 본질은 매우 단순한 선형 조정이었지만, 실제 exploit에서는 그 연산이 이루어지는 필드의 구조를 정확히 따라가야만 최종적으로 검증을 통과시킬 수 있었습니다. 다음은 QM31 필드의 SageMath 구현입니다.
p = 2^31 - 1
Fp = GF(p)
# i^2 = -1
R.<X> = PolynomialRing(Fp)
CM31.<i> = Fp.extension(X^2 + 1)
# u^2 = 2 + i
S.<Y> = PolynomialRing(CM31)
QM31.<u> = CM31.extension(Y^2 - (CM31(2) + i))
사칙연산이 잘 정의되는 체이기에, 똑같이 선형적으로 푸는 데에 문제가 없으나, 결과로 나온 값의 형태가 $2^{31} - 1$ 미만의 값 4개로 형성되어 있음에 주의합니다.
(2042649430*i + 1471302658)*u + 384541130*i + 1645951658
정리하면, Nexus에서는 transcript에 바인딩되지 않은 claimed_sum을 조절할 수 있었고, 그 값이 단일 검증식에 선형적으로 영향을 준다는 점을 이용해 invalid witness에 대한 proof를 통과시키는 것이 가능했습니다. 구조는 Jolt보다 단순했지만, 오히려 그만큼 transcript 누락이 얼마나 직접적으로 soundness 문제로 이어지는지를 더 선명하게 보여주는 사례였습니다.