时间戳

首页 > 解决方案 > 调用修改输入的函数时如何正确使用z3

python - 调用修改输入的函数时如何正确使用z3

问题描述

我正在学习如何使用 z3（我想在 CTF 挑战中使用它）并且已经达到了我开始同意我妻子最喜欢的说法“我需要帮助”的地步:) 我在这里发帖希望有人可以查看我的嵌入式示例问题（CTF 二进制文件中的实际代码太大且令人费解，无法在此处包含）并帮助指导我获得上述帮助。

我想要完成的是：

现在我已经编写并重写了下面的代码，直到我脸色发青，头发都拔光了，还没有弄清楚我做错了什么。作为健全性检查，我添加了代码，当在没有 z3 的情况下使用时会生成我正在寻找的 64 位密钥（它不知道列表值之一是什么，但显示了我希望 z3 找出的最终答案）。

最后，我知道下面的代码在 z3 本质上是相当简单的（代码也只是为了帮助支持我的问题而设计的，因此没有编码为发布/生产标准）并且我可能缺少基本概念（在我之后对这个 SMT 事情非常陌生）所以不要害怕证实我妻子的理论：我很愚蠢；）因为这不是第一次这样一件可能的微不足道的事情让我发疯了几天（而且我肯定不会是最后一次）。

非常感谢任何可以将我的头从沙子中拉出来并向我展示我的方式错误的人。

顺便说一句：sample_func 代码是来自 CTF 二进制文件的实际汇编语言代码的 Python 表示

from z3 import *

def sample_func(pDataBuf_1, pDataBuf_2):

    tVar1 = pDataBuf_1[0]
    tVar2 = pDataBuf_1[1]

    xVar1 = pDataBuf_1[0]
    xVar2 = pDataBuf_1[1]


    tVar3 =(  (tVar1 * 0x1000 | tVar2 >> 0x14) + xVar1 ) & 0xFFFFFFFF
    tVar4 =(  ((tVar3 ^ xVar2) & xVar2 ^ tVar3) + xVar2 + -0x3e423112 + tVar2 ) & 0xFFFFFFFF

    pDataBuf_1[0] = tVar4
    pDataBuf_1[1] = tVar3

    #
    # I am adding the return value as a value for z3 to check against.  What I 
    # really want is to have z3 just operate on the bitvector values.  In the real
    # binary these bitvector values will be used to form two 64 bit keys.
    #
    return (tVar3 << 32) | tVar4

use_z3 = False

non_z3_pbuf1 = [0x67452301, 0xefcdab89] 

p1 = z3.BitVecVal(0x00000000, 32) # Z3 needs to figure out that p1 == 0x67452301
p2 = z3.BitVecVal(0xefcdab89, 32)

tlist1 = [p1, p2]

non_z3_pbuf2 = [0x79707062, 0x6d326e34]

pb1 = z3.BitVecVal(0x79707062, 32)
pb2 = z3.BitVecVal(0x6d326e34, 32)

tlist2 = [pb1, pb2]

if use_z3 == True:
    s = Solver()

    while True:
        s.add( sample_func(tlist1, tlist2) == 0xb97541fda15711fd)    
        print(s)
        if s.check() == sat:
            break;
else:
    #
    # Using non_z3_pbuf1 and non_z3_pbuf2 will generate the following 
    # results:
    #
    #    0xb97541fda15711fd
    #    0xa15711fd
    #    0x6d326e34
    #
    x = sample_func(non_z3_pbuf1, non_z3_pbuf2)
    print(hex(x))
    print(hex(non_z3_pbuf1[0]))
    print(hex(non_z3_pbuf2[1]))

标签： pythonz3pyctf

解决方案

最好提出具体问题，而不是一般性建议。但看起来你在正确的道路上。特别是，您应该使用print s.sexpr()where sis the solver instance 来查看 z3 试图解决的问题。很难从您的问题中解读出确切的目标，但这里有一个简单的重写：

from z3 import *

def sample_func(pDataBuf_1, pDataBuf_2):

    tVar1 = pDataBuf_1[0]
    tVar2 = pDataBuf_1[1]

    xVar1 = pDataBuf_1[0]
    xVar2 = pDataBuf_1[1]


    tVar3 =(  (tVar1 * 0x1000 | tVar2 >> 0x14) + xVar1 ) & 0xFFFFFFFF
    tVar4 =(  ((tVar3 ^ xVar2) & xVar2 ^ tVar3) + xVar2 + -0x3e423112 + tVar2 ) & 0xFFFFFFFF

    pDataBuf_1[0] = tVar4
    pDataBuf_1[1] = tVar3

    return (tVar3 << 32) | tVar4

p1 = BitVec('p1', 32)
p2 = BitVec('p2', 32)

tlist1 = [p1, p2]

pb1 = BitVec('pb1', 32)
pb2 = BitVec('pb2', 32)

tlist2 = [pb1, pb2]

s = Solver()
s.add( sample_func(tlist1, tlist2) == 0xb97541fda15711fd)
print s.sexpr()

res = s.check()

if res == sat:
   print s.model()
else:
   print "Didn't get sat"

当我运行它时，我得到：

(declare-fun p2 () (_ BitVec 32))
(declare-fun p1 () (_ BitVec 32))
(assert (let ((a!1 (bvand (bvadd (bvor (bvmul p1 #x00001000) (bvashr p2 #x00000014)) p1)
                  #xffffffff)))
(let ((a!2 (bvadd (bvxor (bvand (bvxor a!1 p2) p2) a!1) p2 #xc1bdceee p2)))
  (= (bvor (bvshl a!1 #x00000020) (bvand a!2 #xffffffff)) #xa15711fd))))

[p1 = 2944401152, p2 = 269336837]

现在，您应该研究打印内容的第一部分。这就是您“构建”并提供给 z3 的程序。它采用类似 lisp 的符号，但应该易于阅读。需要注意的一件事是，变量pb1永远pb2不会出现！那是因为你没有在sample_func. 那是你的意图吗？下一步是研究打印的表达式并确保它确实是您想要计算的。你可以从那里拿走它。

最后，确保找到的模型 z3（即[p1 = 2944401152, p2 = 269336837]在本例中）确实是您构建的程序的正确答案。如果您真的是认真写的，那将很清楚！（答案无疑是正确的；但可能不是您想要的。）

通常，在使用 z3py 编程时，您应该考虑“函数”而不是“覆盖”变量。但是，随着您取得进展，最好继续沿着这条道路和具体问题。祝你好运！

推荐阅读