技术分享

Technology sharing

带你入逆向坑,怎样在win10上安装并使用Z3库
2018-09-19 15:44

本文为原创文章,转载请注明出处!



本文主要是写一下自己在使用Z3约束器来解方程时遇到的坑,失败了好多次才流泪写下这篇教程(好几次都想放弃)  避免大家和我一样浪费时间 百度谷歌了好久 也没找到方法 话说大佬们是不是有什么技巧

一、z3简单介绍

z3是由微软公司开发的一个优秀的SMT求解器(其实就是一个定理证明器),它能够检查逻辑表达式的可满足性。我们做CTF逆向题可能会经常用它来解方程。变量类型有整数Int,实数Real(需要得到float型的值时可以用这个),至于数组,就用BitVec好啦

先来说一下简单的使用吧

比如我想求一下a*b=0x24这个方程的解

微信图片_20180919144606.jpg

很明显,这里的解不止一个

这里就是z3的一个特点就是当解有多个的时候只会帮我们求出一个可能的解

如果我们想要拿到需要的解 那就增加约束条件  比如我想要得到当a==2时的解 就像下图所示:

微信图片_20180919144709.jpg

二、windows下安装z3步骤

1:确定你的Python版本为2.X(我的是2.7)

2:pipinstall z3或者pipinstall z3-solver是不行的(亲测)

3:必须采用源码安装

下载链接:

https://pypi.org/project/z3-solver/4.5.1.0/#files

我用的是这个版本 可以正常使用  好像有新版本  你自己可以尝试

4:下载对应电脑版本的

    我的电脑是win10x64位专业版,所以我选择的是 

微信图片_20180919144854.png

点击就可以下载

5:安装的话直接cmd 

(如果你的环境变量配置的是默认Python3的话  记得一定要切换到Python2.x\Scripts)

6:最后输入命令 

pipinstall z3_solver-4.5.1.0-py2-none-win_amd64.whl

微信图片_20180919145047.png

注意:文件路径,我是直接放在了桌面

三、说一下z3的用法

以iscc中的一道逆向题为例

先放到我的ubuntu子系统中  file一下  格式file + 文件名

知道是elfx64位文件,于是直接载入IDAx64中,函数不是太多,直接双击左侧main

发现右侧图形模式很明显的可以看到一些关键的字符串,稍加思索就可以知道sub_400766就是关键的函数 jz是关键跳转

微信图片_20180919145312.jpg

那么我们先F5一下,接着双击函数名

微信图片_20180919145419.png

看到有一个长度的判断  还有两个四元一次方程组  等等

微信图片_20180919145926.jpg


但是这样对于新手来说不太好看  那就美化一下

在s头上按Y键  将原来的char s[4] 改为chars[32]  点击OK

微信图片_20180919150039.png


将那些让人头大的变量名按N重新命名(x1~x8),就像下图一样

接着右键—Hidecast(隐藏声明),最后变成这个样子

微信图片_20180919150148.jpg

具体计算的时候我们分开来做,先来求解第一个方程组

微信图片_20180919150253.jpg


这时候可以得到

[x4= 862734414,

x3= 829124174,

x2= 1801073242,

x1= 1869639009]

接着打算用python求srand的种子还有确定v1,v2,v7,v8,v9,v10,v11,v12的值的

但是不会

我是直接gdb动态调试得到的

v1= 0x16

v2= 0x27

v7= 0x2d

v8= 0x2d

v9= 0x23

v10= 0x29

v11= 0xd

v12= 0x24

有大佬用的C语言解的 我觉得很不错  贴上来

#include<stdio.h>

#include<stdlib.h>

intv1,v2,v7,v8,v9,v10,v11,v12;

intmain(void) {

srand(829124174^ 1801073242 ^ 1869639009 ^ 862734414);

v1 = rand() % 50;

v2 = rand() % 50;

v7 = rand() % 50;

v8 = rand() % 50;

v9 = rand() % 50;

v10 = rand() % 50;

v11 = rand() % 50;

v12 = rand() % 50;

printf("v1=%d \n v2=%d \n V7=%d \n v8=%d \n v9=%d \n v10=%d \n v11=%d \nv12=%d",v1,v2,v7,v8,v9,v10,v11,v12);

return0;

}

接着求解第二个方程组,代码如下

微信图片_20180919161206.jpg

好啦  接下来就简单了

不过还缺一个库libnum(同样只能python2.x安装百度有教程),我还是用kalilinux吧

微信图片_20180919163706.jpg


当然这个还不是flag

需要运行 输入得到的ampoZ2ZkNnk1NHl3NTc0NTc1Z3NoaGFG

即可得到 flag{th3_Line@r_4lgebra_1s_d1fficult!}

完。后记:最好还是用linux吧,有些库太难装了



文章仅用于普及网络安全知识,提高小伙伴的安全意识的同时介绍常见漏洞的特征等,若读者因此做出危害网络安全的行为后果自负,与合天智汇以及原作者无关,特此声明。



上一篇:Linux heap 学习 (下)
下一篇:docker简单实用教程
版权所有 合天智汇信息技术有限公司 2013-2018 湘ICP备14001562号-6
Copyright © 2013-2018 Heetian Corporation, All rights reserved
4006-123-731