调用修改inpu的函数时如何正确使用z3

Question

我正在学习如何使用z3（我想在CTF挑战中使用它），我开始同意我妻子最喜欢的一句话“我需要帮助”：）我在这里发帖，希望有人能回顾一下我的嵌入式示例问题（CTF二进制文件中的实际代码太大，太复杂）包括在这里）和帮助指导我通过获得所说的帮助

我要做的是：

• 我想将两个python列表（包含32位值）作为函数参数传递到函数中
• 在这个函数中，我提取函数参数并在一些基本的数学例程中使用它们
• 最后的计算结果将记录回第一个python列表中

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

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

提前向任何人表示感谢，谁能把我的头从沙子里拔出来，让我知道我的错误

顺便说一句：示例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]))

Answer 1

最好问一些具体的问题，而不是一般性的建议。但看起来你走对了路。特别是，您应该使用print s.sexpr()，其中s是解算器实例，以查看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编程时，应该考虑“函数”而不是“覆盖”变量。但最好继续走这条路，并在取得进展时提出具体问题。祝你好运