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

Question

[我正在学习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)

Answer 1

您如何编写此代码有些问题，但是我认为您如何解决此问题还有一个更根本的问题。最后，您要做的只是要求Z3为您找到两个长度为31（因为31 * 8 = 248）的整数列表，以使它们的元素xor为密码。它做的很好。要查看，我在您的程序中添加了以下内容：