Z3Py在CTF逆向中的利用
发布时间：2022-07-04 04:45:43 所属栏目：安全 来源：互联网
导读：前言 Z3是Microsoft Research开发的高性能定理证明器。Z3拥有者非常广泛的应用场景：软件/硬件验证和测试，约束求解，混合系统分析，安全性研究，生物学研究（计算机分析）以及几何问题。Z3Py是使用Python脚本来解决一些实际问题，Z3Py在windows下的安装可以
|
前言 Z3是Microsoft Research开发的高性能定理证明器。Z3拥有者非常广泛的应用场景：软件/硬件验证和测试，约束求解，混合系统分析，安全性研究，生物学研究（计算机分析）以及几何问题。Z3Py是使用Python脚本来解决一些实际问题，Z3Py在windows下的安装可以参考如下链接：https://github.com/Z3Prover/z3/wiki/Using-Z3Py-on-Windows。Z3Py的使用教学可以参考如下链接： https://ericpony.github.io/z3py-tutorial/guide-examples.htm CTF逆向中的应用 现在的CTF逆向中，求解方程式或者求解约束条件是非常常见的一种考察方式，而ctf比赛都是限时的，当我们已经逆向出来flag的约束条件时，可能还需要花一定的时间去求解逆过程。而Z3求解器就给我们提供了一个非常便利求解方式，我们只需要定义未知量（x,y等），然后为这些未知量添加约束方式即可求解。Z3求解器能够求解任意多项式，但是要注意的是，当方程的方式为2**x这种次方运算的时候，方程式已经不是多项式的范畴了，Z3便无法求解。 基本使用 现在我们利用官方文档中的一个例子来粗略的看一下Z3Py的使用。 x = Int('x') y = Int('y') solve(x > 2, y < 10, x + 2*y == 7) 代码非常简单，首先利用Int()定义两个int型未知数x和y，然后利用三个约束条件进行相应的求解： x > 2 y < 10 x + 2*y == 7 由上述的代码看得出来Z3Py的使用方式比较简单， 定义未知量 添加约束条件 然后求解 CTF中的示例 XXX比赛中的逆向题 首先我们利用IDA去打开该文件，定位到关键点，发现关键函数如下： signed __int64 sub_400766() { if ( strlen((const char *)&stru_6020A0) != 32 ) return 0LL; v3 = stru_6020A0.y1; v4 = stru_6020A0.y2; v5 = stru_6020A0.y3; v6 = stru_6020A0.y4; if ( stru_6020A0.x2 * (signed __int64)stru_6020A0.x1 - stru_6020A0.x4 * (signed __int64)stru_6020A0.x3 != 0x24CDF2E7C953DA56LL ) goto LABEL_15; if ( 3LL * stru_6020A0.x3 + 4LL * stru_6020A0.x4 - stru_6020A0.x2 - 2LL * stru_6020A0.x1 != 0x17B85F06 ) goto LABEL_15; if ( 3 * stru_6020A0.x1 * (signed __int64)stru_6020A0.x4 - stru_6020A0.x3 * (signed __int64)stru_6020A0.x2 != 0x2E6E497E6415CF3ELL ) goto LABEL_15; if ( 27LL * stru_6020A0.x2 + stru_6020A0.x1 - 11LL * stru_6020A0.x4 - stru_6020A0.x3 != 0x95AE13337LL ) goto LABEL_15; srand(stru_6020A0.x3 ^ stru_6020A0.x2 ^ stru_6020A0.x1 ^ stru_6020A0.x4); v1 = rand() % 50; v2 = rand() % 50; v7 = rand() % 50; v8 = rand() % 50; v9 = rand() % 50; v10 = rand() % 50; v11 = rand() % 50; v12 = rand() % 50; if ( v6 * v2 + v3 * v1 - v4 - v5 != 0xE638C96D3LL || v6 + v3 + v5 * v8 - v4 * v7 != 0xB59F2D0CBLL || v3 * v9 + v4 * v10 - v5 - v6 != 0xDCFE88C6DLL || v5 * v12 + v3 - v4 - v6 * v11 != 0xC076D98BBLL ) { LABEL_15: result = 0LL; } else { result = 1LL; } return result; } 函数关键部分如下： int __cdecl main(int argc, const char **argv, const char **envp) { unsigned int ii; // esi unsigned int v4; // kr00_4 char flag_i; // bl unsigned int jj; // eax char *v7; // edx char v8; // cl int v9; // eax char xor_result[80]; // [esp+8h] [ebp-A4h] char flag[80]; // [esp+58h] [ebp-54h] sub_DC1020("Please input your flag: "); sub_DC1050("%40s", flag); memset(xor_result, 0, 0x50u); ii = 0; v4 = strlen(flag); if ( v4 ) { do { flag_i = flag[ii]; jj = 0; do { v7 = &xor_result[jj + ii]; v8 = flag_i ^ data1[jj++]; *v7 += v8; } while ( jj < 0x20 ); ++ii; } while ( ii < v4 ); } v9 = strcmp(xor_result, (const char *)&data2); if ( v9 ) v9 = -(v9 < 0) | 1; if ( v9 ) puts("No, it isn't."); else puts("Yes, it is."); return 0; } 很简洁明了，我们利用Z3Py来进行变量的声明和约束的增加并进行求解 from z3 import * s = Solver() X = [BitVec(('x%s' % i),8) for i in range(0x22) ] data1 = [0x21,0x22,0x23,0x24,0x25,0x26,0x27,0x28,0x29,0x2A,0x2B,0x2C,0x2D,0x2E,0x2F,0x3A, 0x3B,0x3C,0x3D,0x3E,0x3F,0x40,0x5B,0x5C,0x5D,0x5E,0x5F,0x60,0x7B,0x7C,0x7D,0x7E] data2 = [0x72,0xE9,0x4D,0xAC,0xC1,0xD0,0x24,0x6B,0xB2,0xF5,0xFD,0x45,0x49,0x94,0xDC,0x10, 0x10,0x6B,0xA3,0xFB,0x5C,0x13,0x17,0xE4,0x67,0xFE,0x72,0xA1,0xC7,0x04,0x2B,0xC2, 0x9D,0x3F,0xA7,0x6C,0xE7,0xD0,0x90,0x71,0x36,0xB3,0xAB,0x67,0xBF,0x60,0x30,0x3E, 0x78,0xCD,0x6D,0x35,0xC8,0x55,0xFF,0xC0,0x95,0x62,0xE6,0xBB,0x57,0x34,0x29,0x0E,3] xor_result = [0]*0x41 for m in range(0,0x22): for n in range(0,0x20): xor_result[n+m] += X[m] ^ data1[n] for o in range(0,0x41): s.add(xor_result[o] == data2[o]) print s.check() m = s.model() print "traversing model..." for i in range(0,0x22): print chr(int("%s" % (m[X[i]]))), 很简单的几行代码，声明0x22个8位BitVec的未知数，获取数据，然后增加约束条件，求解，这样就能够帮助我们获取flag。 题目链接：https://pan.baidu.com/s/1o8QdFIE 总结 虽然CTF逆向比赛中重点考察的是逆向的能力，采用求解器的方式来求解并不能锻炼到自己的逆向逻辑，REConvolution逆向题目有一个非常清晰明了的逆过程，还是很有趣的。 （编辑：财气旺网 - 财气网） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |
站长推荐