# [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") }
```

`q`

and modify one extra coefficient to bring everything
back to 0 in the inner product. To do so, let’s write the “base” value
of
$q$,
the one with only the first 3 coefficients non-zero, and our new,
corrected value
$q' = q + \delta$.
Since we intend to modify
$\delta$
only at one coefficient, say the
$\ell$th,
We also overload the notation
$\delta$
to mean the value that this coefficient of
$\delta$
will be. When we write out the equation we need to satisfy, we then
arrive at
$\begin{aligned}
&\left\langle A (q + \delta) \odot B (q + \delta) - \Delta C (q + \delta), c \right\rangle\\
= &\left\langle A q \odot B q - \Delta C q, c\right\rangle
+ \delta \left\langle A q \odot B_\ell + A_\ell \odot B q - \Delta C_\ell, c \right\rangle
+ \delta^2 \left\langle A_\ell \odot B_\ell, c \right\rangle.
\end{aligned}$
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}`