From a2bfc392fd5f7171217960bb13ea2024c74f3d93 Mon Sep 17 00:00:00 2001 From: firmianay Date: Tue, 28 Nov 2017 17:12:21 +0800 Subject: [PATCH] finish 4.5; add 6.2.2 --- README.md | 1 + SUMMARY.md | 1 + doc/4.5_z3.md | 228 +++++++++++++++++++- doc/4.8_dynelf.md | 40 ++-- doc/6.2.1_re_xhpctf2017_dont_panic.md | 2 +- doc/6.2.2_re_ectf2016_tayy.md | 241 ++++++++++++++++++++++ doc/6_writeup.md | 1 + src/Others/4.5_z3/exp.py | 42 ++++ src/Others/4.5_z3/harder_serial.py | 72 +++++++ src/writeup/6.2.2_re_ectf2016_tayy/tayy | Bin 0 -> 13172 bytes src/writeup/6.2.2_re_ectf2016_tayy/tayy.c | 79 +++++++ 11 files changed, 682 insertions(+), 25 deletions(-) create mode 100644 doc/6.2.2_re_ectf2016_tayy.md create mode 100644 src/Others/4.5_z3/exp.py create mode 100644 src/Others/4.5_z3/harder_serial.py create mode 100755 src/writeup/6.2.2_re_ectf2016_tayy/tayy create mode 100644 src/writeup/6.2.2_re_ectf2016_tayy/tayy.c diff --git a/README.md b/README.md index e3b2e49..dc3e309 100644 --- a/README.md +++ b/README.md @@ -78,6 +78,7 @@ - [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md) - re - [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) - [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md) diff --git a/SUMMARY.md b/SUMMARY.md index 6907d96..ce4eca6 100644 --- a/SUMMARY.md +++ b/SUMMARY.md @@ -74,6 +74,7 @@ * [6.1.7 pwn 0CTF2015 freenote](doc/6.1.7_pwn_0ctf2015_freenote.md) * re * [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) * [7.1 更多 Linux 工具](doc/7.1_Linuxtools.md) * [7.2 更多 Windows 工具](doc/7.2_wintools.md) diff --git a/doc/4.5_z3.md b/doc/4.5_z3.md index f371fdc..f1e0fdc 100644 --- a/doc/4.5_z3.md +++ b/doc/4.5_z3.md @@ -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 函数和谓词符号 - 实数和整形运算(有限支持非线性运算) - 位向量 @@ -30,7 +30,7 @@ $ make $ sudo make install ``` -另外还可以使用 pip 来安装 Python 接口，这是二进制分析框架 angr 里内置的修改版： +另外还可以使用 pip 来安装 Python 接口（py2和py3均可），这是二进制分析框架 angr 里内置的修改版： ``` $ sudo pip install z3-solver ``` @@ -61,7 +61,7 @@ $ sudo pip install z3-solver >>> solve(x > 2, y < 10, x + 2*y == 7) [y = 0, x = 7] ``` -首先定义了两个变量 x 和 y，类型是 Z3 内置的整数类型 `Int`，`solve()` 函数会创造一个 solver，然后对括号中的约束条件进行求解，注意在 Z3 默认情况下只会找到满足条件的一组解。 +首先定义了两个常量 x 和 y，类型是 Z3 内置的整数类型 `Int`，`solve()` 函数会创造一个 solver，然后对括号中的约束条件进行求解，注意在 Z3 默认情况下只会找到满足条件的一组解。 ```python >>> simplify(x + y + 2*x + 3) @@ -73,8 +73,13 @@ And(x >= 2, 2*x**2 + y**2 >= 3) >>> >>> simplify((x + 1)*(y + 1)) (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 +>>> 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()` 获得。 @@ -169,7 +174,222 @@ x = 11 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 中的运用 +#### 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 远比这个强大，后面我们还会讲到它更高级的应用。 ## 参考资料 diff --git a/doc/4.8_dynelf.md b/doc/4.8_dynelf.md index 301edbb..0255b3b 100644 --- a/doc/4.8_dynelf.md +++ b/doc/4.8_dynelf.md @@ -117,26 +117,26 @@ gdb-peda$ pattern_offset 0x41384141 在 r2 中对程序进行分析，发现一个漏洞函数，地址为 `0x08048484`： ``` [0x080483d0]> pdf @ sub.setbuf_484 -/ (fcn) sub.setbuf_484 58 -| sub.setbuf_484 (); -| ; var int local_6ch @ ebp-0x6c -| ; var int local_4h @ esp+0x4 -| ; var int local_8h @ esp+0x8 -| ; CALL XREF from 0x0804855f (main) -| 0x08048484 55 push ebp -| 0x08048485 89e5 mov ebp, esp -| 0x08048487 81ec88000000 sub esp, 0x88 -| 0x0804848d a120a00408 mov eax, dword [obj.stdin] ; [0x804a020:4]=0 -| 0x08048492 8d5594 lea edx, [local_6ch] -| 0x08048495 89542404 mov dword [local_4h], edx -| 0x08048499 890424 mov dword [esp], eax -| 0x0804849c e8dffeffff call sym.imp.setbuf ; void setbuf(FILE *stream, -| 0x080484a1 c74424080001. mov dword [local_8h], 0x100 ; [0x100:4]=-1 ; 256 -| 0x080484a9 8d4594 lea eax, [local_6ch] -| 0x080484ac 89442404 mov dword [local_4h], eax -| 0x080484b0 c70424000000. mov dword [esp], 0 -| 0x080484b7 e8d4feffff call sym.imp.read ; ssize_t read(int fildes, void *buf, size_t nbyte) -| 0x080484bc c9 leave +/ (fcn) sub.setbuf_484 58 +| sub.setbuf_484 (); +| ; var int local_6ch @ ebp-0x6c +| ; var int local_4h @ esp+0x4 +| ; var int local_8h @ esp+0x8 +| ; CALL XREF from 0x0804855f (main) +| 0x08048484 55 push ebp +| 0x08048485 89e5 mov ebp, esp +| 0x08048487 81ec88000000 sub esp, 0x88 +| 0x0804848d a120a00408 mov eax, dword [obj.stdin] ; [0x804a020:4]=0 +| 0x08048492 8d5594 lea edx, [local_6ch] +| 0x08048495 89542404 mov dword [local_4h], edx +| 0x08048499 890424 mov dword [esp], eax +| 0x0804849c e8dffeffff call sym.imp.setbuf ; void setbuf(FILE *stream, +| 0x080484a1 c74424080001. mov dword [local_8h], 0x100 ; [0x100:4]=-1 ; 256 +| 0x080484a9 8d4594 lea eax, [local_6ch] +| 0x080484ac 89442404 mov dword [local_4h], eax +| 0x080484b0 c70424000000. mov dword [esp], 0 +| 0x080484b7 e8d4feffff call sym.imp.read ; ssize_t read(int fildes, void *buf, size_t nbyte) +| 0x080484bc c9 leave \ 0x080484bd c3 ret ``` 于是我们构造 leak 函数如下，即 `write(1, addr, 4)`： diff --git a/doc/6.2.1_re_xhpctf2017_dont_panic.md b/doc/6.2.1_re_xhpctf2017_dont_panic.md index 10bbe38..d79211c 100644 --- a/doc/6.2.1_re_xhpctf2017_dont_panic.md +++ b/doc/6.2.1_re_xhpctf2017_dont_panic.md @@ -1,4 +1,4 @@ -# 6.2.1 re xhpctf2017 dont_panic +# 6.2.1 re XHPCTF2017 dont_panic - [题目解析](#题目解析) - [参考资料](#参考资料) diff --git a/doc/6.2.2_re_ectf2016_tayy.md b/doc/6.2.2_re_ectf2016_tayy.md new file mode 100644 index 0000000..8409671 --- /dev/null +++ b/doc/6.2.2_re_ectf2016_tayy.md @@ -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�▒#@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. +> 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 (: call 0x4005c0 ) +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 : mov rsi,rax + 0x4009db : mov edi,0x400d2c + 0x4009e0 : mov eax,0x0 +=> 0x4009e5 : call 0x4005c0 + 0x4009ea : jmp 0x4009f6 + 0x4009ec : mov edi,0x400d38 + 0x4009f1 : call 0x4005a0 + 0x4009f6 : mov eax,DWORD PTR [rip+0x201688] # 0x602084 +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) 相应文件夹中。 + + +## 参考资料 diff --git a/doc/6_writeup.md b/doc/6_writeup.md index 6590c60..78c2800 100644 --- a/doc/6_writeup.md +++ b/doc/6_writeup.md @@ -10,3 +10,4 @@ - [6.1.7 pwn 0CTF2015 freenote](./6.1.7_pwn_0ctf2015_freenote.md) - re - [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) diff --git a/src/Others/4.5_z3/exp.py b/src/Others/4.5_z3/exp.py new file mode 100644 index 0000000..29d7f37 --- /dev/null +++ b/src/Others/4.5_z3/exp.py @@ -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)])) diff --git a/src/Others/4.5_z3/harder_serial.py b/src/Others/4.5_z3/harder_serial.py new file mode 100644 index 0000000..9ac174e --- /dev/null +++ b/src/Others/4.5_z3/harder_serial.py @@ -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") diff --git a/src/writeup/6.2.2_re_ectf2016_tayy/tayy b/src/writeup/6.2.2_re_ectf2016_tayy/tayy new file mode 100755 index 0000000000000000000000000000000000000000..95d055141a5e319c54d17101d6e8f32544a24b8d GIT binary patch literal 13172 zcmeHNZ)_aLb)UQAKcA!{&QPg)9;tjZ_Li7hXecT4i3 z``5cYNfh9Q#aXrvj8vg<3pw=%1^s9ALld-yA^Sr`T8gOzN=Cws)c{frhbn52+8ogZ>6&Pr)bjzYf}_i816^KKFhn1=VMdgCh!opf zEUIK}y1L#Li896ofOgo|hDU@5bU-jf)3P5YB_%r)(XK_>wMaXn)3RekX?!>~Ji^jn z*sFqsvWkTDit{2xT`UJbu%gJnvPOtNRlyKl&hC%E4*U6eOM_HAB->jqF7tAHM5V|c zi^m4Hbv_o4Zi&Z|xszK?c5U0Tty9USlnya&^pCoG4;&UPQ5+jV!tt$x1J?l7H~sA4 zzT3CPzH{Oi_kZoL-#Bvfs&s{iZ-d{oc>&xIzEQ5D1gRfc!4+GBOaF=EP zD)ndWGWhCca0c;?V0gE&Y{p1NnXbpOsmP8UdNyJthgdpiWtkOAm{5_mjL0!PGIC5G zGGcL-&cu?|5a8$nD>Ig!Fk(qSh7+lzM0B>dzpuMT?@+dvxXu#Sp=`yGd121H;)i?{ z93DV$o@hNi7>mKmtzr?0trN13C8V5tD0Uy(o&XukLeqetxOScEw~^a;E#T;%3U}c0 z(h^lI4%|n|K-(NRU1M0?<-nc$iR!?e{m~pa_KC_t2Ts>M);;6EVZf!LuZ;7}gH%DI^$l;&@vj3Jqu7V;p<7>cHAId)x@*$LQ=yMl^ybom@^4xhLccY9$of{MKPLy$ob7>)Wpo~MC8vwceH+_Zo zp4SS$((>IDH=Zxjn9tOkNBy{ZPyVWlN8vW=_?nLet^ZINs3B0h`VwZ903(rt^8AmvJb<)$Ct=RxB2#W-TDI zKSX}=?O_;T;o9$RzxPSu+T=o0>pO+%Lg@PV;p>Iz$r-O_x^=Q}4S~>g?SeMm`{QY? z@b2Zm1h=-w`@qXju81xbUYIT9ZcT;mVS95o;51(SkBywYI(fUvGo7FDv`)h!^XC^l z*7I}!jMbrgT4Y)q56x<4JG~CcGhP2CD@=`tZq@%VbPqcD_t%DhiJd%K<)2)rF1%Cf z>g0^iQ|jkW3)7y3Gc|X<<#6@;a@;yq0N3a9p?jYE3->nFpW`qSl?qS73#FNA65@+ee_x1 zuvR!&r@giLk2|#OyW4hX1+77Qd*|L=og1G#8iTsVDV6VQ`I>)dO5OA{yZk!De>Qoq zSiC%oTogFCj<-S|aCRPr+q6A9$FSmTXadpJ68g7*&RrK1FoCmCn_uu+NA4uR#q9^& zE?R6CSIb=t0y-YLdU_(~y|a7#@KqdH;f4ll>!VMLMZ57ZaCg2U#thAGE;WDSe*pJi z?gC);AAldPJ_D`h7wU4WFF%9eU!cNH=uLDV?9FqL4VU&~+dXgluYZsP{}?9t$J!K1rTyc#S71fpo-4Ol58QjOeB+B0f4jniqoX{YFjAX&*pRH^?@;(RQ#o#AOn%(V zjPgh(XT}x(;|kwzCd{m;h>s2_{!WGOO>yIdF}hLlZ&mmyDE@5R^BQVA1#ZjG3HC}-thl2Stu z(ak(+9yjBuv>D}tqx?W$kRLL$rjdz^*ps`FHD_6Kl;KE4ufX5IxM^ffZYC`=!wnuu zWin>O;;FP1OTj?J2ym)~P0NZUhk3>{;@pa5pbcmgW+}r5bMbg~1Y*YfP2;%9lc^IM z!4m%OZ16py0>zu~z26m!-v#>GLb3Q9&_Dn0V(|^2&2VA-9OxFf#y$r6KI{(b;9o&M z>;TUJT?ZHzPqbF#s+VRdcYc~5Nv;`mI}1^)0qF_p^tjBNr1)E|Lc-gaho1QQ&ov8>9@c0z`R8(neX2&;MAc{=Ysercl1%Rgsjw`M&P6W%@RA$!p8>q9_l#SnxX? zmPVVfFH1_qM+_ej9K8#;DRFuqLf?8Gl=y`zRd9rlNtyah?a?_FT;hm|F zDW3CE-Yn~7bN}arzGJ%^`a3zVZ%X>Eq&Fn}wWN0?t&!{H0ZAWqtsnBgAlJwIDpf#x zdwO>AmcxU&q?O~H$_}M-OGi#f?SInVskC(}?X5P>T&i75RUb!Hz!_7rqY29x1Zrh$ zIzk+L3^g-prX*9AsRXV)^c76ttaP`qw&jnehelgmIgc&Q&GOX4-)`?Jch=DlBQgNl1$)w|y^E-Gyt5 z+P~mch4KXnQ2*&0FkQz&2~G##z`ca*FL_mv;NzYI=7nT`yT-ATJze)t1BQDI+0*{@ zy4-;B(w>Mre$PV%?iFND`@?2A&~?&~`cHa9@$)k7JtWiqqe^>K+SdSe_Fuy66fmet z_O#!PNqZV6weKGPi!OWGKQBo8o3bIa$9sy~{v2S~FYF%{y5FQ_gLEIUYwf-gkF)@X z)Be2Nug**Ri>Tx%l*d5y6{vICQ(jb??9e~SagYnLBl-I-d%8c~k~b{6PmsRL9lI#) zDgN_*RjAHO`yWt+Ko{dDMfN%{*nd)^JR-_3>Lo=<-R-~WvcCym3$fgkH~da??kF^W z1Wf=FfI}|#(*FU}3hCR@qD=T5sBqddK47bIn@GtP;7oQzKL*Tc zKOpS~xNRbdEx?)V2>3)|G=5COz%s@KS)%V=KSfZ(_Seq#X=PGq^NCC zAx}5B&4_PFjta6P2xVIPgdrVhwIz->7bt%K$768N_-S9m>$6h(V{$+ryPUh*2lHhM zW=?f^)g|?qV->E5`tjgZOXGP~`eC&yaEs+tU_BM)+!5ctydb`0=Jd8{u8d<}a`&KK>+F9Y5HPv11})XF)bzx4Wj zWf}iJS_Z$m4E`U>;CBJX{`@sXksATQcvj+RIbWs>&@sRpV7|_{+Qs~IoL~C?N%1@(_1$sKOMT48#3FJkfSv)I zBj75p34Ip`;+ueD9NhljS;o)%!q3uu{#VQRXOWDRwQ`WL6@h%@eLaWt{=TQey3QaO z$Q+Jk;aOd`5_%+_N}5?#0n+toN*|7=293BLwNja^ZsblfcmPhvO~{Z^ws&mn0M8Ya zbbJ)IAFOqFSk8+AX4tMW24+Qu3^?;V6Mr3F+eQ*Dh-NAnS$vu0X3WfD>u)9Bm?nDxIB%2ex zXUSXwM%NeKuP??cyuSyd6*i!Q3||V^8QvmATvaK{8#B6xV?#sw5M(tm-4t&RY^UxF z@l2PU%ecH`B?0iD-9j$vMGH8^1z_`df$`K`)Dkw=dxy0B)FG* z63Oj4X2howx&>)tddAGAQ^_nQ!k1!&(S +#include +#include + +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. \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; +}