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
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 (18.104.22.168) - an efficient SMT solver library INSTALLED: 22.214.171.124 (latest) z4-solver (2019.10.12.2) - z3++ z3-solver-mythril (126.96.36.199) - 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
And a little vim tip, to modifiy the conditional statements (from js to python syntax), you can use:
So search for
&& and replace it with
, followed by new line