[MeePwn CTF] Missing Hash write up

For English version, please read below.

Binary: crackme2_fix4

Tiếng Việt

Mô tả

Thử thách này có thể mô tả như sau:
Tại địa chỉ 0x401588, chương trình hiển thị thông báo "Enter Your Hero: ", yêu cầu nhập vào một chuỗi printable, tạm gọi là heroName. Chuỗi kí tự này có kích thước 10 bytes. Khi nhận chuỗi này, chương trình sẽ thông qua 1 hàm tại địa chỉ 0x401500, tính toán các giá trị và lưu lại các giá trị này. Tôi cũng không quan tâm tới các giá trị này lắm. Sau đây là giả mã của hàm 0x401500.

unsigned __int16 __cdecl sub_401500(char *a1, __int16 *a2, unsigned __int16 a3)
{
unsigned __int16 v4; // [sp+Eh] [bp-Ah]@1
signed int i; // [sp+10h] [bp-8h]@1

v4 = a3;
for ( i = 0; (signed __int16)a3 > i; ++i )
{
v4 = (~a2[i] & v4) + (~v4 & a2[i]);
LOBYTE(v4) = v4 + a1[i];
}
return v4;
}

 

Một heroName sẽ được gọi là hợp lệ nếu thỏa mãn tất cả các điều kiện sau:

  • kí tự đầu tiên là 'Z'
  • kí tự cuối cùng là '!'
  • các giá trị tại các địa chỉ sau bằng 0: 0x403040, 0x403042, 0x403044, 0x403046, 0x403048, 0x40304A, 0x40304C, 0x40304E, 0x403050

Cách giải

Để giải thử thách này, tôi sử dụng angr binary analysis framework . Tôi thiết lập trạng thái bắt đầu tại địa chỉ 0x4015B6, chương trình sẽ bắt đầu phân tích sau khi một chuỗi heroName giả định được nhập vào. Chuỗi kí tự được nhập vào sẽ lưu tại địa chỉ 0x040305A, tôi sẽ đặt tại địa chỉ này một symbolic bitvector (BVS), có kích thước đúng bằng số kí tự nhập vào (10 kí tự * 8 bits). Các kí tự này đều là printable nên tôi sẽ thêm ràng buộc: kí tự nằm trong khoảng 0x20<=x<=0x7e. Chúng ta cần tìm một chuỗi có thể để chương trình "chạy" đến địa chỉ 0x401B21, và chắc chắn không bao giờ đến địa chỉ 0x00401B1. Sau khi tìm thành công 1 "đường" để có thể đến được 0x401B21, ta biết được sẽ có rất nhiều giá trị phù hợp với "đường" này. Để tìm ra cờ chính xác, ta cần thêm một só ràng buộc phù hợp với điều kiện ở trên. Script mất khoảng gần 3 giây để thực thi và tìm ra giá trị phù hợp.

Toàn bộ code được tôi để phía bên dưới: crackme2.py

English version

Analyze

The program displays a message: "Enter Your Hero: ", and you must enter a printable string, I call it heroName. The length of heroName is 10. The program will calculate many values from input tring and store these values. I don't care about these values. The program uses only one function at 0x401500. There is the pseudocode of this function:

unsigned __int16 __cdecl sub_401500(char *a1, __int16 *a2, unsigned __int16 a3)
{
unsigned __int16 v4; // [sp+Eh] [bp-Ah]@1
signed int i; // [sp+10h] [bp-8h]@1

v4 = a3;
for ( i = 0; (signed __int16)a3 > i; ++i )
{
v4 = (~a2[i] & v4) + (~v4 & a2[i]);
LOBYTE(v4) = v4 + a1[i];
}
return v4;
}

A valid heroName MUST satisfy the following conditions:

  • the fist character is 'Z'
  • the last character is '!'
  • all the values at these addresses are equal to 0: 0x403040, 0x403042, 0x403044, 0x403046, 0x403048, 0x40304A, 0x40304C, 0x40304E, 0x403050

Solution

To solve this challenge, I use angr binary analysis framework. I set the entry state at 0x4015B6, angr will start to analyze after a symbolic string is stored. The input string is stored in 0x040305A, I store a symbolic bitvector (BVS) in 0x040305A, its size is 10 chars * 8 bits. All these characters are printable, so I add more constraint: 0x20 <= character <= 0x7e. We need to find a path to 0x401B21, and avoid 0x00401B1. After finding a path, we know there are many acceptable strings. To find the correct one, we need to add some constraints that matchs to the conditions of a valid heroName.

The solution is here: crackme2.py

Crackme2.py

Key: Zer0C0d3r!

import angr

# load the binary into an angr project.
proj = angr.Project('crackme2_fix4.exe', load_options={"auto_load_libs": False})
# I'm going to skip all the beginning of the program.
state = proj.factory.entry_state(addr=0x004015B6)

# scanf() reads from stdin and stores it a this address
bind_addr = 0x040305A
# a symbolic input string with a length up to 10 bytes
input_string = state.se.BVS("input_string", 8 * 10)
# To be safe, I'm constraining input string. They are printable characters
for byte in input_string.chop(8):
state.add_constraints(byte >= ' ') # '\x20'
state.add_constraints(byte <= '~') # '\x7e'
state.add_constraints(byte != 0) # null

# bind the symbolic string at bind_addr
state.memory.store(bind_addr, input_string)

# Attempt to find a path
path = proj.factory.path(state=state)
ex = proj.surveyors.Explorer(start=path, find=0x401B21, avoid=0x00401B1)
ex.run()

state = ex.found[0].state
# We know all the values at: 0x403040, 0x403042, 0x403044, 0x403046, 0x403048, 0x40304A, 0x40304C, 0x40304E, 0x403050
for i in range(18):
state.add_constraints(state.memory.load(0x408040 + i, 1) == 0)
# We know the flag starts with "Z" and ends with "!"
state.add_constraints(state.memory.load(bind_addr + 9, 1) == '!')
state.add_constraints(state.memory.load(bind_addr, 1) == 'Z')

print 'Found:', state.se.any_str(input_string)
# Zer0C0d3r!
# 2.7s