Использование z3, где ограничение зависит от выхода функции - PullRequest
Новая
       9

Использование z3, где ограничение зависит от выхода функции

0 голосов
/ 11 декабря 2018

Я хочу использовать z3 для решения этого случая.Ввод представляет собой строку из 10 символов.Каждый символ ввода является печатным символом (ASCII).Входные данные должны быть такими, чтобы при вызове функции calc2 () с входным параметром в качестве параметра получался результат: 0x0009E38E1FB7629B.

Как использовать z3py в таких случаях?

Обычно я хотел быпросто добавьте независимые уравнения в качестве ограничения для z3.В этом случае я не уверен, как использовать z3. 

def calc2(input):
    result = 0

    for i in range(len(input)):
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = (r1 ^ r2)

        result = (r3 ^ ord(input[i]))

    return result

if __name__ == "__main__":
        input = sys.argv[1]
        result = calc2(input)

        if result == 0x0009E38E1FB7629B:
             print "solved"

Обновление: Я пробовал следующее, но это не дает мне правильный ответ: 

from z3 import *

def calc2(input):
    result = 0

    for i in range(len(input)):
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = (r1 ^ r2)

        result = r3 ^ Concat(BitVec(0, 56), input[i])


    return result

if __name__ == "__main__":
    s = Solver()
    X = [BitVec('x' + str(i), 8) for i in range(10)]

    s.add(calc2(X) == 0x0009E38E1FB7629B)

    if s.check() == sat:
        print(s.model())

Ответы [ 2 ]

0 голосов
/ 11 декабря 2018

Я надеюсь, что это не домашняя работа, но вот один из способов сделать это: 

from z3 import *

s = Solver()

# Input is 10 character long; represent with 10 8-bit symbolic variables
input = [BitVec("input%s" % i, 8) for i in range(10)]

# Make sure each character is printable ASCII, i.e., between 0x20 and 0x7E
for i in range(10):
  s.add(input[i] >= 0x20)
  s.add(input[i] <= 0x7E)

def calc2(input):

    # result is a 64-bit value
    result = BitVecVal(0, 64)

    for i in range(len(input)):
        # NB. We don't actually need to mask with 0xffffffffffffffff
        # Since we explicitly have a 64-bit value in result.
        # But it doesn't hurt to mask it, so we do it here.
        r1 = (result << 0x5) & 0xffffffffffffffff
        r2 = result >> 0x1b
        r3 = r1 ^ r2

        # We need to zero-extend to match sizes
        result = r3 ^ ZeroExt(56, input[i])

    return result


# Assert the required equality
s.add(calc2(input) == 0x0009E38E1FB7629B)

# Check and get model
print s.check()
m = s.model()

# reconstruct the string:
s = ''.join([chr (m[input[i]].as_long()) for i in range(10)])
print s

Это печатает: 

$ python a.py
sat
L`p:LxlBVU

Похоже, ваша секретная строка

"L`p: LxlBVU"

Я добавил несколько комментариев в программу, чтобы помочь вам с тем, как все закодировано в z3py, но не стесняйтесь спрашивать разъяснения,Надеюсь, это поможет!

Получение всех решений

Чтобы получить другие решения, вы просто зацикливаетесь и утверждаете, что решение не должно быть предыдущим.Вы можете использовать следующий цикл while после утверждения: 

while s.check() == sat:
   m = s.model()
   print ''.join([chr (m[input[i]].as_long()) for i in range(10)])
   s.add(Or([input[i] != m[input[i]] for i in range(10)]))

Когда я его запустил, он продолжал идти!Вы можете остановить его через некоторое время.

0 голосов
/ 11 декабря 2018

Вы можете кодировать calc2 в Z3.вам нужно будет развернуть цикл 1,2,3,4, .., n раз (для n = ожидаемый максимальный размер ввода), но это все.(На самом деле вам не нужно развертывать цикл, вы можете использовать z3py для создания ограничений)

...