[KalmarCTF 2024] Breakfaest

Points: 500 (0 solves, first blood after the CTF)

I heard that you could use VOLE-in-the-head to make post-quantum signatures. Here’s a signature scheme based on the Poseidon hash function. Can you create a forgery? Hint to narrow the bug search: volonym’s zero knowledge proofs are vulnerable, and can be forged for arbitrary statements.

It’s not just a party, it’s a FAEST

With so many strong cryptographers in Kalmarunionen, and particularly such a large amount of them doing irl cryptography at Aarhus, it didn’t come as a big surprise to me to see a challenge inspired by the FAEST post-quantum signature proposal pop up on the CTF. Having collaborated with just shy of half the chefs behind that recipe, on related topics even (mostly MPC-in-the-Head things, so not exactly all the way to vOLE), I quickly claimed this challenge in our team chat. Once I started actually looking at the challenge, a moment of regret occured when I saw how tricky it got to properly read the source code of the used library and how badly documented it turned out to be. Nevertheless, it was a matter of personal pride, so I got to work.

Several hours later, I’d managed to find at least some bugs, including one which made my MPCitH brain say things like

Oh, equality constraints might just be public openings to zero, so if we can truncate them, that could be an easy flaw to exploit.

but nothing actually exploitable in context of the challenge actually came out of that. (If you want to see that specific bug, look at zkp/mod.rs and pay close attention to the condition used in Verifier::verify_public.)

As a result, I moved on to some other challenges, and failed to exploit a UAF in a python extension module for several hours instead. Then, about half an hour to an hour before the end of the CTF, a teammate suddenly alerted me to something that promised to be far more useful if it was indeed a bug. And it was! Alas, that is not enough time to wrangle rust and a library that resents being wrangled, so my personal pride had to wait for several more hours – well after the CTF was over and the extra points didn’t matter for the team anymore; at least I got some extra bounty swag out of it too – to be vindicated. We’ll get to the details of the bug I abused in a bit, but first, let’s get some high-level context of zero-knowledge protocols and the ever-misuse-inviting Fiat-Shamir transform.

Cryptographical social anxiety

ZK proofs originated as interactive protocols, initially proving very specific relations between some private “witness” and a public “statement” about that witness. One of the best known such protocols is Schnorr’s identification scheme, which can be seen as a general instantiation of a proof of knowledge for a preimage of a group homomorphism, as described by Maurer.

In general, a sigma protocol (which is what we call those things), proceeds in 3 rounds of communication:

• The prover commits to some random value
• The verifier sends random challenge that the prover should (with high probability) only be able to answer if they actually know the witness
• The prover sends a value that the verifier can check against a combination of the public statement and the commitment of the first round.

Many further improvements to these schemes have since been devised, including things like more rounds of communication and the ability to prove arbitrary statements in NP (so mostly anything reasonable you’d want to prove), but the general structure of having a commitment and a challenge is still there.

Many cryptographers turn out to be introverts, and not all that much into partying and social interaction however, so we started coming up with ways to not have to talk to a verifier, while still remaining capable of proving stuff. Proofs are a mathematician’s and a cryptographer’s bread and butter, of course, so what else would we be spending our time on… For ZK schemes that have properties like “honest verifier zero-knowledge” and “public coin”, a way was found in which to replace the verifier with merely a hash function, and they don’t expect you to make much conversation at a party, yay! (Technically, this is all modeled as random oracles, so a hash function is actually not exactly what we want, but we’ll just ignore that little detail.)

The trick behind it is that the prover should not be able to predict the random challenge before making the initial commitment, since otherwise they can cheat. So if we simply take a hash of the initial commitment as input to a hash function that outputs the challenge, this dependency can be made explicit. This is known as the Fiat-Shamir transformation or heuristic. Of course, in real-world implementations, all kinds of things can go wrong, and if you forget to include some important parts of the prerequisites into the hash function, a lot more room for cheating becomes available. Common things that get forgotten as inputs to the hash functions include but are not limited to some sort of session identifier to avoid proof replays, the public statement, and of course the initial commitments. As such, whenever you see a ZK CTF challenge, always look for what is (or rather what isn’t) included in the Fiat-Shamir implementation.

