欢迎来到 黑吧安全网 聚焦网络安全前沿资讯,精华内容,交流技术心得!

Z3Py在CTF逆向中的运用

来源:本站整理 作者:佚名 时间:2018-05-15 TAG: 我要投稿

前言
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
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;
}
可以看得出来这个题目的目的就是找出满足方程的flag。我们可以很方便的把方程式列出来,但是求解对于一些数学不是很好的人来说简直就是噩梦,这时候Z3求解器就可以很方便的给我们帮助。我们按照题目的意思一步一步利用Z3求解器来求解:
from z3 import *
x1 = Int('x1')
x2 = Int('x2')
x3 = Int('x3')
x4 = Int('x4')
s = Solver()
s.add( x2*x1-x4*x3 == 0x24CDF2E7C953DA56)
s.add( 3*x3+4*x4-x2-2*x1 == 0x17B85F06)
s.add( 3*x1*x4-x3*x2 == 0x2E6E497E6415CF3E)
s.add( 27*x2+x1-11*x4 - x3 == 0x95AE13337)
print s.check()
m = s.model()
print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])
Solver()命令创建一个通用求解器。我们可以通过add函数添加约束条件。我们称之为声明约束条件。check()函数解决声明的约束条件,sat结果表示找到某个合适的解,unsat结果表示没有解。这时候我们称约束系统无解。最后,求解器可能无法解决约束系统并返回未知作为结果。
对于上面的题目我们首先定义x1,x2,x3,x4四个int变量,然后添加逆向中的约束条件,最后进行求解。Z3会在找到合适解的时候返回sat。我们认为Z3能够满足这些约束条件并得到解决方案。该解决方案被看做一组解决约束条件的模型。模型能够使求解器中的每个约束条件都成立。最后我们遍历model中的解。
得到x1,x2,x3,x4的解后,我们将其代入逆向题中,得出v1,v2,v7,v8,v9,v9,v10,v11,v12的值,然后进行下一步的求解:
v1 = 0x16
v2 = 0x27
v7 = 0x2d
v8=  0x2d
v9 = 0x23
v10= 0x29
v11 = 0xd
v12 = 0x24
v3 = Int('v3')
v4 = Int('v4')
v5 = Int('v5')
v6 = Int('v6')
s = Solver()
s.add(v6 * v2 + v3 * v1 - v4 - v5 == 0xE638C96D3)
s.add(v6 + v3 + v5 * v8 - v4 * v7 == 0xB59F2D0CB)
s.add(v3 * v9 + v4 * v10 - v5 - v6 == 0xDCFE88C6D)
s.add(v5 * v12 + v3 - v4 - v6 * v11 == 0xC076D98BB)
print s.check()
m = s.model()
print "traversing model..."
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])
这样的话我们就花了比较少的时间得到我们想要的flag,还是比较方便的。

[1] [2]  下一页

【声明】:黑吧安全网(http://www.myhack58.com)登载此文出于传递更多信息之目的,并不代表本站赞同其观点和对其真实性负责,仅适于网络安全技术爱好者学习研究使用,学习中请遵循国家相关法律法规。如有问题请联系我们,联系邮箱admin@myhack58.com,我们会在最短的时间内进行处理。
  • 最新更新
    • 相关阅读
      • 本类热门
        • 最近下载