nganhkhoa/CTF-All-In-One
1
0
Fork 0
mirror of https://github.com/nganhkhoa/CTF-All-In-One.git synced 2024-12-25 11:41:16 +07:00
Code Issues Projects Releases Wiki Activity

finish 4.5; add 6.2.2

Browse Source
This commit is contained in:
firmianay 2017-11-28 17:12:21 +08:00
parent 1874b59e20
commit a2bfc392fd
11 changed files with 682 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
README.md
View File

@ -78,6 +78,7 @@
- [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md) - [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md)
- re - re
- [6.2.1 re XHPCTF2017 dont_panic](doc/6.2.1_re_xhpctf2017_dont_panic.md) - [6.2.1 re XHPCTF2017 dont_panic](doc/6.2.1_re_xhpctf2017_dont_panic.md)
- [6.2.2 re ECTF2016 tayy](doc/6.2.2_re_ectf2016_tayy.md)
- [七、附录](doc/7_appendix.md) - [七、附录](doc/7_appendix.md)
- [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md) - [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md)

1
SUMMARY.md
View File

@ -74,6 +74,7 @@
* [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md) * [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md)
* re * re
* [6.2.1 re XHPCTF2017 dont_panic](doc/6.2.1_re_xhpctf2017_dont_panic.md) * [6.2.1 re XHPCTF2017 dont_panic](doc/6.2.1_re_xhpctf2017_dont_panic.md)
* [6.2.2 re ECTF2016 tayy](doc/6.2.2_re_ectf2016_tayy.md)
* [七、附录](doc/7_appendix.md) * [七、附录](doc/7_appendix.md)
* [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md) * [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md)
* [7.2 更多 Windows 工具](doc/7.2_wintools.md) * [7.2 更多 Windows 工具](doc/7.2_wintools.md)

228
doc/4.5_z3.md
View File

