Challenge Description

I know the flag and I can prove it… dumb.zip

Overview

We’re given a few different files: a folder called parts, and two Python scripts called check.py and proof.py. To make sense of the files in the parts folder, we’ll first want to look at the check script.

import json
import subprocess

flag = input('Flag: ').encode('ascii')
assert len(flag) == 32

inp = {
    "flag": list(bytes(flag))
}

open('tmp_input.json', 'w').write(json.dumps(inp))

rcode = subprocess.run('snarkjs wc ./parts/main.wasm tmp_input.json tmp_witness.wtns', shell=True)
if rcode.returncode == 1:
    print('Failed!')
    exit(-1)

print('Generating proof...')
subprocess.run('snarkjs plonk prove parts/circuit_final.zkey tmp_witness.wtns tmp_proof.json tmp_public.json', shell=True)

print('Do you know the flag?')
pub = json.load(open('tmp_public.json', 'r'))
print('Public: ', pub)
if pub == ["1"]:
    print('good :)')
else:
    print('bad :(')
subprocess.run('snarkjs plonk verify parts/verification_key.json tmp_public.json tmp_proof.json', shell=True)

This tells us that the files in the parts folder are intended to be used by SnarkJS, and that they are intended to be used in a protocol called PLONK.

The PLONK protocol

After doing some research, I found out that PLONK is an implementation of a zero-knowledge proof: a method of proving that a computation was made without having to specify the inputs of the computation. I found this explanation of the PLONK protocol somewhat helpful, although we don’t need all of this to solve the challenge.

The important thing to understand is that PLONK uses a formalized representation of a circuit based on a list of constraints on the inputs and outputs. Given this representation, certain properties of the circuit can be used to prove information about the circuit without revealing what the circuit is.

SnarkJS provides an implentation of this protocol. Given a circuit generated by the circom language, SnarkJS can generate constraints and proofs for it. Knowing this, we can now make sense of the files in the parts folder:

  • main.r1cs, main.sym, and main.wasm contain the constraints for our circuit.
  • proof.json, verification_key.json, and circuit_final.zkey contain information that proves that our circuit has been computed for a private input.
  • public.json contains the output of the circuit after the computation has completed. In this case, the expected output is 1.

This gives us a rough idea of what we need to do to solve the challenge. The circuit containes in the main files is a flag checker that produces the output 1 when the correct flag is entered. The proof.py script runs the flag checker uses the PLONK protocol to generate a proof that the circuit was run with the correct input.

At this point, I suspected that I didn’t actually need to understand how the proof worked. The flag checker circuit is entirely contained in the main files, and we know that the expected output of the circuit is 1. This made me think that it would probably be possible to reverse the circuit without looking at the proof at all.

Replicating the circom circuit

I first printed out the constraints of the circuit using the command snarkjs r1cs print main.r1cs main.sym. I also exported the circuit to JSON using the command snarkjs r1cs export json main.r1cs main.r1cs.json.

The print command gives us a long list of constraints that look like this:

␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.flag[0] ] * [ main.flag[1] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[0] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.flag[1] ] * [ main.flag[2] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[1] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.flag[2] ] * [ main.flag[3] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[2] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.flag[3] ] * [ main.flag[4] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[3] ] = 0

␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[0] ] * [ main.k1[1] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[0] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[1] ] * [ main.k1[2] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[1] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[2] ] * [ main.k1[3] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[2] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k1[3] ] * [ main.k1[4] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[3] ] = 0

␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[0] ] * [ main.k2[1] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k3[0] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[1] ] * [ main.k2[2] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k3[1] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[2] ] * [ main.k2[3] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k3[2] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k2[3] ] * [ main.k2[4] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k3[3] ] = 0

␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698184423875738898432 +main.k3[1] ] * [ 20182628090806273 +21888242871839275222246405745257275088548364400416034343698204186575808495616main.k3[0] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k4[1] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698180566017234982176 +main.k3[2] ] * [ main.k4[1] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k4[2] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698192178981647999616 +main.k3[3] ] * [ main.k4[2] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k4[3] ] = 0
␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698202086355429359616 +main.k3[4] ] * [ main.k4[3] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k4[4] ] = 0

