Question

章节 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
=============================================================

玩了一会儿我们发现：

1. 每次我们与 Tayy 交谈后，flag 就会变
2. 最多可以交谈 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 了。

参考资料