@ -7,7 +7,7 @@
- [参考资料](#参考资料) - [参考资料](#参考资料)
[Z3](https://github.com/Z3Prover/z3) 是一个由微软开发的 Satisfiability Modulo Theories（SMT）求解器。可以用来检查满足一个或多个理论的公式的可满足性，也就是说,它可以自动化地通过内置理论对一阶逻辑多种排列进行可满足性校验。目前其支持的理论有： [Z3](https://github.com/Z3Prover/z3) 是一个由微软开发的可满足性摸理论（Satisfiability Modulo Theories，SMT）的约束求解器。所谓约束求解器就是用户使用某种特定的语言描述对象（变量）的约束条件，求解器将试图求解出能够满足所有约束条件的每个变量的值。Z3 可以用来检查满足一个或多个理论的公式的可满足性，也就是说,它可以自动化地通过内置理论对一阶逻辑多种排列进行可满足性校验。目前其支持的理论有：
- equality over free 函数和谓词符号 - equality over free 函数和谓词符号
- 实数和整形运算(有限支持非线性运算) - 实数和整形运算(有限支持非线性运算)
- 位向量 - 位向量
@ -30,7 +30,7 @@ $ make
$ sudo make install $ sudo make install
``` ```
另外还可以使用 pip 来安装 Python 接口，这是二进制分析框架 angr 里内置的修改版： 另外还可以使用 pip 来安装 Python 接口（py2和py3均可），这是二进制分析框架 angr 里内置的修改版：
``` ```
$ sudo pip install z3-solver $ sudo pip install z3-solver
``` ```
@ -61,7 +61,7 @@ $ sudo pip install z3-solver
>>> solve(x > 2, y < 10, x + 2*y == 7) >>> solve(x > 2, y < 10, x + 2*y == 7)
[y = 0, x = 7] [y = 0, x = 7]
``` ```
首先定义了两个变量 x 和 y，类型是 Z3 内置的整数类型 `Int`，`solve()` 函数会创造一个 solver，然后对括号中的约束条件进行求解，注意在 Z3 默认情况下只会找到满足条件的一组解。 首先定义了两个常量 x 和 y，类型是 Z3 内置的整数类型 `Int`，`solve()` 函数会创造一个 solver，然后对括号中的约束条件进行求解，注意在 Z3 默认情况下只会找到满足条件的一组解。
```python ```python
>>> simplify(x + y + 2*x + 3) >>> simplify(x + y + 2*x + 3)
@ -73,8 +73,13 @@ And(x >= 2, 2*x**2 + y**2 >= 3)
>>> >>>
>>> simplify((x + 1)*(y + 1)) >>> simplify((x + 1)*(y + 1))
(1 + x)*(1 + y) (1 + x)*(1 + y)
>>> simplify((x + 1)*(y + 1), som=True) >>> simplify((x + 1)*(y + 1), som=True) # sum-of-monomials：单项式的和
1 + x + y + x*y 1 + x + y + x*y
>>> t = simplify((x + y)**3, som=True)
>>> t
x*x*x + 3*x*x*y + 3*x*y*y + y*y*y
>>> simplify(t, mul_to_power=True) # mul_to_power 将乘法转换成乘方
x**3 + 2*y*x**2 + x**2*y + 3*x*y**2 + y**3
``` ```
`simplify()` 函数用于对表达式进行化简，同时可以设置一些选项来满足不同的要求。更多选项使用 `help_simplify()` 获得。 `simplify()` 函数用于对表达式进行化简，同时可以设置一些选项来满足不同的要求。更多选项使用 `help_simplify()` 获得。
@ -169,7 +174,222 @@ x = 11
y = 13 y = 13
``` ```
为了将 Z3 中的数和 Python 区分开，应该使用 `IntVal()`、`RealVal()` 和 `RatVal()` 分别返回 Z3 整数、实数和有理数值。
```python
>>> 1/3
0.3333333333333333
>>> RealVal(1)/3
1/3
>>> Q(1, 3) # Q(a, b) 返回有理数 a/b
1/3
>>>
>>> x = Real('x')
>>> x + 1/3
x + 3333333333333333/10000000000000000
>>> x + Q(1, 3)
x + 1/3
>>> x + "1/3"
x + 1/3
>>> x + 0.25
x + 1/4
>>> solve(3*x == 1)
[x = 1/3]
>>> set_param(rational_to_decimal=True) # 以十进制形式表示有理数
>>> solve(3*x == 1)
[x = 0.3333333333?]
```
在混合使用实数和整数变量时，Z3Py 会自动添加强制类型转换将整数表达式转换成实数表达式。
```python
>>> x = Real('x')
>>> y = Int('y')
>>> a, b, c = Reals('a b c') # 返回一个实数常量元组
>>> s, r = Ints('s r') # 返回一个整数常量元组
>>> x + y + 1 + a + s
x + ToReal(y) + 1 + a + ToReal(s) # ToReal() 将整数表达式转换成实数表达式
>>> ToReal(y) + c
ToReal(y) + c
```
现代的CPU使用固定大小的位向量进行算术运算，在 Z3 中，使用函数 `BitVec()` 创建位向量常量，`BitVecVal()` 返回给定位数的位向量值。
```python
>>> x = BitVec('x', 16) # 16 位，命名为 x
>>> y = BitVec('x', 16)
>>> x + 2
x + 2
>>> (x + 2).sexpr() # .sexpr() 返回内部表现形式
'(bvadd x #x0002)'
>>> simplify(x + y - 1) # 16 位整数的 -1 等于 65535
65535 + 2*x
>>> a = BitVecVal(-1, 16) # 16 位，值为 -1
>>> a
65535
>>> b = BitVecVal(65535, 16)
>>> b
65535
>>> simplify(a == b)
True
```
## Z3 在 CTF 中的运用 ## Z3 在 CTF 中的运用
#### re PicoCTF2013 Harder_Serial
题目如下，是一段 Python 代码，要求输入一段 20 个数字构成的序列号，然后程序会对序列号的每一位进行验证，以满足各种要求。题目难度不大，但完全手工验证是一件麻烦的事，而使用 Z3 的话，只要定义好这些条件，就可以得出满足条件的值。
```python
import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
print ("Usage: %s [serial number]"%sys.argv[0])
exit()
print ("#>" + sys.argv[1] + "<#")
def check_serial(serial):
if (not set(serial).issubset(set(map(str,range(10))))):
print ("only numbers allowed")
return False
if len(serial) != 20:
return False
if int(serial[15]) + int(serial[4]) != 10:
return False
if int(serial[1]) * int(serial[18]) != 2:
return False
if int(serial[15]) / int(serial[9]) != 1:
return False
if int(serial[17]) - int(serial[0]) != 4:
return False
if int(serial[5]) - int(serial[17]) != -1:
return False
if int(serial[15]) - int(serial[1]) != 5:
return False
if int(serial[1]) * int(serial[10]) != 18:
return False
if int(serial[8]) + int(serial[13]) != 14:
return False
if int(serial[18]) * int(serial[8]) != 5:
return False
if int(serial[4]) * int(serial[11]) != 0:
return False
if int(serial[8]) + int(serial[9]) != 12:
return False
if int(serial[12]) - int(serial[19]) != 1:
return False
if int(serial[9]) % int(serial[17]) != 7:
return False
if int(serial[14]) * int(serial[16]) != 40:
return False
if int(serial[7]) - int(serial[4]) != 1:
return False
if int(serial[6]) + int(serial[0]) != 6:
return False
if int(serial[2]) - int(serial[16]) != 0:
return False
if int(serial[4]) - int(serial[6]) != 1:
return False
if int(serial[0]) % int(serial[5]) != 4:
return False
if int(serial[5]) * int(serial[11]) != 0:
return False
if int(serial[10]) % int(serial[15]) != 2:
return False
if int(serial[11]) / int(serial[3]) != 0:
return False
if int(serial[14]) - int(serial[13]) != -4:
return False
if int(serial[18]) + int(serial[19]) != 3:
return False
return True
if check_serial(sys.argv[1]):
print ("Thank you! Your product has been verified!")
else:
print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")
```
首先创建一个求解器实例，然后将序列的每个数字定义为常量：
```python
serial = [Int("serial[%d]" % i) for i in range(20)]
```
接着定义约束条件，注意，除了题目代码里的条件外，还有一些隐藏的条件，比如这一句：
```python
solver.add(serial[11] / serial[3] == 0)
```
因为被除数不能为 0，所以 `serial[3]` 不能为 0。另外，每个序列号数字都是大于等于 0，小于 9 的。最后求解得到结果。
完整的 exp 如下，其他文件在 [github](../src/Others/4.5_z3) 相应文件夹中。
```python
from z3 import *
solver = Solver()
serial = [Int("serial[%d]" % i) for i in range(20)]
solver.add(serial[15] + serial[4] == 10)
solver.add(serial[1] * serial[18] == 2 )
solver.add(serial[15] / serial[9] == 1)
solver.add(serial[17] - serial[0] == 4)
solver.add(serial[5] - serial[17] == -1)
solver.add(serial[15] - serial[1] == 5)
solver.add(serial[1] * serial[10] == 18)
solver.add(serial[8] + serial[13] == 14)
solver.add(serial[18] * serial[8] == 5)
solver.add(serial[4] * serial[11] == 0)
solver.add(serial[8] + serial[9] == 12)
solver.add(serial[12] - serial[19] == 1)
solver.add(serial[9] % serial[17] == 7)
solver.add(serial[14] * serial[16] == 40)
solver.add(serial[7] - serial[4] == 1)
solver.add(serial[6] + serial[0] == 6)
solver.add(serial[2] - serial[16] == 0)
solver.add(serial[4] - serial[6] == 1)
solver.add(serial[0] % serial[5] == 4)
solver.add(serial[5] * serial[11] == 0)
solver.add(serial[10] % serial[15] == 2)
solver.add(serial[11] / serial[3] == 0) # serial[3] can't be 0
solver.add(serial[14] - serial[13] == -4)
solver.add(serial[18] + serial[19] == 3)
for i in range(20):
solver.add(serial[i] >= 0, serial[i] < 10)
solver.add(serial[3] != 0)
if solver.check() == sat:
m = solver.model()
for d in m.decls():
print("%s = %s" % (d.name(), m[d]))
print("".join([str(m.eval(serial[i])) for i in range(20)]))
```
Bingo!!!
```
$ python exp.py
serial[2] = 8
serial[11] = 0
serial[3] = 9
serial[4] = 3
serial[1] = 2
serial[0] = 4
serial[19] = 2
serial[14] = 5
serial[17] = 8
serial[16] = 8
serial[10] = 9
serial[8] = 5
serial[6] = 2
serial[9] = 7
serial[5] = 7
serial[13] = 9
serial[7] = 4
serial[18] = 1
serial[15] = 7
serial[12] = 3
42893724579039578812
$ python harder_serial.py 42893724579039578812
Please enter a valid serial number from your RoboCorpIntergalactic purchase
#>42893724579039578812<#
Thank you! Your product has been verified!
```
这一题简直是为 Z3 量身定做的，方法也很简单，但 Z3 远比这个强大，后面我们还会讲到它更高级的应用。
## 参考资料 ## 参考资料

2
doc/6.2.1_re_xhpctf2017_dont_panic.md
View File

@ -1,4 +1,4 @@
# 6.2.1 re xhpctf2017 dont_panic # 6.2.1 re XHPCTF2017 dont_panic
- [题目解析](#题目解析) - [题目解析](#题目解析)
- [参考资料](#参考资料) - [参考资料](#参考资料)

241
doc/6.2.2_re_ectf2016_tayy.md Normal file
View File

@ -0,0 +1,241 @@
# 6.2.2 re ECTF2016 tayy
- [题目解析](#题目解析)
- [参考资料](#参考资料)
章节 4.5 中讲解了 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<58>▒#@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<5A>*$IX@2hv<<EFBFBD>D[KTFPR`XO=l{<7B>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 ; k <= 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
```
该函数的汇编代码大概可以整理成下面的伪代码：
```C
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 了。
完整的 exp 如下，其他文件在 [github](../src/writeup/6.2.2_re_ectf2016_tayy) 相应文件夹中。
## 参考资料

1
doc/6_writeup.md
View File

@ -10,3 +10,4 @@
- [6.1.7 pwn 0CTF2015 freenote](./6.1.7_pwn_0ctf2015_freenote.md) - [6.1.7 pwn 0CTF2015 freenote](./6.1.7_pwn_0ctf2015_freenote.md)
- re - re
- [6.2.1 re XHPCTF2017 dont_panic](./6.2.1_re_xhpctf2017_dont_panic.md) - [6.2.1 re XHPCTF2017 dont_panic](./6.2.1_re_xhpctf2017_dont_panic.md)
- [6.2.2 re ECTF2016 tayy](./6.2.2_re_ectf2016_tayy.md)

42
src/Others/4.5_z3/exp.py Normal file
View File

@ -0,0 +1,42 @@
from z3 import *
solver = Solver()
serial = [Int("serial[%d]" % i) for i in range(20)]
solver.add(serial[15] + serial[4] == 10)
solver.add(serial[1] * serial[18] == 2 )
solver.add(serial[15] / serial[9] == 1)
solver.add(serial[17] - serial[0] == 4)
solver.add(serial[5] - serial[17] == -1)
solver.add(serial[15] - serial[1] == 5)
solver.add(serial[1] * serial[10] == 18)
solver.add(serial[8] + serial[13] == 14)
solver.add(serial[18] * serial[8] == 5)
solver.add(serial[4] * serial[11] == 0)
solver.add(serial[8] + serial[9] == 12)
solver.add(serial[12] - serial[19] == 1)
solver.add(serial[9] % serial[17] == 7)
solver.add(serial[14] * serial[16] == 40)
solver.add(serial[7] - serial[4] == 1)
solver.add(serial[6] + serial[0] == 6)
solver.add(serial[2] - serial[16] == 0)
solver.add(serial[4] - serial[6] == 1)
solver.add(serial[0] % serial[5] == 4)
solver.add(serial[5] * serial[11] == 0)
solver.add(serial[10] % serial[15] == 2)
solver.add(serial[11] / serial[3] == 0) # serial[3] can't be 0
solver.add(serial[14] - serial[13] == -4)
solver.add(serial[18] + serial[19] == 3)
for i in range(20):
solver.add(serial[i] >= 0, serial[i] < 10)
solver.add(serial[3] != 0)
if solver.check() == sat:
m = solver.model()
for d in m.decls():
print("%s = %s" % (d.name(), m[d]))
print("".join([str(m.eval(serial[i])) for i in range(20)]))

72
src/Others/4.5_z3/harder_serial.py Normal file
View File

@ -0,0 +1,72 @@
#!/usr/bin/env python
# Looks like the serial number verification for space ships is similar to that
# of your robot. Try to find a serial that verifies for this space ship
import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
print ("Usage: %s [serial number]"%sys.argv[0])
exit()
print ("#>" + sys.argv[1] + "<#")
def check_serial(serial):
if (not set(serial).issubset(set(map(str,range(10))))):
print ("only numbers allowed")
return False
if len(serial) != 20:
return False
if int(serial[15]) + int(serial[4]) != 10:
return False
if int(serial[1]) * int(serial[18]) != 2:
return False
if int(serial[15]) / int(serial[9]) != 1:
return False
if int(serial[17]) - int(serial[0]) != 4:
return False
if int(serial[5]) - int(serial[17]) != -1:
return False
if int(serial[15]) - int(serial[1]) != 5:
return False
if int(serial[1]) * int(serial[10]) != 18:
return False
if int(serial[8]) + int(serial[13]) != 14:
return False
if int(serial[18]) * int(serial[8]) != 5:
return False
if int(serial[4]) * int(serial[11]) != 0:
return False
if int(serial[8]) + int(serial[9]) != 12:
return False
if int(serial[12]) - int(serial[19]) != 1:
return False
if int(serial[9]) % int(serial[17]) != 7:
return False
if int(serial[14]) * int(serial[16]) != 40:
return False
if int(serial[7]) - int(serial[4]) != 1:
return False
if int(serial[6]) + int(serial[0]) != 6:
return False
if int(serial[2]) - int(serial[16]) != 0:
return False
if int(serial[4]) - int(serial[6]) != 1:
return False
if int(serial[0]) % int(serial[5]) != 4:
return False
if int(serial[5]) * int(serial[11]) != 0:
return False
if int(serial[10]) % int(serial[15]) != 2:
return False
if int(serial[11]) / int(serial[3]) != 0:
return False
if int(serial[14]) - int(serial[13]) != -4:
return False
if int(serial[18]) + int(serial[19]) != 3:
return False
return True
if check_serial(sys.argv[1]):
print ("Thank you! Your product has been verified!")
else:
print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")

BIN
src/writeup/6.2.2_re_ectf2016_tayy/tayy Executable file
View File

Binary file not shown.

79
src/writeup/6.2.2_re_ectf2016_tayy/tayy.c Normal file
View File

@ -0,0 +1,79 @@
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
int num2 = 0;
static char *option2 =
"=============================================================\n1. Ayy lmao, Tayy lmao.\n2. You are very cruel.\n3. Memes are lyf.\n4. Go away!.\n5. zzzz\n6. Cats > Dogs.\n7. Dogs > Cats.\n8. AI is overrated?.\n9. I dont like you.\n0. <exit to menu>\n> ";
static char *option1 =
"=============================================================\n1. Talk to Tayy.\n2. Flag?\n0. Exit.\n> ";
void print_random_tayy_response() {
const char *a[5];
a[0] = "Die, human!";
a[1] = "You are mean.";
a[2] = "I disagree.";
a[3] = "I agree.";
a[4] = "I dont understand.";
srand(time(NULL));
int r = rand()%5;
printf("Tayy: %s\n\n", a[r]);
}
void giff_flag (char *flg, int num1) {
// ASCII printable range 48-125
int i;
for (i=0;i<37;i++) {
switch (num2%2) {
case 0: flg[i] = (char) ((int)flg[i] + (num1*i)%37);
break;
case 1: flg[i] = (char) ((int)flg[i] - (num1*i)%37);
break;
}
}
num2++;
}
int main() {
// printf("========================");
// printf("Welcome to the chat-bot");
// ECTF{41_1S_D3f1n1t3lY_N0T_TH3_FuTUR3}
// 5146183
char buff[37];
char *flag = buff;
strcpy(flag, "EEXL\x83\x19\x18#\x1C@N5&[\x03g,q2H7?09:G>4!O]iJ('\nV");
int opt1, opt2;
printf("=============================================================\n");
printf("Welcome to the future of AI, developed by NIA Research, Tayy!\n");
printf("%s", option1);
scanf("%d", &opt1);
while(opt1!=0) {
switch(opt1) {
case 1: printf("%s", option2);
scanf("%d", &opt2);
if (opt2 == 0)
break;
giff_flag(flag, opt2);
print_random_tayy_response();
break;
case 2: printf("Flag: %s\n", flag);
break;
default: printf("Please enter a correct option.\n");
}
if (num2 == 8) {
printf("Tayy is getting real tired of your bullshit. Leave now!.\n");
break;
}
printf("%s", option1);
scanf("%d", &opt1);
}
return 0;
}