To quickly touch on some other big ideas on modern ZK schemes, first consider trying to compactly prove that a bunch of things are simultaneously zero, i.e. $$\forall i: a_i = 0.$$ A first idea might be to just sum everything together, and that should still be zero, but of course, that structure is entirely predictable and far too easy to cheat. Instead, we’ll take a random linear combination, where the random coefficients are obtained as a challenge from the verifier. Now we get $$\sum_i c_i \cdot a_i = 0,$$ which satisfies both our ask for compactness and being hard to cheat on. As long as we still cannot predict the $c_i$, that is. In a similar fashion, these protocols often squash multiple things together in a single polynomial, and then prove things about the evaluation of the polynomial at a random (so a verifier challenge) evaluation point, by using the Schwartz-Zippel lemma.

🦀🦀🦀

Let’s now take a short detour and organize a crab rave setup our rust environment. Of course, the first step in settin up any kind of development environment is picking your favorite editor, and starting a flame war with the emacs users. My editor of choice these days is helix, though my vim is not too far away either should I feel the need. /dev/null will happily receive all your complaints and remarks about this choice.

All joking aside though, the most important thing that you’ll really want in your editor is LSP integration, and in particular integration with the rust LSP known as rust-analyzer. It has the indispensable functionalities of showing you exactly what types can be inferred on specific values, jumping to definitions of types, functions, traits, showing cross references to functions and variables, and more. It can even show you where implementations of a trait are to be found!

The other thing you’ll want is a local version of the volonym library to mess around with, directly integrated with the rest of the source code you’ll be writing and modifying. The “go to definition” parts of rust-analyzer can already take you to the implementation of things in the library, but you’ll soon notice that editing these would usually not have the desired effect. Instead, we’ll make a local clone, directly from the branch and repository that’s listed in Cargo.toml, and then point cargo towards that new directory for the dependency instead. Where at first you could read

volonym = { git = "https://github.com/holonym-foundation/vole-zk-prover.git", branch = "main" }

now you’ll want to write

volonym = { path = "./vole-zk-prover" }

instead.

Try it out, add some println! or panic! at a code path of your choice in volonym, cargo run it and rejoice, for you’re one step closer to solving this challenge and partying with the other carcinized creatures in your neighborhood.

ZK CTF challenges, the general approach

From personal experience, if you want to break a ZK scheme in a CTF challenge, 90% of the time, if not more, you’ll follow these steps:

• Completely ignore any theoretical description of the protocol
• Determine the missing part of the FS transformation
• Work through the verifier to see what you can do with the input that was not used as input to the FS hash

In particular the first step here is important to remember. It’s tempting to try and understand what’s going on in the protocol, but so much that’s happening based on the “known” challenge is so simple – remember, linear combinations and polynomials – that it would take far longer to determine how the source code of some convoluted implementation corresponds to what is described in a beautifully typeset and completely theoretical mathematical paper, than just applying one age-old technique: “Fuck around and find out.”

Let’s eat!

Now for the real exploitation part of the challenge. Let’s start by having a look at the bug.

let sgc_diag_delta = self.code.batch_encode(&proof.s_matrix.0).iter().map( |row| row * &deltas ).collect::<Vec<FVec::<T>>>();
let lhs = &challenges.s_challenge * &(&q1.scalar_mul(challenges.vith_delta) + &q2).transpose();
let rhs = &proof.s_consistency_check + &(&challenges.s_challenge * &FMatrix(sgc_diag_delta).transpose());
if lhs != rhs { return Err(anyhow!("failed to verify S matrix")) }

