When I try to solve this crackme chall (https://crackmes.one/crackme/61ffb07c33c5d46c8bcbfc1d) , there is a condition that I can't bypass and my z3 script can't predict the input string that will bypass the condition

enter image description here

and this is my z3 script

from z3 import *

v7 = [123,456,789,987,654,321]
v6 = [92,29,380,2,497,296]

s = [BitVec(f'a{i}', 8) for i in range(5)]

solver = Solver()

v20 = 0x7FFFFFFF
for i in range(5):
    v20 += i * s[i]
    solver.add(v20 % v7[i] == v6[i])

  • The function has much more logic and you need to add that in the script too
    – sudhackar
    Apr 22 at 14:02

1 Answer 1


It is to note that the division in the binary is unsigned while according to doc

Use the function URem() for unsigned remainder, and SRem() for signed remainder.

% operator by default is an alias for SRem or signed modulo. You need to use URem. I have fixed your logic as well in this code

from z3 import *

v7 = [123,456,789,987,654,321]
v6 = [92,29,380,2,497,296]
arrl = 14
argv1 = [BitVec(f'a{i}', 32) for i in range(arrl)]

solver = Solver()
v18 = BitVecVal(0x7fffffff, 32)

for i in range(arrl):
    solver.add(argv1[i] < 128)
    solver.add(argv1[i] > 32)
    v18 += i*argv1[i]

for i in range(6):
    solver.add(URem(v18, v7[i]) == v6[i])

print("".join(map(chr,[solver.model()[argv1[i]].as_long() for i in range(arrl)])))

Please note that this won't solve the problem, It has additional checks.

  • Thanks! as you see there is if ( ((unsigned int (__fastcall *)(char *, size_t))v14)(a2[1], v5) ) in decompiled code, can you explain what this check do ? and what does this mean (unsigned int (__fastcall *)(char *, size_t)) ?
    – Int Ver
    Apr 22 at 18:36
  • @IntVer You can open a new question for that. hint: its a function pointer
    – sudhackar
    Apr 22 at 19:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.