HexRays CTF Challenge

[kao]

Quote

Madame de Maintenon (AKA “IDA lady”) is locked in a castle and needs help to escape. Do you think you could free her? Be careful, you might get lost or caught by vicious guardians. Traps are laid along the way, so keep your eyes open, your mind sharp, and capture the flag.

Send us proof of your success (you will receive instructions upon solving the puzzle) before 17:00 CEST, May 26th, 2023. Over 90 brave reversers are already trying to solve it, but do not worry… speed is not essential! We will randomly pick ten winners and award them.

Here is what awaits the winners:

• One Hex-Rays hoodie
• Two T-shirts
• One F5 cap
• Five cup coasters
• For the bravest and luckiest, there will be some BIG Surprises! Want to know what? Follow the updates on our website and social networks, and you’ll find out very soon.

https://hex-rays.com/blog/free-madame-de-maintenon-ctf-challenge/ 

 

 

[NotSure]

 

Has anyone managed to solve it? Could you provide some hints?

I've tried using the Z3 solver, angr, and a partial brute-force approach with a known-plaintext attack (assuming the PNG signature from the encrypted image), but so far, I haven't been successful.

[kao]

@NotSure: 

Spoiler

Z3 is enough. No known-plaintext attack needed. Just add all the correct constraints. 

 

 

 

Edited May 23, 2023 by kao
spoilerssss

[Washi]

Where is my IDA Pro license!1!?1

Jokes aside, it's a fun challenge. I recommend it to any beginner that is just getting into RE and writing solvers.

Spoiler

 

Edited May 24, 2023 by Washi

[kao]

@Washi: I guess we'll have to do a sword fight for that...

[NotSure]

16 hours ago, kao said:

@Washi: I guess we'll have to do a sword fight for that...

well...not so fast guys, I guess we will have to split the license in 3 since I also got the holly image decrypted 🤓.

But to be honest I'm more interested in the Hex-Rays hoodie or T-shirt.

[Luca91]

I tried to take part in this challange, but I'm a noot at z3solver, so I couldn't quickly find a way to cast two 8-bit elements to a 16-bit one (within the bitvector array) and this week I was so fu**ing busy at work, so I gave up (shame on me).

 

Now that the constest is over, is anybody willing to share a papers about how you solved it? Thank you very much.

 

Ah, @Washi @kao and @NotSure I sincerely hope you can get the goods you desire. You guys really deserve an award.

[NotSure]

@Luca91  I just saw Elias Bachaalany made a video about it on his YouTube channel here: All things IDA

 

 my script with comments:

Spoiler

from z3 import *

# Define a helper function to extract a 16-bit value from the key
def extract_16bit(offset):
    return Concat(key[offset+1], key[offset])
    
# Define a helper function to extract a 32-bit value from the key
def extract_32bit(offset):
    return Concat([key[offset + i] for i in range(4)][::-1])

# Define a helper function to extract a 64-bit value from the key
def extract_64bit(offset):
    return Concat([key[offset + i] for i in range(8)][::-1])
    
# Create a Z3 solver instance
solver = Solver()

# Define symbolic variables for the key bytes
key_len = 24  # Modify this value based on the actual length of the key

key = [BitVec(f'key_{i}',8  ) for i in range(key_len)]

# Add constraints based on the conditions in the code

# Condition 1: *(unsigned __int16 *)&key[0x10] + *(unsigned __int16 *)&key[0x16] - *(unsigned __int16 *)&key[8] - *(unsigned __int16 *)&key[0xE] == 0x1CD4
constraint1 = extract_16bit(0x10) + extract_16bit(0x16) - extract_16bit(8) - extract_16bit(0xE) == 0x1CD4
solver.add(constraint1)

# Condition 2: *(unsigned __int16 *)&key[6] + *(unsigned __int16 *)&key[0x14] + *(unsigned __int16 *)&key[2] - *(unsigned __int16 *)&key[0xA] == 0xD899
constraint2 = extract_16bit(6) + extract_16bit(0x14) + extract_16bit(2) - extract_16bit(0xA) == 0xD899
solver.add(constraint2)

# Condition 3: (*(_QWORD *)&key[0x10] ^ *(_QWORD *)key) == 0xA04233A475D1B72
condition = extract_64bit(0x10) ^ extract_64bit(0) == 0xA04233A475D1B72
solver.add(condition)