␛[32;22m[INFO]  ␛[39;1msnarkJS␛[0m: [ 21888242871839275222246405745257275088548364400416034343698182648991527919616 +main.k3[31] ] * [ main.k4[30] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.correct ] = 0

It’s not immediately clear what’s going on here, we can see a few things right away. The flag is 32 characters long, and the circuit is computing several intermediate values in arrays of length 32 called k1, k2, k3, and k4. In addition, the final values in k3 and k4 are being used to calculate another value called correct, presumably the final return value of the circuit.

I decided that the best way to understand the circuit would be to write a few example circuits in circom myself. I figured out pretty quickly that the values in k1 were generated using a circuit like this:

    for (var i=1; i<32; i++) {
    k1[i-1] <== (flag[i-1])*flag[i];
    }
    
    k1[31] <== flag[0]*flag[31];

In other words, each value k1[i] is the product of flag[i] and flag[i-1]. Similarly, k2[i] = k1[i]*k1[i-1], and k3[i] = k2[i]*k2[i-1].

I noticed that the circom compiler was multiplying some of the values in my circuit by 21888242871839275222246405745257275088548364400416034343698204186575808495616, the same value that appeared in the given circuit, even though I hadn’t specified this value anywhere in my test circuit. However, I eventually noticed the line "prime": "21888242871839275222246405745257275088548364400416034343698204186575808495617" in the main.r1cs.json file. It turns out that all of the calculations for the circuit are being computed modulo the value of prime, so multiplying by 21888242871839275222246405745257275088548364400416034343698204186575808495616 is equivalent to multiplying by -1.

The calculation of the values in k4 is more complicated than the calculation of the values in k1 through k3. Each value of k4 is given by the formula k4[i] = (some constant - k3[i]) * k4[i-1], with a seemingly random constant being used each time. As it turns out, these constants aren’t random at all, but we’ll get to that later.

To obtain the values of the constants, we need to subtract the values in the main.r1cs file from prime. For example, k4[2] is generated like this in the main.r1cs file:

[32;22m[INFO]  [39;1msnarkJS[0m: [ 21888242871839275222246405745257275088548364400416034343698180566017234982176 +main.k3[2] ] * [ main.k4[1] ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.k4[2] ] = 0

And this is the corresponding line in circom:

k4[2] <== (23620558573513441 - k3[2])*k4[1];

Notice that 23620558573513441 is equal to prime - 21888242871839275222246405745257275088548364400416034343698180566017234982176.

The rest of the constants used in the generation of the values in k4 can be calculated in the same way:

consts = [23620558573513441, 12007594160496001, 2100220379136001, 1803906279014401, 7387268108160001, 16789791575437501, 18771962069053126, 15507273013565626, 7381718709890626, 1897417270423126, 1687402949028391, 7404771948190057, 17529594064320097, 17416727046007681, 13111062618776001, 9258575654253001, 10673265496603681, 8194385539754497, 2407628741061889, 2165741790446881, 3368673263124001, 1484258188608001, 1817308501032961, 3795803380482049, 609152945688577, 47068306979329, 54477207152001, 11217882000000001, 909483250000001, 21537584280576001]

Writing our own flag checker

At this point, I knew enough to write my own flag checking script. This script takes in a 32-character flag and returns the calculated value of k4[31]. After testing this script with several 32-character strings, I found that the output matched the values stored in the tmp_public.json files generated after running the check.py script with the same string. This proved that the script was correct.

def check_flag(flag_txt):
    flag = []
    for i in flag_txt: flag.append(ord(i))

    k1 = []
    for i in range(31): k1.append(flag[i]*flag[i+1])
    k1.append(flag[31]*flag[0])

    k2 = []
    for i in range(31): k2.append(k1[i]*k1[i+1])
    k2.append(k1[31]*k1[0])

    k3 = []
    for i in range(31): k3.append(k2[i]*k2[i+1])
    k3.append(k2[31]*k2[0])

    mod = 21888242871839275222246405745257275088548364400416034343698204186575808495617
    consts = [23620558573513441, 12007594160496001, 2100220379136001, 1803906279014401, 7387268108160001, 16789791575437501, 18771962069053126, 15507273013565626, 7381718709890626, 1897417270423126, 1687402949028391, 7404771948190057, 17529594064320097, 17416727046007681, 13111062618776001, 9258575654253001, 10673265496603681, 8194385539754497, 2407628741061889, 2165741790446881, 3368673263124001, 1484258188608001, 1817308501032961, 3795803380482049, 609152945688577, 47068306979329, 54477207152001, 11217882000000001, 909483250000001, 21537584280576001]

    k4 = [None]*32
    k4[1] = ((19762700069597185 - k3[1])*(20182628090806273 - k3[0]))%mod
    for i in range(2, 32):
        k4[i] = ((consts[i-2] - k3[i])*k4[i-1])%mod
    return k4[31]

Generating the flag

Now that we’ve figured out what the flag checker does, it’s time to use that to construct the flag. I was stuck on this step for a long time, and it took me a while to figure out how to approach it.

The formula for k1, k2, and k3 are pretty simple, so we can easily write a formula for k3 based on the characters of the flag: k3[i] = flag[i] * flag[i+1]**3 * flag[i+2]**3 * flag[i+3]. This doesn’t help us right away, since we don’t know the values of k3: the only thing we know for sure is that k4[31] = 1. It’s a start, though.

Since we know that the first characters of the flag are hope{ and the last character is }, we can calculate k3[0], k3[1], and k3[31]. We find that k3[0] is 20182628090806272, k3[1] is 19762700069597184, and k3[31] is 21537584280576000 .

Wait a minute, we’ve seen those values before! The first two constants used in the calculation of k4 are 20182628090806273 and 19762700069597185, and the last one is 21537584280576001.

In our flag checking script, k4[1] = ((19762700069597185 - k3[1])*(20182628090806273 - k3[0])). Substituting in the values we calculated for k3[0] and k3[1], we find that k4[1] should equal 1. Similarly, we can use the value calculated for k3[30] to show that k4[30] is also 1. This suggests that not only is k4[31] equal to 1, but every value in k4 is equal to 1. While that’s not necessarily the only way to get a value of 1 for k4[31], it’s a pretty good guess.

Knowing that, I realized that the values of k3 are basically given to us. Recall that this was the formula used to generate each term of k4:

k4[i] = (constant - k3[i]) * k4[i-1]

If k4[i] and k4[i-1] are both 1, then we’re left with constant = k3[i] + 1. Back when we were writing our flag checker, we already generated a list of all the constants used to generate k3:

    consts = [23620558573513441, 12007594160496001, 2100220379136001, 1803906279014401, 7387268108160001, 16789791575437501, 18771962069053126, 15507273013565626, 7381718709890626, 1897417270423126, 1687402949028391, 7404771948190057, 17529594064320097, 17416727046007681, 13111062618776001, 9258575654253001, 10673265496603681, 8194385539754497, 2407628741061889, 2165741790446881, 3368673263124001, 1484258188608001, 1817308501032961, 3795803380482049, 609152945688577, 47068306979329, 54477207152001, 11217882000000001, 909483250000001, 21537584280576001]

This means that to find the values of k3, all we need to do is subtract 1 from each of these values. Once we have k3, we can write a formula to generate each character of the flag: flag[i+4] = k3[i+1]*(flag[i+1]**2)*flag[i] / (k3[i]*(flag[i+3]**2)).

We now have enough information to write the solve script.

def generate():
    flag_txt = "hope"
    flag = []
    for i in flag_txt: flag.append(ord(i))
    consts = [20182628090806273, 19762700069597185, 23620558573513441, 12007594160496001, 2100220379136001, 1803906279014401, 7387268108160001, 16789791575437501, 18771962069053126, 15507273013565626, 7381718709890626, 1897417270423126, 1687402949028391, 7404771948190057, 17529594064320097, 17416727046007681, 13111062618776001, 9258575654253001, 10673265496603681, 8194385539754497, 2407628741061889, 2165741790446881, 3368673263124001, 1484258188608001, 1817308501032961, 3795803380482049, 609152945688577, 47068306979329, 54477207152001, 11217882000000001, 909483250000001]
    k3 = []
    for i in consts: k3.append(i - 1)
    s = ""
    for i in range(28): 
        v = k3[i+1]*(flag[i+1]**2)*flag[i] / (k3[i]*(flag[i+3]**2))
        flag_txt += chr(int(v))
        flag.append(int(v))
    return flag_txt

This gets us the flag: hope{n0t_so_s3cret_aft3r_4ll...}

Originally posted at https://hackmd.io/@clairelevin/ry6f1ej25