python模块Z3

December 7, 2018 Python学习 访问: 52 次

python-Z3模块

在最近的比赛中,看别人在CTF中经常用到这个模块,感觉功能还挺强大的!

简介

Z3 是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题,CTF 领域来说,能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外,著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

基本操作

在Z3中,内置了多种变量类型,包括整型(Int)、浮点型、char(BitVec)、数组(array)等等。

from z3 import *            #导入z3模块
x = Int('x')
y = Int('y')                #定义了两个变量
solve(x>2,y<10,x+2y==7)     #求解

这里定义的变量位Int型,但是并不是C/C++ 里面包含上下界的 int,Z3 中的 Int 对应的就是数学中的整数,Z3 中的 BitVector 才对应到 C/C++ 中的 int。运行代码输出:

[y = 0, x = 7]

z3默认只输出一组解,并不是将所有的解都输出来。
创建一个求解器:

solver = Solver()

想求解器中添加条件:

solver.add()

检测解的情况,有解的时候会回显sat,无解的时候会回显unsat

check()

在存在解的时候,该函数会将每个限制条件所对应的解集的交集,进而得出正解

model()

定义变量:

单个变量
a = Int('a') 有符号
a = BitVec("a",8) 无符号
多个变量
a,b,c = Ints('a','b','c')

实际利用

这里用一个例子来具体使用一个Z3库(安恒杯11月赛的re100):
题目是一个64位的windows上的可执行文件,用PEID查有没有加壳也没有查出来什么,载入IDA中,发现程序的流程还是很简单的;

// local variable allocation has failed, the output may be wrong!
int __cdecl main(int argc, const char **argv, const char **envp)
{
  __int64 v3; // rdx
  __int64 v4; // rcx
  __int64 v5; // r8
  __int64 v6; // r8
  int result; // eax
  unsigned __int8 v8; // [rsp+46h] [rbp-Ah]
  char v9; // [rsp+47h] [rbp-9h]
  signed int i; // [rsp+48h] [rbp-8h]
  signed int j; // [rsp+48h] [rbp-8h]
  unsigned int v12; // [rsp+4Ch] [rbp-4h]
  _fentry__(*&argc, argv, envp);
  monstartup();
  _main();
  v12 = Getinput(v4, v3, v5);                   // 将输入的字符串转成数字 比如:"1234567890"->1234567890
  v9 = 0;
  for ( i = 0; i <= 31; ++i )
  {
    v8 = v9 ^ v12 ^ byte_404020[i];
    if ( (v8 <= 0x40u || v8 > 0x5Au) && v8 != 0x5F && v8 != 0x7B && v8 != 0x7D )
    {
      puts("Error\n");
      exit(1);
    }
    byte_408040[i] = v8;                        // 将最低有效位给了flag[i]
    v9 ^= byte_404020[i];                       // 更新v8
    v12 >>= 1;
  }
  result = is_begin_with(byte_408040, start, v6);
  if ( result )
  {
    result = byte_40805F;
    if ( byte_40805F == '}' )
    {
      result = puts("Congratulations!\nflag is:");
      for ( j = 0; j <= 31; ++j )
        result = putchar(byte_408040[j]);
    }
  }
  return result;
}

首先是条用了Getinput:

int __fastcall Getinput(__int64 a1, __int64 a2, __int64 a3)
{
  _QWORD *v3; // rdi
  __int64 v5; // [rsp+0h] [rbp-80h]
  char DstBuf; // [rsp+20h] [rbp-60h]
  _fentry__(a1, a2, a3);
  memset(&v5 + 4, 0, 0x30ui64);
  v3 = &v5 + 10;
  *v3 = 0;
  *(v3 + 2) = 0;
  puts("try to enter a number to generate the flag");
  read(0, &DstBuf, 0x10u);
  return atoi(&DstBuf);                         // 将我们输入的字符串变成数字
}

read读入16位的字符串,atoi将我们输入的字符串转变成相对应的数字;接着主函数就对我们输入的数字进行操作,首先的操作是先将byte_404020[i]与我们输入的数字进行异或,然后取有效位的四位(也就是16进制的后两位)与v9异或,将结果存到v8中,然后判断v8是不是在一个区间中,若不在,则退出,若在,则继续往下执行,将v8的后两位存到byte_408040数组里(这个数组就是存放flag的),v9和byte_404020[i]异或,最后将我们输入的数字右移一位,接着循环;

生成Flag流程:
v8 = ((num^byte_404020[i])&0xff)^ v9
flag[i] = v8
v9 ^ byte_404020[i]
num>>=1

当循环结束之后会进入到一个is_begin_with函数,这个函数是检查flag的前5位是不是“FLAG{”,之后有检查了flag的最后一位是不是“}”,是的话则输出flag,不是的话则退出。因为输出的flag是根据我们的输入而生成的,所以我们不能通过修改程序流来直接输出flag,所以我们就要一个一个爆破了,通过一些信息我们可以将输入的数字化一个区间,一是v12是无符号的整数类型4个字节,32位,而是我们输入的字符串的长度是16,三是循环次数是32次,所以我们可以得出我们输入的数字在2**31~2**32之间,虽然范围还是很大,下面是利用Z3写的脚本:


\#coding:utf-8 from z3 import * import time time1 = time.time() current = [164,25,4,130,126,133,80,168,209,234,227,249,232,225,96,58,26,10,135,221,225,97,160,192,96,164,72,40,22,11,5,32] solve = Solver() num = BitVec('x',64) solve.add(num>=2**31) solve.add(num<2**32) v9 = 0 flag = "FLAG{" index=0 for x in range(32): if x<5: solve.add(((num^current[x])&0xff)^v9==ord(flag[x])) elif 5<=x<31: solve.add(Or( And((((num^current[x])&0xff)^v9)<=ord("Z"),(((num^current[x])&0xff)^v9)>=ord("A")),(((num^current[x])&0xff)^v9)==ord("_"))) else: solve.add((((num^current[x])&0xff)^v9)==ord("}")) v9^=current[x] v9&=0xff num>>=1 if solve.check()==sat: a=solve.model() print a else: print "NO result!" time2 = time.time() print time2-time1 #out: [x = 3658134498] 0.0701808929443

可见速度是非常快的,快的没的说!

添加新评论