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 AESunpad = 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  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 
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 resultdef 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.