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

## jharmony — 100 pts

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 structfrom 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 - 300pts`
`Cá 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 NdrClientCall2`
`CLIENT_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!`