So both approaches were interesting but the SENinja approach wasn't leveraging IDA and I have all my favorite plugins in IDA. The second z3 approach involved writing a z3 script which isn't the end of the world but seemed more time consuming than approach 1.
I downloaded the file and first thing I noticed was this was an ElF executable and I'm running on windows. The easiest way to solve this is to run the binary in WSL with remote GDB debugger. However, I did not have WSL installed on this host and didn't want to bother with the set-up (This host was on a Windows 11 insider deprecated build and I've had a bit of pain getting HyperV and WSL to coexsist without needing reboots).
BOCHSDBG and BOCHSRC and I was now debugging an ELF on windows in IDA! Nice!
I hit an issue at first as the ELF base adress was set to 0x0. Rebasing it to 0x4000 fixes our error.
As soon as our BP hits, we symbolize the rsi register:
Next, we run untill a symbolic condition is encountered. A symbolic condition is a constraint that will use our symbolic register in it's evaluation:
Unfortunately, my approach using Bosch kept crashing and I'm not sure why.
I decided to try something else.
Decompiled the code and passed it to GPT4 for analysis asking it to list the constraints for password:
User: Please list all condition checks that are performed on password
ChatGPT
ChatGPT: Certainly! Here are all the condition checks that are performed on the password in the given C function:
The sum of certain pairs of 2-byte values in the password should equal 7380:
*(unsigned __int16 *)&password[16] + *(unsigned __int16 *)&password[22] - *(unsigned __int16 *)&password[8] - *(unsigned __int16 *)&password[14] == 7380
The sum of certain pairs of 2-byte values in the password should equal 55449:
*(unsigned __int16 *)&password[20] + *(unsigned __int16 *)&password[6] + *(unsigned __int16 *)&password[2] - *(unsigned __int16 *)&password[10] == 55449
A bitwise XOR operation between two 8-byte values in the password should equal 0xA04233A475D1B72:
(*(_QWORD *)&password[16] ^ *(_QWORD *)password) == 0xA04233A475D1B72LL
The sum of certain arithmetic operations involving the 4-byte values in the password should equal 78988956:
*(_DWORD *)&password[20] + 2 * *(_DWORD *)password - 4 * *(_DWORD *)&password[8] - (*(_DWORD *)&password[16] >> 3) - (*(_DWORD *)&password[4] >> 3) == 78988956
The XOR result of certain pairs of 4-byte values in the password should equal 0x231F0B21595D0455:
(*(_QWORD *)&password[8] ^ v7) == 0x231F0B21595D0455LL
These condition checks likely serve as validation or authentication mechanisms for the password. Depending on the specific values of the password, different memory data will be loaded and used by the program.
Well this is actually pretty impressive!
I tried to ask it to write the z3 solver and ended up with something pretty decent (even though it didn't work):
from z3 import *
def words(byte1, byte2):
return Concat(byte2, byte1)
def dword(byte1, byte2, byte3, byte4):
return Concat(byte4, byte3, byte2, byte1)
def qword(byte1, byte2, byte3, byte4, byte5, byte6, byte7, byte8):
return Concat(byte8, byte7, byte6, byte5, byte4, byte3, byte2, byte1)
def solve_password():
password = [BitVec(f"password_{i}", 8) for i in range(24)]
# ASCII constraint
ascii_constraint = And([And(password[i] >= 32, password[i] <= 126) for i in range(24)])
# Length constraint
length_constraint = len(password) == 24
# First condition: Sum of specific pairs equals 7380
condition1 = words(password[16], password[17]) + \
words(password[22], password[23]) - \
words(password[8], password[9]) - \
words(password[14], password[15]) == BitVecVal(7380, 16)
# Second condition: Sum of specific pairs equals 55449
condition2 = words(password[20], password[21]) + \
words(password[6], password[7]) + \
words(password[2], password[3]) - \
words(password[10], password[11]) == BitVecVal(55449, 16)
# Third condition: XOR operation results in 0xA04233A475D1B72
condition3 = (qword(password[16], password[17], password[18], password[19],
password[20], password[21], password[22], password[23]) ^
qword(password[0], password[1], password[2], password[3],
password[4], password[5], password[6], password[7])) == BitVecVal(0xA04233A475D1B72, 64)
# Fourth condition: Sum of arithmetic operations equals 78988956
condition4 = dword(password[20], password[21], password[22], password[23]) + \
2 * dword(password[0], password[1], password[2], password[3]) - \
4 * dword(password[8], password[9], password[10], password[11]) - \
(dword(password[16], password[17], password[18], password[19]) >> 3) - \
(dword(password[4], password[5], password[6], password[7]) >> 3) == BitVecVal(78988956, 32)
# Fifth condition: XOR result equals 0x231F0B21595D0455
condition5 = (qword(password[8], password[9], password[10], password[11],
password[12], password[13], password[14], password[15]) ^
qword(password[7], password[6], password[5], password[4],
password[3], password[2], password[1], password[0])) == BitVecVal(0x231F0B21595D0455, 64)
# Create a solver and add all conditions
solver = Solver()
solver.add( length_constraint,condition1, condition2, condition3, condition4, condition5)
# Check if the solver is satisfiable and find a solution
if solver.check() == sat:
model = solver.model()
result = ""
for i in range(24):
char = chr(model[password[i]].as_long())
result += char
return result
return None
# Solve the password and print the result
password = solve_password()
if password:
print("Password:", password)
else:
print("No solution found.")
