Реплицируйте декомпилированный код C с библиотекой Z3

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 () (со временем в качестве начального числа) и записывает его в секретное сообщение. У меня есть зашифрованный текст (ctext в моем python коде). Я пытался перебором кода с помощью Z3. Сел, но в секретном сообщении я неправильно понял. Что может быть не так? Возможно, я делаю ошибки ладьи ie, поэтому, пожалуйста, не будь слишком грубым sh. Вот код 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 является шифром. И это делает это прекрасно. Чтобы увидеть, я добавил в вашу программу следующее:

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, не смешивать целые числа с битовыми векторами и стараться не выполнять присваивания, как вы. Но все это обсуждение является спорным, так как используемый здесь метод грубой силы просто нежизнеспособен.)