Write-ups vòng loại SVATTT 2017 [jharmony, hidden, SerialMe]

jharmony — 100 pts

Thu Nguyen
Nov 7, 2017 · 7 min read

Về cơ bản, thử thách này không khó mà chỉ hơi dài dòng, mình sử dụng z3 để giải

Solve

from z3 import *def to_int(instance): return instance.as_long()checks = [0xbf, 0x86, 0xe2, 0x90, 0x47, 0x42, 0xc3, 0xe7, 0x95, 0xa0, 0x91, 0x41, 0x5, 0x80, 0xe4, 0xa0, 0xa2, 0xd3, 0x47, 0x45, 0x84, 0xbf, 0xb1, 0xfd, 0xcd, 0x7, 0x18, 0xc6]def solve():
s = Solver()
x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27 = BitVecs("x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20 x21 x22 x23 x24 x25 x26 x27", 8)

# Clone variables
x0_ = x0
x1_ = x1
x2_ = x2
x3_ = x3
x4_ = x4
x5_ = x5
x6_ = x6
x7_ = x7
x8_ = x8
x9_ = x9
x10_ = x10
x11_ = x11
x12_ = x12
x13_ = x13
x14_ = x14
x15_ = x15
x16_ = x16
x17_ = x17
x18_ = x18
x19_ = x19
x20_ = x20
x21_ = x21
x22_ = x22
x23_ = x23
x24_ = x24
x25_ = x25
x26_ = x26
x27_ = x27

# Expression
v6 = x1 ^ 215
v7 = x2 ^ 0xF2
x1 = x0 ^ 0xF2
x0 = v6
v8 = x3 ^ 0x91
x3 = x4 ^ 0xA1
x2 = v8
x4 = x5 ^ 0x34
x5 = x6 ^ 0x76
x6 = v7
v9 = x8 ^ 0xD7
v10 = x9 ^ 0xF2
x8 = x7 ^ 0xF2
x7 = v9
v11 = x10 ^ 0x91
x10 = x11 ^ 0xA1
x9 = v11
x11 = x12 ^ 0x34
x12 = x13 ^ 0x76
x13 = v10
v12 = x15 ^ 0xD7
v13 = x16 ^ 0xF2
x15 = x14 ^ 0xF2
x14 = v12
v14 = x17 ^ 0x91
x17 = x18 ^ 0xA1
x16 = v14
x18 = x19 ^ 0x34
x19 = x20 ^ 0x76
x20 = v13
v15 = x22 ^ 0xD7
x22 = x21 ^ 0xF2
x21 = v15
v16 = x24 ^ 0x91
v17 = x27 ^ 0x76
x24 = x25 ^ 0xA1
x27 = x23 ^ 0xF2
x23 = v16
x25 = x26 ^ 0x34
x26 = v17
# Constraints
v = [x0, x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20, x21, x22, x23, x24, x25, x26, x27]
for i in xrange(len(v)):
s.add(v[i] == checks[i])
# Solve
if s.check() == sat:
m = s.model()
flag = "".join(chr(c) for c in map(to_int, [m[x0_], m[x1_], m[x2_], m[x3_], m[x4_], m[x5_], m[x6_], m[x7_], m[x8_], m[x9_], m[x10_], m[x11_], m[x12_], m[x13_], m[x14_], m[x15_], m[x16_], m[x17_], m[x18_], m[x19_], m[x20_], m[x21_], m[x22_], m[x23_], m[x24_], m[x25_], m[x26_], m[x27_]]))
flag += "g3" # last 2 characters
print "Flag is: SVATTT2017{{{}}}".format(flag)

solve()
# Flag is: SVATTT2017{th1s1s4g0r10usR3v3rs3Ch4ll3ng3}hidden - 200 ptsĐọc qua về cấu trúc tập tin Bitmap, mình xây dựng lại một struct header của bitmap để có có thể dễ dàng đọc code
Chương trình nhận 2 tham số là file bitmap và thông điệp cần giấu. Sau đó thông điệp này được mã hóa AES và chuyển thành dạng binary rồi giấu trong pixel arrays (bitmap image data)import struct
from Crypto.Cipher import AES
unpad = lambda x: x[:-ord(x[-1])]def solve():
key = 'dd0ad6afa026634921647a6ddb976133d9363d229c84a8aabd47ce8fd8665e42'.decode("hex")
IV = "e7d61d6d2812bb10e9b610411abadafe".decode("hex")
data = open("hidden.bmp", "rb").read()
flag = "".join([str(ord(data[0x36 + i * 2 + i])) for i in xrange(struct.unpack("<I", data[6: 10])[0])]) # binary data length stored at bitmap_header -> Reversed field
ctext = "".join([chr(int(flag[i: i + 8][::-1], 2)) for i in xrange(0, len(flag), 8)])
c = AES.new(key, AES.MODE_CBC, IV = IV)
print "Flag is: SVATTT2017{{{}}}".format(unpad(c.decrypt(ctext)))

