読者です 読者をやめる 読者になる 読者になる

Unbreakable Enterprise Product Activationをz3pyを使って解いてみる

CTF reversing

はじめに

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!

参考記事