By using our rust-analyzer powers of finding cross-references, we can determine that neither proof.s_consistency_check, nor proof.s_matrix is bound to the Fiat-Shamir challenges. Looking further, we also observe that proof.s_matrix is also of crucial importance in the verification step of the quicksilver proof. Even better, the consistency check value is used nowhere else, so we can modify it to fit whatever value for the matrix will make our proof go through, and not worry about it until then. To get an entire proof, we shall first simply generate a proof in the old way, with maybe a few minor adjustements along the way, which would of course not pass any sort of verification yet with the wrong private key, and then change these values in the proof so that it (incorrectly) gets accepted by the verifier. The usage of s starts off in quicksilver::Verifier::from_vith where it is used to compute the vector q (see zkp/mod.rs), by flattening the matrix and adding on some values from the commitment to the witness.

let mut s_adjustment = witness_comm.scalar_mul(delta);
s_adjustment.0.push(FVec::<T>(vec![T::ZERO; row_len]));
let mut s_adjusted = s_rows + &s_adjustment;
s_adjusted.0.iter_mut().for_each(|row| q.append(&mut row.0));

Again, we shall ignore the adjustment for a moment, and first try to determine a good q vector, from which it becomes then possible to subtract the (scaled) witness commitment, and obtain the matrix s, for which we can then calculate a good consistency value.

q, subsequently is used to validate the R1CS correctness, which we can write with the matrix equation $A q \odot B q - \Delta C q$, where $A$, $B$ and $C$ are matrices that represent the constraints from our verification circuit/public statement, and $\odot$ is pointwise multiplication of vectors.

let new_q = &(&q_a * &q_b) - &q_c.scalar_mul(self.delta);
let success = proof.mul_proof.1 + proof.mul_proof.0 * self.delta == new_q.dot(&challenge_vec);

Because checking that every element of the resulting vector invidually has a certain value is expensive in communication, it gets compressed with a random linear combination instead, taking the inner product $\left\langle A q \odot B q - \Delta C q, c\right\rangle$ for some vector of challenges $c$. Of course, since we’ll only be modifying q here, and that is not included in the FS hash, those challenges remain constant and predictable, allowing us all the freedom we’d want to pass the challenge. for convenience, we’ll let proof.mul_proof be (0, 0), so that we’re exactly targeting a value of zero at the end, and take this into consideration for the derivation of the FS challenges.

The most tempting solution would of course be to make let $q = 0$ and simply not have any worries about the challenges at all, but the next check will prevent that, unfortunately. When we now look at Verifier::verify_public, we’ll see some checks in the first coefficients of q, that have to match up with the public values in the statement: 1, our public key and the hash of the message being signed.

if !(*u * &self.delta + v == self.q.0[*i]) { bail!("Invaliding opening of a public input") }

As you can observe, if you close your eyes just far enough, this is a quadratic equation in $\delta$, which we can solve over the field of definition $\mathbb{F}_r$. When this equation happens to have no solution, we can simply restart, take a new “original” proof with new randomness and hence new challenges and values all around, and hopefully a solvable quadratic this time. Alternatively, it would also be possible to try a different coefficient for our value $\delta$.

crab fight implementing the solution

If at any point, you come across a function being called that is private, simply modify its source to have a pub fn instead. I did that a few times, and I don’t remember where it was needed exactly, so I won’t mention it in those places.

Step 1: Patch the prover to always output (0, 0) for proof.mul_proof (zkp/mod.rs, Prover::prove)

ZKP {
    mul_proof: (T::ZERO, T::ZERO),
}

Step 2: Generate the base proof

// Gotta have _some_ value there for the code to work,
// the actual value doesn't even matter, as we're cheating anyway
self.sk = Some(self.pk)

// ...

// I modified this to also return the challenges,
// so I don't have to compute them again.
let (mut proof, challenges) = prover.commit_and_prove().unwrap();

Step 3: Generate the initial q vector such that the verify_public step will pass

let mut s = FMatrix::<Fr>(
    proof
        .commitment
        .witness_comm
        .0
        .iter()
        .map(|r| FVec::<Fr>(r.0.clone()))
        .collect(),
);

