Write-up for Hex-Rays CTF #1

After having done the second Hex-Rays CTF challenge, I figured it would be fun to try their earlier challenge as well. Together with Jille, this one proved considerably easier.

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.

As before, the challenge consists of a single ELF file. We waste no time loading it into IDA, and are presented with a fairly readable main function. After minor cleanup, we identify interesting fragments:

[..]
char password[25]; // [rsp+50h] [rbp-58h] BYREF
[..]
if ( argc <= 1 )
{
  __fprintf_chk(stderr, 1LL, "You need to give the password as the argument");
  result = 1;
}
else
{
  arg1 = argv[1];
  memset(password, 0, sizeof(password));
  strncpy(password, arg1, 24uLL);
[..]

We need to input a password of (at most) 24 characters.

[..]
if ( *(unsigned __int16 *)&password[16]
    + *(unsigned __int16 *)&password[22]
    - *(unsigned __int16 *)&password[8]
    - *(unsigned __int16 *)&password[14] != 7380 )
  goto LABEL_4;
if ( *(unsigned __int16 *)&password[20]
    + *(unsigned __int16 *)&password[6]
    + *(unsigned __int16 *)&password[2]
    - *(unsigned __int16 *)&password[10] != 55449 )
  goto LABEL_4;
password_16 = *(_QWORD *)&password[16];
if ( (*(_QWORD *)&password[16] ^ *(_QWORD *)password) != 0xA04233A475D1B72LL )
  goto LABEL_4;
[..]
if ( *(_DWORD *)&password[20]
    + 2 * *(_DWORD *)password
    - 4 * *(_DWORD *)&password[8]
    - (*(_DWORD *)&password[16] >> 3)
    - (*(_DWORD *)&password[4] >> 3) != 78988956 )
  goto LABEL_4;
[..]
if ( (*(_QWORD *)&password[8] ^ password_16) == 0x231F0B21595D0455LL )
{
[..]
}

The password needs to meet a series of constraints. When we match the constraints, a large block of data is modified. When we don’t, we jump to LABEL_4.

[..]
    if ( (*(_QWORD *)&password[8] ^ password_16) == 0x231F0B21595D0455LL )
    {
[..]
      v4 = SDL_RWFromConstMem(&unk_711E0, &unk_ECD6C);
    }
    else
    {
LABEL_4:
      v4 = SDL_RWFromConstMem(&unk_4020, &unk_6D1BA);
    }
    Texture_RW = IMG_LoadTexture_RW(v18, v4, 1LL);
[..]

After making it through the checks, v4 is set to point to the modified data block. Otherwise, if we end up at LABEL_4, v4 is set to the buffer at 0x4020. The result is then rendered as a PNG.

At 0x4020, we indeed find a PNG header.

.data:0000000000004020 wrong_png       db  89h                 ; DATA XREF: main+D0↑o
.data:0000000000004021                 db  50h ; P
.data:0000000000004022                 db  4Eh ; N
.data:0000000000004023                 db  47h ; G
.data:0000000000004024                 db  0Dh
.data:0000000000004025                 db  0Ah
.data:0000000000004026                 db  1Ah
.data:0000000000004027                 db  0Ah
[..]

When we view the image (e.g., by selecting Open picture from the context menu), we’re presented with an image telling us we’re not looking in the right place.

The alternative value of v4 (at 0x711E0) looks like random noise; presumably this is the encrypted flag.

The search space for the password is way too big for brute force, but we have a bunch of conditions that we can plug into a constraint solver.

from z3 import *

s = Solver()

pwd = [BitVec(f"p{i}", 8) for i in range(24)]
pwd_int16 = [Concat(*reversed(pwd[i : i + 2])) for i in range(0, 24, 2)]
pwd_int32 = [Concat(*reversed(pwd[i : i + 4])) for i in range(0, 24, 4)]
pwd_int64 = [Concat(*reversed(pwd[i : i + 8])) for i in range(0, 24, 8)]

s.add(pwd_int16[8] + pwd_int16[11] - pwd_int16[4] - pwd_int16[7] == 7380)
s.add(pwd_int16[10] + pwd_int16[3] + pwd_int16[1] - pwd_int16[5] == 55449)
s.add(
    pwd_int32[5]
    + 2 * pwd_int32[0]
    - 4 * pwd_int32[2]
    - (pwd_int32[4] >> 3)
    - (pwd_int32[1] >> 3)
    == 78988956
)

s.add(pwd_int64[2] ^ pwd_int64[0] == 0xA04233A475D1B72)
s.add(pwd_int64[1] ^ pwd_int64[2] == 0x231F0B21595D0455)

for c in pwd:
    s.add(32 <= c, c <= 127)

sat = s.check()
print(sat)
m = s.model()
for c in pwd:
    print(chr(m[c].as_long()), end="")

This immediately presents us with the password: Fr33_M4dam3-De/M4inten0n.

Remarks:

1. Initially, I tried c < 128 to check for ASCII characters. As __lt__ is a signed comparison on BitVecRef objects and the BitVecs are 8 bits, this lead to an unsatisfiable set of constraints: 128 = 0b10000000 is actually -128 when interpreted as a signed 8-bit integer.
2. The endianness of the int16, int32 and int64 values is important: we ensure little-endian integers by using reversed().

Running the challenge requires an x86 Linux system with SDL libraries installed (libsdl2-2.0-0 and libsdl2-img-2.0-0).