6.2.2 re ECTF2016 tayy
章节 5.8.1 中讲解了 Z3 约束求解器的基本使用方法，通过这一题，我们可以更进一步地熟悉它。
题目解析
Tayy is the future of AI. She is a next level chatbot developed by pro h4ckers at NIA Labs. But Tayy hides a flag. Can you convince her to give it you?
$ file tayy
tayy: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=1fcd1c49eae4807f77d51227a3b457d8874170b4, not stripped
$ ./tayy
=============================================================
Welcome to the future of AI, developed by NIA Research, Tayy!
=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 2
Flag: EEXL�▒#@N5&[g,q2H7?09:G>4!O]iJ('
V
=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 1
=============================================================
1. Ayy lmao, Tayy lmao.
2. You are very cruel.
3. Memes are lyf.
4. Go away!.
5. zzzz
6. Cats > Dogs.
7. Dogs > Cats.
8. AI is overrated?.
9. I dont like you.
0. <exit to menu>
> 1
Tayy: Die, human!
=============================================================
1. Talk to Tayy.
2. Flag?
0. Exit.
> 2
Flag: EFZO�*$IX@2hv<�D[KTFPR`XO=l{�jII-z
=============================================================
玩了一会儿我们发现：
- 每次我们与 Tayy 交谈后，flag 就会变
- 最多可以交谈 8 次，然后程序退出
通过调试，我们首先发现了 flag 的初始值：
gdb-peda$ n
[----------------------------------registers-----------------------------------]
RAX: 0x0
RBX: 0x0
RCX: 0x0
RDX: 0x7ffff7dd4710 --> 0x0
RSI: 0x7fffffffe460 --> 0x231819834c584545
RDI: 0x400d2c ("Flag: %s\n")
RBP: 0x7fffffffe490 --> 0x400a70 (<__libc_csu_init>: push r15)
RSP: 0x7fffffffe450 --> 0x2
RIP: 0x4009e5 (<main+292>: call 0x4005c0 <printf@plt>)
R8 : 0x7fffffffdf11 --> 0x3f00007ffff7ff00
R9 : 0xa ('\n')
R10: 0x0
R11: 0xa ('\n')
R12: 0x400630 (<_start>: xor ebp,ebp)
R13: 0x7fffffffe570 --> 0x1
R14: 0x0
R15: 0x0
EFLAGS: 0x246 (carry PARITY adjust ZERO sign trap INTERRUPT direction overflow)
[-------------------------------------code-------------------------------------]
0x4009d8 <main+279>: mov rsi,rax
0x4009db <main+282>: mov edi,0x400d2c
0x4009e0 <main+287>: mov eax,0x0
=> 0x4009e5 <main+292>: call 0x4005c0 <printf@plt>
0x4009ea <main+297>: jmp 0x4009f6 <main+309>
0x4009ec <main+299>: mov edi,0x400d38
0x4009f1 <main+304>: call 0x4005a0 <puts@plt>
0x4009f6 <main+309>: mov eax,DWORD PTR [rip+0x201688] # 0x602084 <num2>
Guessed arguments:
arg[0]: 0x400d2c ("Flag: %s\n")
arg[1]: 0x7fffffffe460 --> 0x231819834c584545
[------------------------------------stack-------------------------------------]
0000| 0x7fffffffe450 --> 0x2
0008| 0x7fffffffe458 --> 0x7fffffffe460 --> 0x231819834c584545
0016| 0x7fffffffe460 --> 0x231819834c584545
0024| 0x7fffffffe468 --> 0x67035b26354e401c
0032| 0x7fffffffe470 (",q2H7?09:G>4!O]iJ('\nV")
0040| 0x7fffffffe478 (":G>4!O]iJ('\nV")
0048| 0x7fffffffe480 --> 0x560a27284a ("J('\nV")
0056| 0x7fffffffe488 --> 0x74941753df1a500
[------------------------------------------------------------------------------]
Legend: code, data, rodata, value
0x00000000004009e5 in main ()
gdb-peda$ x/s 0x7fffffffe460
0x7fffffffe460: "EEXL\203\031\030#\034@N5&[\003g,q2H7?09:G>4!O]iJ('\nV"
gdb-peda$ x/37x 0x7fffffffe460
0x7fffffffe460: 0x45 0x45 0x58 0x4c 0x83 0x19 0x18 0x23
0x7fffffffe468: 0x1c 0x40 0x4e 0x35 0x26 0x5b 0x03 0x67
0x7fffffffe470: 0x2c 0x71 0x32 0x48 0x37 0x3f 0x30 0x39
0x7fffffffe478: 0x3a 0x47 0x3e 0x34 0x21 0x4f 0x5d 0x69
0x7fffffffe480: 0x4a 0x28 0x27 0x0a 0x56
然后是一个有趣的函数 giff_flag，它在每次交谈是被调用，作用是修改 flag。
[0x00400630]> pdf @ sym.giff_flag
/ (fcn) sym.giff_flag 264
| sym.giff_flag ();
| ; var int local_1ch @ rbp-0x1c
| ; var int local_18h @ rbp-0x18
| ; var int local_4h @ rbp-0x4
| ; CALL XREF from 0x004009c3 (main)
| 0x004007b9 55 push rbp
| 0x004007ba 4889e5 mov rbp, rsp
| 0x004007bd 48897de8 mov qword [local_18h], rdi
| 0x004007c1 8975e4 mov dword [local_1ch], esi
| 0x004007c4 c745fc000000. mov dword [local_4h], 0
| ,=< 0x004007cb e9d6000000 jmp 0x4008a6
| | ; JMP XREF from 0x004008aa (sym.giff_flag)
| .--> 0x004007d0 8b05ae182000 mov eax, dword [obj.num2] ; eax = num2 ; num2 是交流次数，最大为 8
| :| 0x004007d6 99 cdq
| :| 0x004007d7 c1ea1f shr edx, 0x1f
| :| 0x004007da 01d0 add eax, edx
| :| 0x004007dc 83e001 and eax, 1 ; eax = eax & 1 = num2 % 2
| :| 0x004007df 29d0 sub eax, edx
| :| 0x004007e1 85c0 test eax, eax
| ,===< 0x004007e3 740a je 0x4007ef ; eax == 0 时跳转，即 num2 % 2 == 0
| |:| 0x004007e5 83f801 cmp eax, 1 ; 1
| ,====< 0x004007e8 745e je 0x400848 ; eax == 1 时跳转
| ,=====< 0x004007ea e9b3000000 jmp 0x4008a2
| |||:| ; JMP XREF from 0x004007e3 (sym.giff_flag) ; 情况一：num2 % 2 != 1
| ||`---> 0x004007ef 8b45fc mov eax, dword [local_4h] ; eax = i ; i 是循环计数
| || :| 0x004007f2 4863d0 movsxd rdx, eax ; rdx = eax = i
| || :| 0x004007f5 488b45e8 mov rax, qword [local_18h] ; rax = &flag
| || :| 0x004007f9 488d3402 lea rsi, [rdx + rax] ; rsi = &flag + i = &flag[i]
| || :| 0x004007fd 8b45fc mov eax, dword [local_4h] ; eax = i
| || :| 0x00400800 4863d0 movsxd rdx, eax ; rdx = eax = i
| || :| 0x00400803 488b45e8 mov rax, qword [local_18h] ; rax = &flag
| || :| 0x00400807 4801d0 add rax, rdx ; rax = &flag + i
| || :| 0x0040080a 0fb600 movzx eax, byte [rax] ; eax = flag[i]
| || :| 0x0040080d 89c7 mov edi, eax ; edi = eax = flag[i]
| || :| 0x0040080f 8b45e4 mov eax, dword [local_1ch] ; eax = key ; key 是交谈语句的序号
| || :| 0x00400812 0faf45fc imul eax, dword [local_4h] ; eax = eax * i = key * i
| || :| 0x00400816 89c1 mov ecx, eax ; ecx = eax = key * i
| || :| 0x00400818 baa7c867dd mov edx, 0xdd67c8a7
| || :| 0x0040081d 89c8 mov eax, ecx
| || :| 0x0040081f f7ea imul edx
| || :| 0x00400821 8d040a lea eax, [rdx + rcx]
| || :| 0x00400824 c1f805 sar eax, 5
| || :| 0x00400827 89c2 mov edx, eax
| || :| 0x00400829 89c8 mov eax, ecx
| || :| 0x0040082b c1f81f sar eax, 0x1f
| || :| 0x0040082e 29c2 sub edx, eax
| || :| 0x00400830 89d0 mov eax, edx
| || :| 0x00400832 c1e003 shl eax, 3
| || :| 0x00400835 01d0 add eax, edx
| || :| 0x00400837 c1e002 shl eax, 2
| || :| 0x0040083a 01d0 add eax, edx
| || :| 0x0040083c 29c1 sub ecx, eax
| || :| 0x0040083e 89ca mov edx, ecx ; edx = ecx = key * i
| || :| 0x00400840 89d0 mov eax, edx ; eax = edx = key * i
| || :| 0x00400842 01f8 add eax, edi ; eax = eax + edi = flag[i] + input * i
| || :| 0x00400844 8806 mov byte [rsi], al ; flag[i] = flag[i] + input * i
| ||,===< 0x00400846 eb5a jmp 0x4008a2
| |||:| ; JMP XREF from 0x004007e8 (sym.giff_flag) ; 情况二：num2 % 2 == 1
| |`----> 0x00400848 8b45fc mov eax, dword [local_4h] ; eax = i
| | |:| 0x0040084b 4863d0 movsxd rdx, eax ; rdx = eax = i
| | |:| 0x0040084e 488b45e8 mov rax, qword [local_18h] ; rax = &flag
| | |:| 0x00400852 488d3402 lea rsi, [rdx + rax] ; rsi = &flag + i = &flag[i]
| | |:| 0x00400856 8b45fc mov eax, dword [local_4h] ; eax = i
| | |:| 0x00400859 4863d0 movsxd rdx, eax ; rdx = eax = i
| | |:| 0x0040085c 488b45e8 mov rax, qword [local_18h] ; rax = &flag
| | |:| 0x00400860 4801d0 add rax, rdx ; rax = &flag + i
| | |:| 0x00400863 0fb600 movzx eax, byte [rax] ; eax = flag[i]
| | |:| 0x00400866 89c7 mov edi, eax ; edi = eax = flag[i]
| | |:| 0x00400868 8b45e4 mov eax, dword [local_1ch] ; eax = key
| | |:| 0x0040086b 0faf45fc imul eax, dword [local_4h] ; eax = eax * i = key * i
| | |:| 0x0040086f 89c1 mov ecx, eax ; ecx = eax = key * i
| | |:| 0x00400871 baa7c867dd mov edx, 0xdd67c8a7
| | |:| 0x00400876 89c8 mov eax, ecx
| | |:| 0x00400878 f7ea imul edx
| | |:| 0x0040087a 8d040a lea eax, [rdx + rcx]
| | |:| 0x0040087d c1f805 sar eax, 5
| | |:| 0x00400880 89c2 mov edx, eax
| | |:| 0x00400882 89c8 mov eax, ecx
| | |:| 0x00400884 c1f81f sar eax, 0x1f
| | |:| 0x00400887 29c2 sub edx, eax
| | |:| 0x00400889 89d0 mov eax, edx
| | |:| 0x0040088b c1e003 shl eax, 3
| | |:| 0x0040088e 01d0 add eax, edx
| | |:| 0x00400890 c1e002 shl eax, 2
| | |:| 0x00400893 01d0 add eax, edx
| | |:| 0x00400895 29c1 sub ecx, eax ; ecx = (key * i) % 37
| | |:| 0x00400897 89ca mov edx, ecx ; edx = ecx
| | |:| 0x00400899 89d0 mov eax, edx ; eax = edx = ecx
| | |:| 0x0040089b 29c7 sub edi, eax ; edi = edi - eax = flag[i] - key * i % 37
| | |:| 0x0040089d 89f8 mov eax, edi ; eax = edi
| | |:| 0x0040089f 8806 mov byte [rsi], al ; flag[i] = flag[i] - key * i % 37
| | |:| 0x004008a1 90 nop
| | |:| ; JMP XREF from 0x00400846 (sym.giff_flag)
| | |:| ; JMP XREF from 0x004007ea (sym.giff_flag)
| `-`---> 0x004008a2 8345fc01 add dword [local_4h], 1 ; i = i + 1
| :| ; JMP XREF from 0x004007cb (sym.giff_flag)
| :`-> 0x004008a6 837dfc24 cmp dword [local_4h], 0x24 ; [0x24:4]=-1 ; '$' ; 36
| `==< 0x004008aa 0f8e20ffffff jle 0x4007d0 ; i <= 36 时跳转
| 0x004008b0 8b05ce172000 mov eax, dword [obj.num2] ; [0x602084:4]=0
| 0x004008b6 83c001 add eax, 1
| 0x004008b9 8905c5172000 mov dword [obj.num2], eax ; [0x602084:4]=0
| 0x004008bf 5d pop rbp
\ 0x004008c0 c3 ret
该函数的汇编代码大概可以整理成下面的伪代码：
int num2 = 0; // 交谈次数
void giff_flag(&flag, int key) {
for(int i = 0; i <= 36; i++) {
if (num2 % 2 == 1) {
flag[i] = flag[i] - i * key % 37;
} else {
flag[i] = flag[i] + i * key % 37;
}
}
num2++;
}
我们知道 flag 的格式应该是 ECTF{...}，所以只要初始 flag 在多次转换后出现这几个字符，就很可能是最终的 flag 了。我们已经理清了算法，接下来的事情就交给 Z3 了。