1.elf z3暴力破解·改

源代码如下

unsigned __int64 level1(void)
{
  char v1; // [rsp+Fh] [rbp-81h]
  int v2; // [rsp+10h] [rbp-80h]
  int i; // [rsp+14h] [rbp-7Ch]
  int j; // [rsp+18h] [rbp-78h]
  int k; // [rsp+1Ch] [rbp-74h]
  char s[104]; // [rsp+20h] [rbp-70h] BYREF
  unsigned __int64 v7; // [rsp+88h] [rbp-8h]

  v7 = __readfsqword(0x28u);
  puts("This is level1!");
  puts("show me your flag:");
  input_string(s);
  if ( strlen(s) != 40 )
    exit(-1);
  v1 = '\xAB';
  v2 = 0;
  for ( i = 0; i <= 39; ++i )//这个是加密过程 直接原样复制到z3求解器中即可
  {
    for ( j = 0; j <= 50; ++j )
    {
      v1 ^= j ^ v2 ^ 0x5F;
      s[i] ^= s[(i + 1) % 40];
      s[i] ^= v1;
      ++v2;
    }
  }
  for ( k = 0; k <= 39; ++k )
  {
    if ( s[k] != compare_data[k] )
    {
      puts("Ohhhh, TRY HARD");
      return __readfsqword(0x28u) ^ v7;
    }
  }
  puts("Yeah you win!");
  puts("Yeah you win!");
  puts("Yeah you win!");
  puts("Yeah you win!");
  return __readfsqword(0x28u) ^ v7;
}

可通过如下代码

"前面需要输入条件"
f=Solver()
print(f.model)

可以查找自己所输入的条件
通过对z3的检验发现自己出现了个python的低级常识性错误
for循环时range输出的可遍历对象实际是小于该对象的
如range(10)其应该是<10
所以经过对遍历对象的修改
真正的z3代码应该如下

from z3 import *    
DataCmp=[		
161, 186, 110, 70, 128, 244, 217, 170, 180, 54, 90,
   204, 140, 30, 149, 33, 143, 67, 225, 19, 138, 168, 106,
   66, 174, 251, 247, 165, 157, 11, 75, 222, 186, 0, 135,
   35, 144, 70, 211, 223]#加密逻辑中最后的校验数组
flag = [BitVec('flag[%2d]' % i, 8) for i in range(40)]  #设置8位位向量数组代表原来的flag,这种只是创建数组的快速方式 也可以用for循环创建数组
out=[0]*40#out代表
for i in range(40):
    out[i]=flag[i]#将out赋值为flag，因为flag是用于保存flag的状态，out用于进行加密变化
v1=0xab#添加初始条件
v2=0#添加初始条件
for i in range(40):#用out进行加密操作，如果用flag进行加密操作 则最后求解求的就不是flag，因为flag变量一直被赋值
    for j in range(51):
        v1=(v1^j^v2^0x5f)%256
        out[i]^=out[(i+1)%40]
        out[i]^=v1
        v2+=1
f = Solver()
for i in range(40):
    f.add(out[i]==DataCmp[i])#添加条件使变化中的out=校验数组中的值
while(f.check()==sat):#z3求解需要先进行check()否则不能直接获得解 sat代表有解 unsat代表没有解
    condition = []
    m = f.model()#获取解的字典(具体格式类似于{flag[0]:123,flag[1]:321})
    p=""
    for i in range(40):
        p+=chr(int("%s" % (m[flag[i]])))#用于访问flag字典(如果i=0则此时获取的是flag[0]的值)因为此处m[flag[i]]不是数字类型，是z3特有的类型，此处先转为"123"再转化为int 123最后转化为123对应的ascii字符
        condition.append(flag[i]!=int("%s" % (m[flag[i]])))#用于添加条件，让下一次结果跟现在的结果不同
    print(p)
    f.add(Or(condition))#用于添加条件，让下一次结果跟现在的结果不同

此处也可用暴力破解因为在for j in range(51)循环内前一个字符只跟后一个字符有关如果了解了flag前三个字符是SYC也是可以直接破解的