IDA Challenge

14 Jul 2023

Didn't have time to finish the IDA challenge but below are a couple of notes; I wanted to try some new approaches documented below.

or z3: https://www.youtube.com/watch?v=kZd1Hi0ZBYc

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 decided I'd try and solve this using Ponce ( https://github.com/illera88/Ponce ).

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).

So I decided to download https://sourceforge.net/projects/bochs/ a emulator that supports debugging with IDA. I installed it following instructions in https://www.hex-rays.com/products/ida/support/idadoc/1329.shtml ; Edited the dbg_boch.cfg file in IDA by uncommenting and setting values for:

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.")