This is my write-up of a Reversing challenge The Secret Lock on the CTF site 247CTF.com.
Can you reverse the secret combination to open the lock and recover the flag?
I won’t go into details, basically it is a SAT solver problem. The thing I want to point out is that the most problems I’ve had with the python libraries.
The problem I got was:
NameError: name 'BitVec' is not defined
If you try to install z3 from pip, you will be unpleasantly surprised to find out that there are many z3 packages, and the first one is not the right tool for the job.
$ pip3 search z3
z3 (0.2.0) - Backup ZFS snapshots to S3
INSTALLED: 0.2.0 (latest)
z3-tracker (0.9.9) - Helper program for Link to the Past randomiser
z3-solver (4.8.7.0) - an efficient SMT solver library
INSTALLED: 4.8.7.0 (latest)
z4-solver (2019.10.12.2) - z3++
z3-solver-mythril (4.8.4.1) - an efficient SMT solver library
z3gi (0.1.1) - Grammatical inference using the Z3 SMT solver
pymxml (2.8) - Python wrapper for mini-xml(http://www.msweet.org/projects.php?Z3)
collective.z3cform.datagridfield (1.5.3) - Fields with repeatable data grid (table-like) for z3.cform
$ pip3 install z3-solver
$ pip3 uninstall z3
So to make the library work, you need to uninstall the z3 and install the z3-solver.
And a little vim tip, to modifiy the conditional statements (from js to python syntax), you can use:
:%s/&&/,\r/g
So search for && and replace it with , followed by new line \r.