前段时间在忙各种事情，这两天有学弟学妹要入re，想带着他们打个新生赛，我就打算把这个比赛week1的题先出一遍，后面的之后再说。
这次0xGame的re题目名称都很有意思，开始做吧。
数字筑基
解法
直接搜索字符串
代码金丹
解法
就比第一题多个判断过程，不过flag仍然明文
网络元婴
解法
进去后明文，只不过分开了
为了方便就用x64dbg进去之后，在赋值结束后下断
然后进入内存地址
复制下来即可
虚拟化身
解法1
我特意把hint也截下来了，这也是信息之一，告诉我们重启之后验证。
所以我们这题的思路由逆向算法转为爆破程序。
可以看到这题相对于前面几题复杂了不少
不过不重要，我们现在的思路是爆破，直接找到判断的地方
地址151D，看看汇编
应该是删除了符号表了，没啥信息，没关系，看看字符串
也没有，应该是动态生成的，直接上X64dbg
跑出来了，点进去
根据字符串的信息很明显，第一个跳不能让他成功，成功的话就输出错误字符串，第二个让他成功，直接让他挂起
我们直接nop第一个跳
可以看到我们随便输入的东西导致即将导致第一个跳转，我们nop
跑
爆破成了
再次打开，就出现了flag
解法2
应该更加接近正确的做法把
strcmp的两个参数v15和v10，v15没有什么信息，v10有
两个word点进去
小端序存储的
a = bytes.fromhex('0000000000004B1B7E070E01084B234C085707196A55585309557F030C541D4E')
a += p32(0x50585475) + p32(0x2234E52) + p32(0x553045B)
key = b'0xGame'
xor(a,key)
#0xGame{c9fcd83d-e27a-4569-8ba1-62555b6dc6ac}
赛博天尊
解法
这题目我还是用心看了一下
已查无壳64位，扔进ida
长得还行（因为关键函数我重命名过，题目自带符号表被删了）
最主要的就是中间if的一大坨，根据这一大坨可以直接看出需要z3解，但我们还是进入程序的内部结构看看。
搜索字符串，只发现一个自带的0xGame的一个待格式化的一个字符串，所以关键信息仍然是动态生成的，我们x64dbg
找到了，点进去
这是我们要执行的代码
并且这个跳转不能成功，这样字符串就会被覆盖掉
同时这个
也不能跳成功，看一下有几个要这么跳
这些都是
在上面下断，然后一个个调ZF位
就可以爆破这个程序，但是这题不想上题，爆了也没用。
好好看一下，是什么决定这些跳转执不执行的
第一个，应该是不断读我们的字符串，然后比较我们输入的和0，然后根据未读到0的位置，不断自增rax，然后rax和2C比较。
第二个检查是否为}
后面的一坨lea，xx*4啥的就是刚刚ida里面看到的表达式了，有点恶心。
到这边知道看程序内部没啥用了
还是z3吧
from z3 import *
v7,v8,v9,v10,v11 = Ints('v7 v8 v9 v10 v11')
s = Solver()
s.add(7 * v9 + 5 * (v8 + v11) + 2 * (v10 + 4 * v7) == 0x12021DE669FC2)
v4 = v9 + v10 + 2 * v10 + 2 * (v11 + v7)
s.add(v8 + 3*v4 == 0x159BFFC17D045)
s.add(v10 + v9 + v11 + 2 * v9 + 2 * (v9 + v11 + 2 * v9) + 2 * (v8 + 4 * v7) == 0xACE320D12501)
s.add(v8 + 2 * (v7 + v11 + v9 + 2 * v10) == 0x733FFEB3A4FA)
s.add(v8 + 7 * v11 + 8 * (v9 + v10) + 5 * v7 == 0x1935EBA54EB28)
s.check()
d = s.model()
print(d)
v11 = 63356652901730
v9 = 16488
v7 = 2693650760
v8 = 14810
v10 = 41791
a='-'.join([hex(i)[2:] for i in [v7,v8,v9,v10,v11]])
print(a)
出了
关于z3的研究我这两天会出一篇flag