Problem files
Solve script
Points
800
Description
Can you crack the key to decrypt map2 for us? The key to map1 is 11443513758266689915.
Hints
Have you heard of z3?
How to solve
The decrypt.py script takes as input an integer key and a map file. The code does some bizzare operation in verify() to determine if the key is correct, and then decrypts the key to a string. Since it tells us in the description “the key to map1 is 11443513758266689915,” we can try this as initial experimentation.
$ python2 decrypt.py 11443513758266689915 map1.txt
Congrats the flag for map1.txt is: not_a_flag{Real_flag_will_be_loooooooonger_than_me}
At this point, you can guess that you need to determine the key for map2.txt, run it with the script, and it will give you the flag. The hint suggests that we can use z3py for this, a python library that can solve a series of constraints. We can treat verify() returning nonzero as a z3 constraint. Since this script is already written in python, only a few modifications can make it solve for the correct key.
How to solve (continued)
z3 allows symbolic execution. This means that instead of performing calculations with concrete values, the inputs to the calculations are variables. This allows us to find the input to an algorithm that makes the output a certain value. z3py provides two types of integer symbols: Int and BitVec. The former is substantially slower, but the second requires that we know the amount of bits. For this challenge, we can determine a maximum number of bits with the following line.
key = int(sys.argv[1]) % (1 << chalbox[0])
This means any key value greater than or equal to (1 << chalbox[0]) will wrap around back to zero. Using this, we can compute the maximum amount of bits with int(math.log2(1 << chalbox[0])) + 1. After doing this, we can use z3 to solve the constraint verify(key, chalbox) != 0 for the correct key. Feeding this key into decrypt.py gives us the flag.
$ python keygen.py 000 map2.txt
Mod operand: 340282366920938463463374607431768211456
Attempting to decrypt map2.txt...
Type of constraint: <class 'z3.z3.BoolRef'>
Got the key \o/
219465169949186335766963147192904921805
$ python2 decrypt.py 219465169949186335766963147192904921805 map2.txt
Attempting to decrypt map2.txt...
Congrats the flag for map2.txt is: picoCTF{36cc0cc10d273941c34694abdb21580d__aw350m3_ari7hm37ic__}