我正在学习如何使用 z3(我想在 CTF 挑战中使用它)并且已经达到了我开始同意我妻子最喜欢的说法“我需要帮助”的地步:) 我在这里发帖希望有人可以查看我的嵌入式示例问题(CTF 二进制文件中的实际代码太大且令人费解,无法在此处包含)并帮助指导我获得上述帮助。
我想要完成的是:
- 我想将两个 python 列表(包含 32 位值)作为函数参数传递给函数。
- 在这个函数中,我提取函数参数并在一些基本的数学例程中使用它们。
- 最终计算将被记录回第一个 python 列表
现在我已经编写并重写了下面的代码,直到我脸色发青,头发都拔光了,还没有弄清楚我做错了什么。作为健全性检查,我添加了代码,当在没有 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]))