Unbreakable Enterprise Product Activationをz3pyを使って解いてみる
はじめに
z3pyにkatagaitai勉強会#6 - 関西|easyで入門したので、練習がてらGoogle CTF 2016のUnbreakable Enterprise Product Activationを解いた。 この問題を人力で解くのは難しく、競技期間中は解けなかったが、z3pyを使えば楽に解くことができた。
実行してみる
$ ./unbreakable-enterprise-product-activation unbreakable-enterprise-product-activation: ./unbreakable_enterprise_product_activation product-key $ ./unbreakable-enterprise-product-activation aaaa Product activation failure 255
正しいproduct-keyがflagになりそうと分かる。
静的解析
0x4005aaから0x4005b8までの処理では入力したproduct-keyをコピーしている。0x4005bfから0x40071bまでつづくcallによって、0x4027f0から0x403440にproduct-keyをチェックする処理を呼んでいる。
4005aa mov rsi, qword [ds:rsi+8] ; src address 4005ae mov edx, 0x43 ; size 4005b3 mov edi, 0x6042c0 ; dist address 4005b8 call j_strncpy 4005bd xor eax, eax 4005bf call 0x4027f0 4005c4 xor eax, eax 4005c6 call 0x402830 4005cb xor eax, eax 4005cd call 0x402870 4005d2 xor eax, eax 4005d4 call 0x4028c0
以下のようなproduct-keyをチェックする処理が50個ほどあり、人力で解くのは難しいと分かる。
4027f0 movzx edx, byte [ds:0x6042e6] ; XREF=sub_400590+47 4027f7 movzx eax, byte [ds:0x6042de] 4027fe movzx ecx, byte [ds:0x6042c6] 402805 movzx esi, byte [ds:0x6042c8] 40280c movzx edi, byte [ds:0x6042c0] 402813 xor eax, edx 402815 sub eax, esi 402817 add eax, ecx 402819 cmp dil, al
また、strcpyのコピー先でXREFがついているアドレスは0x6042c0から0x6042f2だったので、flagの長さは51だと分かった。
6042c0 db 0x00 ; '.' ; XREF=sub_400590+35, sub_400870+9, sub_400870+30, sub_400870+2932, sub_400870+4029, sub_400870+4644, sub_400870+4934, sub_400870+6356, sub_400870+7477, sub_400870+8092, sub_400870+9189, … 6042c1 db 0x00 ; '.' ; XREF=sub_400870+47, sub_400870+65, sub_400870+2954, sub_400870+3889, sub_400870+4666, sub_400870+5244, sub_400870+6378, sub_400870+6980, sub_400870+8156, sub_400870+8528, sub_400870+9902, … 6042c2 db 0x00 ; '.' ; XREF=sub_400870+83, sub_400870+103, sub_400870+2977, sub_400870+4007, sub_400870+4651, sub_400870+4689, sub_400870+6401, sub_400870+6527, sub_400870+8227, sub_400870+9088 6042c3 db 0x00 ; '.' ; XREF=sub_400870+122, sub_400870+141, sub_400870+3001, sub_400870+3675, sub_400870+4713, sub_400870+5824, sub_400870+6425, sub_400870+7099, sub_400870+8213, sub_400870+8307, sub_400870+9182, … 6042c4 db 0x00 ; '.' ; XREF=sub_400870+161, sub_400870+179, sub_400870+3026, sub_400870+3034, sub_400870+4738, sub_400870+5100, sub_400870+6450, sub_400870+6598, sub_400870+8366, sub_400870+8414, sub_400870+8421, … 6042c5 db 0x00 ; '.' ; XREF=sub_400870+197, sub_400870+215, sub_400870+3050, sub_400870+4074, sub_400870+4762, sub_400870+5078, sub_400870+6474, sub_400870+6956, sub_400870+8428, sub_400870+8592, sub_400870+8599, … ...
z3pyを使う
コード
#!/usr/bin/env python2.7 # coding: UTF-8 from z3 import * FLAG_LENGTH = 0x6042f2 - 0x6042c0 + 1 s = Solver() text = [] for i in xrange(FLAG_LENGTH): text.append(BitVec(i, 8)) s.add(And(text[i] >= 0x20, text[i] < 0x7f)) # in printable ascii s.add(text[0] == text[6] + (text[38] ^ text[30]) - text[8]) s.add(text[1] == (text[42] ^ (text[38] ^ text[20] ^ text[19]))) s.add(text[2] == text[35] + text[36] - text[19] - text[3] - text[44]) s.add(text[3] == text[19] + (text[17] ^ (text[41] - text[10] - text[10]))) s.add(text[4] == text[33] - text[21]) s.add(text[5] == (text[4] ^ (text[4] ^ text[8] ^ text[39]))) s.add(text[6] == (text[14] ^ (text[10] + text[25] - text[39]))) s.add(text[7] == text[32] + (text[15] ^ text[1])) s.add(text[8] == text[8]) s.add(text[9] == (text[24] ^ text[7])) s.add(text[10] == text[32] + (text[49] ^ text[17]) - text[4]) s.add(text[11] == (text[42] ^ text[38]) - text[17] - text[8]) s.add(text[12] == text[14] + text[8]) s.add(text[13] == text[45] + text[20]) s.add(text[14] == text[9] + (text[20] ^ (text[25] - text[48]))) s.add(text[15] == text[18] - text[31]) s.add(text[16] == (text[24] ^ text[46])) s.add(text[17] == ((text[13] + text[2] + text[47]) ^ (text[14] ^ text[50]))) s.add(text[18] == text[0] + text[36] + text[44] - text[3]) s.add(text[19] == (text[41] ^ text[30]) - text[25] - text[28]) s.add(text[20] == (text[25] ^ text[44])) s.add(text[21] == text[25] + ((text[28] + text[22]) ^ (text[39] ^ text[21]))) s.add(text[22] == (text[31] ^ (text[44] - text[4] - text[12])) - text[30]) s.add(text[23] == (text[39] ^ (text[32] - text[14]))) s.add(text[24] == (text[21] ^ (text[0] ^ text[18] ^ text[21]))) s.add(text[25] == text[18] + text[4] + (text[12] ^ text[17]) - text[11]) s.add(text[26] == (text[32] ^ text[46]) + text[49] + text[20]) s.add(text[27] == text[36] + text[25] + text[39] - text[48]) s.add(text[28] == (text[14] ^ text[15])) s.add(text[29] == text[1] + text[35] - text[42]) s.add(text[30] == text[8] - text[31] - text[30] - text[24]) s.add(text[31] == (text[42] ^ (text[15] + text[18] - text[29]))) s.add(text[32] == text[14] + text[5] + text[15] - text[44]) s.add(text[33] == (text[20] ^ (text[45] - text[15])) - text[32]) s.add(text[34] == (text[3] ^ text[33]) - text[20] - text[10]) s.add(text[35] == (text[44] ^ (text[6] - text[43])) + text[1] - text[44]) s.add(text[36] == (text[49] ^ (text[31] + text[25] - text[28]))) s.add(text[37] == text[11] + (text[34] ^ text[31]) - text[34]) s.add(text[38] == text[42] + (text[27] ^ text[36]) - text[5]) s.add(text[39] == (text[37] ^ text[8])) s.add(text[40] == (text[44] ^ (text[7] + text[28])) - text[10]) s.add(text[41] == (text[20] ^ (text[7] ^ text[17] ^ text[26]))) s.add(text[42] == text[50] + text[1] - text[28]) s.add(text[43] == text[46] + text[33] - text[15]) s.add(text[44] == ((text[24] + text[42] + text[16]) ^ (text[45] ^ text[21]))) s.add(text[45] == text[22] - text[40]) s.add(text[46] == text[12] - text[46] - text[7] - text[35]) s.add(text[47] == (text[39] ^ (text[15] + text[26])) - text[12]) s.add(text[48] == (text[11] ^ (text[15] - text[8]))) s.add(text[49] == (text[27] ^ text[37])) s.add(text[50] == ((text[13] + text[8] + text[17]) ^ (text[24] ^ text[15]))) if s.check() == sat: m = s.model() flag = '' for i in xrange(FLAG_LENGTH): flag += chr(int(str(m[text[i]]))) print('RESULT : {0}'.format(flag))
結果
$ python unbrekable.py
RESULT : CTF{0The1Quick2Brown3Fox4Jumped5Over6The7Lazy8Fox9}
$ ./unbreakable-enterprise-product-activation CTF{0The1Quick2Brown3Fox4Jumped5Over6The7Lazy8Fox9}
Thank you - product activated!