s.0.push(FVec::<Fr>(vec![Fr::ZERO; s.0[0].0.len()]));

// Ensure the public openings are correct
let pin = &proof.proof.public_openings.public_inputs;
s.0[0].0[0] = pin[0].1 + challenges.vith_delta * pin[0].0;
s.0[0].0[1] = pin[1].1 + challenges.vith_delta * pin[1].0;
s.0[0].0[2] = pin[2].1 + challenges.vith_delta * pin[2].0;

let mut q = Vec::new();
s.0.iter_mut().for_each(|row| q.append(&mut row.0.clone()));
// q A . q B - Δ q C = 0
let challenge = calc_quicksilver_challenge(&proof.commitment.seed_comm,
                                        &proof.commitment.witness_comm);
let qs_challenges = get_challenge_vec(&challenge, q.len());

Step 4: Determine and solve the quadratic equation

// Used to get X_l for matrices X
let mut ell_hot = FVec::<Fr>(vec![Fr::ZERO; q.len()]);
ell_hot.0[ell] = Fr::ONE;
let (al, bl, cl) = prover.circuit.r1cs.vec_mul(&ell_hot);
// Aq, Bq, Cq
let (qa, qb, qc) = prover.circuit.r1cs.vec_mul(&FVec::<Fr>(q.clone()));
let const_coef = (&(&qa * &qb) - &qc.scalar_mul(challenges.vith_delta)).dot(&qs_challenges);
// Holy borrows, batman!
let lin_coef = (&(&(&qa * &bl) + &(&al * &qb)) - &cl.scalar_mul(challenges.vith_delta))
    .dot(&qs_challenges);
let sq_coef = (&al * &bl).dot(&qs_challenges);

// Solve it, thanks for providing the .sqrt(), ig
let det = (lin_coef * lin_coef - Fr::from(4) * const_coef * sq_coef)
    .sqrt()
    .unwrap();
let q_ell = q[ell] + (-lin_coef + det) * (sq_coef + sq_coef).invert().unwrap();

s.0[0].0[ell] = q_ell;

Step 5: Correct for the adjustment to s, and build the final proof

for (i, x) in proof.commitment.witness_comm.0[0].0.iter().enumerate() {
    s.0[0].0[i] -= challenges.vith_delta * x;
}
proof.proof.s_matrix = s;

// And the consistency check
let verif = Verifier::from_circuit(prover.circuit.clone());

// This is just a slightly modified copy of Verifyer::verify
proof.proof.s_consistency_check = verif.get_consistency_vals(&proof).unwrap();

Step 6: Serialize the proof so you can send it to the server

fn main() {
    let key = Key::generate(&mut StdRng::from_entropy());

    let pubkey = BASE64_STANDARD
        .decode(std::env::args().nth(1).unwrap().as_bytes())
        .unwrap();
    let pk = Key::deserialize(&pubkey[..]).unwrap();

    println!(
        "sig: {}",
        BASE64_STANDARD.encode(&serde_bare::to_vec(&pk.sign(b"Give me the flag!")).unwrap())
    );
}

Step 7: Script it in python because you really don’t want to paste such a large base64 blob into your terminal and risk messing it up

from pwn import *
io = remote("chal-kalmarc.tf", 3)
io.recvuntil(b"key: ")
key = io.recvline().strip()
print("key: ", key)
out = process(["cargo", "r", "--", key.decode()]).recvall().decode().split("sig: ")[1].split("\n")[0]
io.sendlineafter(b":", b"Give me the flag!")
context.log_level = "info"
io.sendlineafter(b":", out.encode())
io.interactive()

Finally, remark that we’re particularly lucky with this library as it doesn’t check if the statement we’re proving is actually correct, so we don’t even need to convince it to let us generate false proofs.

🚩

Kalmar{SeEMS_l1KE-fI47-5hamir_Is-VI3Wed_AS_jUs7-a_SuGgE$TIOn}