# Condition 4: 2 * *(_DWORD *)&key[4] + (unsigned int)*(unsigned __int16 *)&key[0x14] - 4 * *(_DWORD *)&key[8] - (*(_QWORD *)&key[0x10] >> 3) - (*(_DWORD *)&key[4] >> 3) == 0x4B5469C

# Extract the necessary values from the key
value_0 = extract_32bit(0)
value_4 = extract_32bit(4)
value_8 = extract_32bit(8)
value_10 = extract_32bit(0x10)
value_14 = extract_32bit(0x14)

# Define the intermediate value
intermediate = value_14 + 2 * value_0 - 4 * value_8 - (value_10 >> 3) - (value_4 >> 3)

# Define the condition
condition = intermediate == 0x4B5469C
solver.add(condition)

# Condition 5: (*(_QWORD *)&key[0x10] ^ *(_QWORD *)&key[8]) == 0x231F0B21595D0455LL
condition = extract_64bit(0x10) ^ extract_64bit(8) == 0x231F0B21595D0455
solver.add(condition)           

# Add additional constraints for printable characters (ASCII range)
for byte in key:
    solver.add(byte >= 0x20, byte <= 0x7E)

# Check if the solver has a satisfying solution
if solver.check() == sat:
    model = solver.model()

    # Extract the concrete byte values for the key
    key_bytes = [model[key[i]].as_long() for i in range(key_len)]

    # Convert the byte values to a string
    key_string = ''.join(chr(byte) for byte in key_bytes)

    print("Success: ", key_string)

    # Add a new constraint to exclude the found key
    solver.add(Or([key[i] != model[key[i]] for i in range(key_len)]))

    # Print the key bytes as hexadecimal
    key_hex = [hex(byte)[2:].zfill(2) for byte in key_bytes]
    print("Key (hex): ", key_hex)
else:
    print("No solution found.")
 

 

Edited May 26, 2023 by NotSure

[Luca91]

Thanks a lot @NotSure

Ok, that's how to extract 16/32/64 bits value from a bitvector! 👍

[kao]

That's obviously one way of doing things. My solution was completely different.

Considering that I'm Z3 newbie, I'm sure Elias' solution is much cleaner.

[mrexodia]

At first I tried to solve it with angr to automatically collect the constraints (using hooks to skip the decryption loops), but but it ended up being much faster to do it by hand:

Spoiler

from z3 import *

arr = [BitVec(f"key_{i}", 8) for i in range(0, 24)]

solver = Solver()

def deref(offset, bytes):
    values = []
    for i in range(0, bytes):
        values.append(arr[i + offset])
    values.reverse()
    return Concat(*values)

def uint16(offset):
    return deref(offset, 2)
def uint32(offset):
    return deref(offset, 4)
def uint64(offset):
    return deref(offset, 8)

# Printable ASCII range
def isascii(c):
    return And(c >= ord(' '), c <= ord('~'))
solver.add(*[isascii(c) for c in arr])

check1 = ZeroExt(16, uint16(16))
check1 += ZeroExt(16, uint16(22))
check1 -= ZeroExt(16, uint16(8))
check1 -= ZeroExt(16, uint16(14))
solver.add(check1 == BitVecVal(0x1CD4, 32)) # 0x1012BF

check2 = ZeroExt(16, uint16(20))
check2 += ZeroExt(16, uint16(6))
check2 += ZeroExt(16, uint16(2))
check2 -= ZeroExt(16, uint16(10))
solver.add(check2 == BitVecVal(0xD899, 32)) # 0x1012E0

check3 = uint64(16) ^ uint64(0)
solver.add(check3 == BitVecVal(0xA04233A475D1B72, 64)) # 0x1013C5

check4 = uint32(20)
check4 += 2 * uint32(0)
check4 -= 4 * uint32(8)
check4 -= uint32(16) >> 3
check4 -= uint32(4) >> 3
solver.add(check4 == BitVecVal(0x4B5469C, 32)) # 0x101447

check5 = uint64(8) ^ uint64(16)
solver.add(check5 == BitVecVal(0x231F0B21595D0455, 64)) # 0x101492

res = solver.check()
if res == sat:
    m = solver.model()

    result = [m.eval(c).as_long() for c in arr]
    s = ''.join([chr(c) for c in result])
    print(f"Password: {s}")
else:
    print("No solution found")

 

 

[NotSure]

another solution using BN from Robert Yates YouTube channel - Solving the Hex-Rays CTF using path driven symbolic execution.

Edited May 28, 2023 by NotSure

[jackyjask]

Hex-Rays SA

@HexRaysSA

And the big prize - the IDA Pro license goes to: Harald Andreasen