记录一次菜的抠脚的学习过程
题目是一个bin文件，首先通过file命令看一下文件格式
$ file blend/main.bin
blend/main.bin: DOS/MBR boot sector
拖到IDA Pro 可以识别其中的汇编，但需要快捷键p创建函数才可以使用空格，静态可能看不太明白，因为它和我们常见的程序不太一样，函数调用都是通过软件断点形式实现，动态调一下就会明白程序流程。
程序的调试可以使用qemu
$ qemu-system-i386 -s -drive format=raw,file=./main.bin
程序就可以执行起来，可以通过gdb进行调试，程序默认加载地址为0x7c00，所以下端点的时候地址为偏移地址+0x7c00。由于是16为汇编所以gdb的插件可能会有bug，只是pwndbg是这样，建议使用原生gdb，gdb调试流程如下
$ gdb
GNU gdb (Ubuntu 7.11.1-0ubuntu1~16.5) 7.11.1
Copyright (C) 2016 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law. Type "show copying"
and "show warranty" for details.
This GDB was configured as "x86_64-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<http://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
<http://www.gnu.org/software/gdb/documentation/>.
For help, type "help".
Type "apropos word" to search for commands related to "word".
(gdb) set architecture i8086
warning: A handler for the OS ABI "GNU/Linux" is not built into this configuration
of GDB. Attempting to continue with the default i8086 settings.
The target architecture is assumed to be i8086
(gdb) set disassembly-flavor intel
(gdb) target remote:1234
注意要执行这句set architecture i8086，否则汇编也会出错。其他就没什么区别了，正常调试即可。通过调试可知其实程序一直会在一个循环里运行，默认走绿色分支。
当输入够20个字符会进入红色的分支，输入保存在0x1234处，这一分支也就是对输入flag进行验证的地方，也是需要我们重点关注的部分。程序首先会对前4字节进行判断，静态可知前4字节为flag。紧接着对0x1238处的输入进行验证，汇编为SSE浮点汇编，没接触过的可能有些难度，多用Google搜索，看几个例子相信你对每句汇编就理解了。程序首先会对你的输入进行一个乱序处理，实现这一操作的是pshufd指令，如果可以动态调试其实可以不用理细节，可以直接看执行完的xmm0寄存器。紧接着和内存中的数进行相与
0xffffffffffffff00 0xffffffffffffff00
0xffffffffffff00ff 0xffffffffffff00ff
0xffffffffff00ffff 0xffffffffff00ffff
0xffffffff00ffffff 0xffffffff00ffffff
0xffffff00ffffffff 0xffffff00ffffffff
0xffff00ffffffffff 0xffff00ffffffffff
0xff00ffffffffffff 0xff00ffffffffffff
0x00ffffffffffffff 0x00ffffffffffffff
写出来应该可以看明白相与之后的结果了吧。相与之后与xmm5做一个绝对差求和的运算，将最终的结果与程序的数据进行比较
0x03110304
0x02d902cd
0x02d402db
0x02c402e2
0x02ce02e2
0x02d802ed
0x02dc02e8
0x02dd02f6
注意这三句汇编其实它的效果是进行了一次高低位交换
image.png
如果相等继续下次循环，一共要循环8次，每次循环xmm0不变，变得只有xmm5，xmm5其实就是上一次循环的结果。所以整个算法逻辑就是这样，如果可以动态调试是很好理解的，最初没找到合适的调试方法，静态看有点吃力。
要解整个题很难逆推回去，因为算法不是一个可逆算法。所以自然想到暴力破解，当然暴力破解也有技巧，可以借助z3，可以提高效率。直接上最后的python脚本(python3执行)
from z3 import *
s = Solver()
a = Int('a')
b = Int('b')
c = Int('c')
d = Int('d')
e = Int('e')
f = Int('f')
g = Int('g')
h = Int('h')
i = Int('i')
j = Int('j')
k = Int('k')
l = Int('l')
m = Int('m')
n = Int('n')
o = Int('o')
p = Int('p')
s.add(a < 127)
s.add(b < 127)
s.add(c < 127)
s.add(d < 127)
s.add(e < 127)
s.add(f < 127)
s.add(g < 127)
s.add(h < 127)
s.add(i < 127)
s.add(j < 127)
s.add(k < 127)
s.add(l < 127)
s.add(m < 127)
s.add(n < 127)
s.add(o < 127)
s.add(p < 127)
s.add(a > 32)
s.add(b > 32)
s.add(c > 32)
s.add(d > 32)
s.add(e > 32)
s.add(f > 32)
s.add(g > 32)
s.add(h > 32)
s.add(i > 32)
s.add(j > 32)
s.add(k > 32)
s.add(l > 32)
s.add(m > 32)
s.add(n > 32)
s.add(o > 32)
s.add(p > 32)
def abs(x):
return If(x >= 0,x,-x)
s.add(abs(d-0x22)+abs(c-0xf)+abs(b-0x2)+abs(a-0xc8)+abs(h-0x83)+abs(g-0xfb)+abs(f-0xe0)+abs(0-0x83) ==0x304)
s.add(abs(p-0xc0)+abs(o-0x20)+abs(n-0xf)+abs(m-0x10)+abs(l-0xcd)+abs(k-0x00)+abs(j-0x13)+abs(0-0xb8) ==0x311)
s.add(abs(d-0x0)+abs(c-0x0)+abs(b-0x0)+abs(a-0x0)+abs(h-0x0)+abs(g-0x0)+abs(0-0x3)+abs(e-0x4) ==0x2cd)
s.add(abs(p-0x0)+abs(o-0x0)+abs(n-0x00)+abs(m-0x0)+abs(l-0x0)+abs(k-0x00)+abs(0-0x3)+abs(i-0x11) ==0x2d9)
s.add(abs(d-0x0)+abs(c-0x0)+abs(b-0x0)+abs(a-0x0)+abs(h-0x0)+abs(0-0x0)+abs(f-0x2)+abs(e-0xcd) ==0x2db)
s.add(abs(p-0x0)+abs(o-0x0)+abs(n-0x0)+abs(m-0x0)+abs(l-0x0)+abs(0-0x00)+abs(j-0x2)+abs(i-0xd9) ==0x2d4)
s.add(abs(d-0x0)+abs(c-0x0)+abs(b-0x0)+abs(a-0x0)+abs(0-0x0)+abs(g-0x0)+abs(f-0x2)+abs(e-0xdb) ==0x2e2)
s.add(abs(p-0x0)+abs(o-0x0)+abs(n-0x0)+abs(m-0x0)+abs(0-0x0)+abs(k-0x00)+abs(j-0x2)+abs(i-0xd4) ==0x2c4)
s.add(abs(d-0x0)+abs(c-0x0)+abs(b-0x0)+abs(0-0x0)+abs(h-0x0)+abs(g-0x0)+abs(f-0x2)+abs(e-0xe2) ==0x2e2)
s.add(abs(p-0x0)+abs(o-0x0)+abs(n-0x0)+abs(0-0x0)+abs(l-0x0)+abs(k-0x00)+abs(j-0x2)+abs(i-0xc4) ==0x2ce)
s.add(abs(d-0x0)+abs(c-0x0)+abs(0-0x0)+abs(a-0x0)+abs(h-0x0)+abs(g-0x0)+abs(f-0x2)+abs(e-0xe2) ==0x2ed)
s.add(abs(p-0x0)+abs(o-0x0)+abs(0-0x0)+abs(m-0x0)+abs(l-0x0)+abs(k-0x00)+abs(j-0x2)+abs(i-0xce) ==0x2d8)
s.add(abs(d-0x0)+abs(0-0x0)+abs(b-0x0)+abs(a-0x0)+abs(h-0x0)+abs(g-0x0)+abs(f-0x2)+abs(e-0xed) ==0x2e8)
s.add(abs(p-0x0)+abs(0-0x0)+abs(n-0x0)+abs(m-0x0)+abs(l-0x0)+abs(k-0x00)+abs(j-0x2)+abs(i-0xd8) ==0x2dc)
s.add(abs(0-0x0)+abs(c-0x0)+abs(b-0x0)+abs(a-0x0)+abs(h-0x0)+abs(g-0x0)+abs(f-0x2)+abs(e-0xe8) ==0x2f6)
s.add(abs(0-0x0)+abs(o-0x0)+abs(n-0x0)+abs(m-0x0)+abs(l-0x0)+abs(k-0x00)+abs(j-0x2)+abs(i-0xdc) ==0x2dd)
if s.check() == sat:
model = s.model()
answer = [model[a],model[b],model[c],model[d],model[e],model[f],model[g],model[h], model[i],model[j],model[k],model[l],model[m],model[n],model[o],model[p],0]
flag = ""
answer_str = ""
for i in range(len(answer)-1):
answer_str += chr(int(str(answer[i])))
print(answer_str)
else:
print('unsat')
