时间戳

首页 > 解决方案 > 使用 Z3 库复制反编译的 C 代码

z3 - 使用 Z3 库复制反编译的 C 代码

问题描述

我正在学习 Z3 并尝试使用 Z3 对加密算法进行逆向工程，而不是用 C 编写它。我有以下由 IDA 反编译的伪代码：

int __cdecl main(int argc, const char **argv, const char **envp)
{
  char *v3; // rsi
  unsigned int v4; // eax
  int v5; // eax
  __m128i *v6; // rbx
  __int64 v7; // rdx
  char v9; // [rsp+0h] [rbp-80h]
  __int64 v10; // [rsp+10h] [rbp-70h]
  int v11; // [rsp+18h] [rbp-68h]
  __int16 v12; // [rsp+1Ch] [rbp-64h]
  char v13; // [rsp+1Eh] [rbp-62h]
  char v14; // [rsp+1Fh] [rbp-61h]
  __m128i v15; // [rsp+20h] [rbp-60h]
  __int64 v16; // [rsp+30h] [rbp-50h]
  __int64 v17; // [rsp+38h] [rbp-48h]

  _main(argc, argv, envp);
  strcpy(v15.m128i_i8, "THE SECRET HAS BEEN REMOVED LOL");
  v3 = &v9;
  v4 = _time64(0i64);
  srand(v4);
  do
  {
    v5 = rand();
    *(++v3 - 1) = v5 - ((unsigned __int64)((0x7F807F81i64 * v5) >> 39) - (v5 >> 31));
  }
  while ( v3 != &v14 );
  v6 = &v15;                                   
  v15 = _mm_xor_si128(_mm_loadu_si128((const __m128i *)&v9), v15);
  v16 ^= v10;
  LODWORD(v17) = v11 ^ v17;
  WORD2(v17) ^= v12;
  BYTE6(v17) ^= v13;
  do
  {
    v7 = LOBYTE(v6->m128i_i64[0]);
    v6 = (__m128i *)((char *)v6 + 1);
    printf("%.2x ", v7);
  }
  while ( v6 != (__m128i *)((char *)&v17 + 7) );
  return 0;
}

简而言之，它从 rand() 中获取一个随机数（以时间为种子）并将其与秘密消息异或。我有密文（我的python代码中的ctext）。我试图用 Z3 暴力破解代码。它是坐着的，但我弄错了秘密信息。有什么问题？我可能会犯菜鸟错误，所以请不要太苛刻。这是python 3代码：

from z3 import *

# The ciphertext is:
ctext="9a 60 76 14 8b 36 5a 10 2b 91 \
c4 6c ab 27 92 99 f8 6a ec 5d 32 20 3d 61 8f c7 fb dd 02 72 bf"
ctext = ctext.split(' ')

S=Solver()

# We want a message with printable chars
def is_printable(x):
    x = BV2Int(x)
    return And((x>=0x20),
               (x<=0x7e))

key=[]
v5 = BitVec("v5",248) # key
for i in range(0, 248, 8):
    seed_byte = Extract(i + 7, i, v5)
    seed_byte = seed_byte - ((seed_byte * 2139127681) >> 39) - (seed_byte >> 31)
    seed_byte = Extract(7, 0, seed_byte)
    key.append(seed_byte)

message=[]
v15 = BitVec("v15",248) # message
for i in range(0, 248,8):
    message_byte = Extract(i+7,i,v15)
    S.add(is_printable(message_byte))
    message.append(message_byte)

j=0
for i in range(0, 248,8):
    secret = Extract(i+7,i,v15)
    S.add((key[j] ^ secret) == int(ctext[j],16))
    j+=1




print(S.check())
str = S.model()[v15].as_string()
result = hex(int(str,10))[2:]
f=""
for i in range(0,len(result),2):
    f+=chr(int(result[i:i+2],16))
print("The message is: \n" + f)

标签： z3

解决方案

您的编码方式存在一些问题，但我认为您处理此问题的方式存在更根本的问题。最后，您要做的就是要求 Z3 为您找到两个长度为 31 的整数列表（因为 31*8 = 248），这样它们的元素异或就是密码。它做得非常好。为了查看，我在您的程序中添加了以下内容：

S.check()
m = S.model()

mesg   = [m.eval(i).as_long()  for i in message]
key    = [m.eval(i).as_long()  for i in key]
cipher = [int(i, 16) for i in ctext]
check  = [m ^ k for (m, k) in zip(mesg, key)]
print cipher == check

它打印：

True

因此，该解决方案确实是“正确的”，Z3 完全按照您的要求进行了操作。

显然这不是你“想要”它做的！使用基于 XOR 的加密，您将获得每个密钥和每个密文的答案。你需要进一步的约束。（您的“仅 ascii”约束排除了一堆解决方案，但同样，这并不是真正关注实际问题。）

因此，您有两个选择：遍历所有解决方案，看看您喜欢哪一个，或者以某种方式进一步限制问题以获得唯一的解决方案。但两者都不是真正可行的：首先，解决方案空间如此巨大，您的计算机（和您）将在您完成每个解决方案之前很久就死了。其次，您只是没有从所描述的内容中获得足够的信息来获得独特的模型。

这一点也不奇怪：毕竟，从某种意义上说，这就是所谓的“一次性”加密，而且非常完美：没有任何信息可以从密文中收集到可以让你缩小范围的信息搜索空间。

希望这能让你走上正确的道路。一旦你有了其他一些可用的约束，我们就可以讨论如何在 z3py 中实际编写代码。（特别是，您应该使用 BV 操作，不要将整数与位向量混合，并且尽量不要像您所做的那样进行分配。但是所有这些讨论都没有实际意义，因为您在这里使用的蛮力方法只是不可行。）

推荐阅读