使用 z3 其中约束取决于函数的输出

Question

我想用 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())

Answer 1

您可以在 Z3 中对 calc2 进行编码。您需要将循环展开 1,2,3,4,..,n 次（对于 n = 预期的最大输入大小），仅此而已。（您实际上不需要展开循环，您可以使用 z3py 创建约束）