solve()
# Flag is: SVATTT2017{dont_forget_Treasure_hidden_by_one_of_us}
SerialMe - 300ptsCá nhân mình rất thích bài này, vì mình thấy nó lạ, lạ là do mình là một dân dịch ngược nửa-chánh-đạo - mình không biết nhiều về lập trình C/C++ hay các công nghệ/kỹ thuật lập trình của MS (so bad), nên mình sẽ đi chi tiết hơn các bài kia.Bắt đầu với DialogFunc
Bỏ qua các đoạn mã làm rối, đặt breakpoint tại call ebx, mình sẽ tạm đặt tên hàm là ModelessDialog
Đây là lần đầu tiên mình gặp hàm RpcStringBindingComposeW , như thường lệ mình search trên MSDN, đọc xong mình vẫn còn chưa hiểu (tất nhiên rồi). Hàm này nằm trong mục Remote Procedure Call (RPC), lướt qua các chỉ mục con, mình chọn sẽ đọc qua hai articles là Overview > Microsoft RPC Model > How RPC works [1] và Overview > Tutorial > The Client (and Server) Application [2]Về cơ bản RPC là giao thức cho phép client thực thi một method tại một máy khác (server) thông qua network. Dựa vào 2 ví dụ ở trên ta có thể xem hàm ModelessDialog đóng vai trò là client.Hàm setupRpcServer decrypt từ resource BIN  một tập tin DLL, load và gọi DllEntryPoint .
Code trên DLL
OK, có vẻ như là đã đúng hướng. Chúng ta đã có server và client.Xác định được hàm xử lý sự kiện nhấp chuột vào button Check bằng string hoặc GetDlgItemTextA  như thông thường, có thể thấy client sử dụng NdrClientCall2  để thực hiện kiểm tra name và serial (client_postName  và client_checkSerial )
Vậy làm thế nào để xác định được server sử dụng hàm nào, hay nói cách khác server và client giao tiếp với nhau như thế nào. Quay trở lại với hàm NdrClientCall2CLIENT_CALL_RETURN RPC_VAR_ENTRY NdrClientCall2(
_In_ PMIDL_STUB_DESC pStubDescriptor,
_In_ PFORMAT_STRING pFormat,
_Inout_ ...
);

pFormat [in] — Pointer to the MIDL-generated procedure format string that describes the method and parameters

Có thể hiểu đơn giản rằng client và server marshal các thông tin mô tả hàm và tham số cần thực thi theo một cách nào đó, ở đây có đề cập đến MIDL-generated procedure format string (có thể nghĩ đến việc serialize object trong PHP, Java...). Tuy nhiên, sau khi tìm kiếm và không có được thông tin hữu ích, và mình cũng không muốn phải dịch ngược các stub của nó để hiểu cấu trúc, mình sẽ chọn 1 cách làm CTF-way hơn. Mình giả định rằng các format string này phải đồng bộ giữa cả client và server thì mới có thể giao tiếp với nhau. Do đó mình sẽ tìm kiếm các bytes này (̶p̶̶S̶̶t̶̶u̶̶b̶̶D̶̶e̶̶s̶̶c̶̶r̶̶i̶̶p̶̶t̶̶o̶̶r̶ *pFormat ) trên server (DLL space)
Kết quả hoàn toàn như mong đợi, mình sẽ đặt 1 hardware breakpoint tại đây (có 1 lưu ý nhỏ là các bạn có thể đặt 1 hoặc 2 bytes, do địa chỉ này không align 4 bytes nên không thể đặt được một dword-bp). Breakpoint này triggered ngay sau khi nhấn Check
Chương trình đang dừng tại một mã lệnh trong thư viện rpcrt4.dll , tới đây, mình sử dụng một tính năng trên x64dbg là Singleshoot (memory execute) trên vùng nhớ DLL được load lên
Breakpoint này được trigger ngay tại hàm chúng ta cần tìm (tức là hàm client cần gọi đến), tạm gọi là getName
Client gửi lên server hai tham số là 0x1337  và một giá trị được biến nổi từ tên nhập vào, hàm getName thực hiện gán các giá trị này lần lượt cho hai biến toàn cục.Bằng cách tương tự có thể xác định được hàm kiểm tra serial
Đến đây bài toán coi như đã được giải quyết, mình có viết 1 script nhỏ, nó tệ, nhưng đại khái là "chạy" được.from z3 import *def to_int(instance):
try: return instance.as_long()
except: return instance

def post_name(name):
result = 0
for i in xrange(len(name)):
result = ord(name[i]) + result * 2
return result
def keygen(name):
s = Solver()
nname = post_name(name)
magic = 0x1337
x0, x1, x2, x3, x4, x5, x6, x8, x9, x10, x11, x12, x13, x14 = BitVecs("x0 x1 x2 x3 x4 x5 x6 x8 x9 x10 x11 x12 x13 x14", 16)
for x in [x0, x1, x2, x3, x4, x5, x6, x8, x9, x10, x11, x12, x13, x14]:
s.add(x >= 32, x < 127)
s.add(((nname ^ (x6 + 5 * x1 + 11 * x2 + 31 * x4 + 43 * x5 + 3 * (x0 + 9 * x3))) + (magic ^ (x14 + 5 * x9 + 11 * x10 + 31 * x12 + 43 * x13 + 3 * (x8 + 9 * x11)))) == 0x5a5a)
if s.check() == sat:
m = s.model()
return "".join(chr(c) for c in map(to_int, [m[x0], m[x1], m[x2], m[x3], m[x4], m[x5], m[x6], ord("-"), m[x8], m[x9], m[x10], m[x11], m[x12], m[x13], m[x14]]))
return ""
def main():
name = raw_input("name? ")
print "serial: {}".format(keygen(name))
if __name__ == '__main__':
main()
Cảm ơn vì đã đọc đến dòng cuối cùng!

nightst0rm

NightSt0rm is a group of IT security researchers, enthusiasts , who share the same interests. We are focusing on Hacking, Cryptography, Malware analyst & Computer forensics.

Thu Nguyen

Written by

nightst0rm

NightSt0rm is a group of IT security researchers, enthusiasts , who share the same interests. We are focusing on Hacking, Cryptography, Malware analyst & Computer forensics.