@@ 0,0 1,432 @@
+---
+date: 2024-03-18T20:00:00+01:00
+title: "[KalmarCTF 2024] Breakfaest"
+tags: ["vole-in-the-head", "crypto", "zero-knowledge", "fiat-shamir"]
+author: Robin Jadoul
+summary: "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?"
+---
+
+**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](https://faest.info/) 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](https://crypto.ethz.ch/publications/files/Maurer15.pdf).
+
+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](https://link.springer.com/content/pdf/10.1007/3-540-47721-7_12.pdf)
+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](https://en.wikipedia.org/wiki/Schwartz%E2%80%93Zippel_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](https://helix-editor.com/),
+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
+```toml
+volonym = { git = "https://github.com/holonym-foundation/vole-zk-prover.git", branch = "main" }
+```
+now you'll want to write
+```toml
+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.
+
+```rust
+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.
+
+```rust
+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.
+
+```rust
+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.
+
+```rust
+if !(*u * &self.delta + v == self.q.0[*i]) { bail!("Invaliding opening of a public input") }
+```
+
+So instead, we'll take the right values for those first 3 coefficients
+of `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(\left\langle A q \odot B_\ell + A_\ell \odot B q - \Delta C_\ell, c \right\rangle \right)
+ + \delta^2 \left(\left\langle A_\ell \odot B_\ell, c \right\rangle\right).
+\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`)
+
+```rust
+ZKP {
+ mul_proof: (T::ZERO, T::ZERO),
+}
+```
+
+Step 2: Generate the base proof
+
+```rust
+// 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
+
+```rust
+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
+
+```rust
+// 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
+
+```rust
+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
+
+```rust
+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
+
+```python
+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}`