逆向工程 Z3 SMT 求解器解决方案

Question

我正在使用名为 SMT 求解器的 Z3 在某些约束下从给定向量生成一组新的随机数。我这样做是为了隐藏我的输入流。对应代码如下：

from z3 import *
import sys
import io
import math


X0 = Real('X0')
X1 = Real('X1')
X2 = Real('X2')
X3 = Real('X3')
X4 = Real('X4')
X5 = Real('X5')
X6 = Real('X6')
X7 = Real('X7')
X8 = Real('X8')
X9 = Real('X9')
X10 = Real('X10')
X11 = Real('X11')
X12 = Real('X12')
X13 = Real('X13')
X14 = Real('X14')

DistinctParameter = [Distinct(X0 , X1 , X2 , X3 , X4 , X5 , X6 , X7 , X8 , X9 , X10 , X11 , X12 , X13 , X14 )]

maxPossibleValue = max(InputStream)

AggregateValue = 0
for x in InputStream:
    AggregateValue = AggregateValue + float(x)

S_Con_Comparison1 = [(X0 < maxPossibleValue)] 
S_Con_Comparison2 = [(X1 < maxPossibleValue)] 
S_Con_Comparison3 = [(X2 < maxPossibleValue)] 
S_Con_Comparison4 = [(X3 < maxPossibleValue)] 
S_Con_Comparison5 = [(X4 < maxPossibleValue)] 
S_Con_Comparison6 = [(X5 < maxPossibleValue)] 
S_Con_Comparison7 = [(X6 < maxPossibleValue)] 
S_Con_Comparison8 = [(X7 < maxPossibleValue)] 
S_Con_Comparison9 = [(X8 < maxPossibleValue)] 
S_Con_Comparison10 = [(X9 < maxPossibleValue)] 
S_Con_Comparison11 = [(X10 < maxPossibleValue)] 
S_Con_Comparison12 = [(X11 < maxPossibleValue)] 
S_Con_Comparison13 = [(X12 < maxPossibleValue)] 
S_Con_Comparison14 = [(X13 < maxPossibleValue)] 
S_Con_Comparison15 = [(X14 < maxPossibleValue)] 


S_Con_Comparison = S_Con_Comparison1 + S_Con_Comparison2 + S_Con_Comparison3 + S_Con_Comparison4 + S_Con_Comparison5 + S_Con_Comparison6 + S_Con_Comparison7 + S_Con_Comparison8 + S_Con_Comparison9 + S_Con_Comparison10 + S_Con_Comparison11 + S_Con_Comparison12 + S_Con_Comparison13 + S_Con_Comparison14 + S_Con_Comparison15

S_Con = [( X0 + X1 + X2 + X3 + X4 + X5 + X6 + X7 + X8 + X9 + X10 + X11 + X12 + X13 + X14 == AggregateValue)]

Solve = S_Con + S_Con_Comparison + DistinctParameter

s = Solver()

s.add(Solve)


x = Reals('x')
i = 0 
output =[0] * len(InputStream)

if s.check() == sat:
    m = s.model()
    for d in m.decls():
        location = int((repr(d).replace("X","")))
        x=round(float(m[d].numerator_as_long())/float(m[d].denominator_as_long()),5)
        output[location]= x

print(output)

输入流的每个值都可以取自一组可能的大小为 2^25 的值。根据我的理解，找到输入流的唯一方法是对结果流进行暴力破解。鉴于这种情况，我想知道是否可以从相应的输出流对输入流进行逆向工程。

Answer 1

如评论中所述，不应将生成 真正随机 模型的任务委托给 SMT 求解器。话虽如此，您的应用程序似乎不需要这样的属性保证。

我修改了你的模型，以便强加 X_i >= 0，因为这是评论中的要求。

from z3 import *
import sys
import io
import math

def obfuscate(input_stream):
    X_list = [Real('X_{0}'.format(idx)) for idx in range(0, len(input_stream))]
    assert len(X_list) == len(input_stream)

    max_input_value = max(input_stream)
    aggregate_value = sum(input_stream)

    distinct_cs = Distinct(X_list)
    lower_cs = [(0 <= Xi) for Xi in X_list]
    upper_cs = [(Xi < max_input_value) for Xi in X_list]
    same_sum_cs = (Sum(X_list) == aggregate_value)

    s = Solver()
    s.add(distinct_cs)
    s.add(lower_cs)
    s.add(upper_cs)
    s.add(same_sum_cs)

    status = s.check()

    if status == sat:
        r_ret = []
        fp_ret = []

        m = s.model()
        for Xi in X_list:
            r_value = m.eval(Xi)
            r_ret.append(r_value)

            num = r_value.numerator_as_long()
            den = r_value.denominator_as_long()

            fp_value = round(float(num) / float(den), 5)
            fp_ret.append(fp_value)

        return input_stream, aggregate_value, "sat", r_ret, fp_ret, sum(fp_ret)

    else:
        return input_stream, aggregate_value, "unsat", None, None, None


if __name__ == '__main__':
    print("Same-value inputs are all unsat")
    print(obfuscate([0.0, 0.0, 0.0]))
    print(obfuscate([1.0, 1.0, 1.0]))
    print(obfuscate([2.0, 2.0, 2.0]))

    print("\nRe-ordering input does not change output")
    print(obfuscate([1.0, 2.0, 3.0]))
    print(obfuscate([1.0, 3.0, 2.0]))
    print(obfuscate([3.0, 2.0, 1.0]))
    print("")
    print(obfuscate([0.1, 0.0, 0.0]))
    print(obfuscate([0.0, 0.1, 0.0]))
    print(obfuscate([0.0, 0.0, 0.1]))

    print("\nSame-sum input do not necessarily map to the same outputs")
    print(obfuscate([0.1, 0.9, 2.0]))
    print(obfuscate([1.1, 0.1, 1.8]))

    print("\nSame outputs may result from different inputs")
    print(obfuscate([0.6, 1.3, 1.1]))
    print(obfuscate([1.3, 0.7, 1.0]))

输出为：

Same-value inputs are all unsat
([0.0, 0.0, 0.0], 0.0, 'unsat', None, None, None)
([1.0, 1.0, 1.0], 3.0, 'unsat', None, None, None)
([2.0, 2.0, 2.0], 6.0, 'unsat', None, None, None)

Re-ordering input does not change output
([1.0, 2.0, 3.0], 6.0, 'sat', [5/2, 11/4, 3/4], [2.5, 2.75, 0.75], 6.0)
([1.0, 3.0, 2.0], 6.0, 'sat', [5/2, 11/4, 3/4], [2.5, 2.75, 0.75], 6.0)
([3.0, 2.0, 1.0], 6.0, 'sat', [5/2, 11/4, 3/4], [2.5, 2.75, 0.75], 6.0)

([0.1, 0.0, 0.0], 0.1, 'sat', [1/30, 1/15, 0], [0.03333, 0.06667, 0.0], 0.09999999999999999)
([0.0, 0.1, 0.0], 0.1, 'sat', [1/30, 1/15, 0], [0.03333, 0.06667, 0.0], 0.09999999999999999)
([0.0, 0.0, 0.1], 0.1, 'sat', [1/30, 1/15, 0], [0.03333, 0.06667, 0.0], 0.09999999999999999)

Same-sum input do not necessarily map to the same outputs
([0.1, 0.9, 2.0], 3.0, 'sat', [4/3, 5/3, 0], [1.33333, 1.66667, 0.0], 3.0)
([1.1, 0.1, 1.8], 3.0, 'sat', [7/5, 8/5, 0], [1.4, 1.6, 0.0], 3.0)

Same outputs may result from different inputs
([0.6, 1.3, 1.1], 3.0, 'sat', [23/20, 49/40, 5/8], [1.15, 1.225, 0.625], 3.0)
([1.3, 0.7, 1.0], 3.0, 'sat', [23/20, 49/40, 5/8], [1.15, 1.225, 0.625], 3.0)

这个简单的例子让我们得出以下结论：

输出由输入值决定，但不受顺序影响
混淆过程可能对输入流的变化敏感

因此，即使 攻击者 试图使用 rainbow tables 来寻找潜在的输入 multiset 生成输出序列，他们仍然无法找到输入流中值的确切顺序。

让我们忽略构建这样的 rainbow tables 是不切实际的事实，因为可以生成大量大小为 15 的输入序列和 2^25 个候选值的池（松散的上限是 2^375），并假设我们有办法有效地访问它。

给定输出序列 O，由 obfuscate() 生成，我们可以在 rainbow table[=61] 中寻找匹配项 M =]，其中 M 是 multisets that, when used as input, would result in the same output O. Let M[i] be the i-th input set in M containing n elements, each with multiplicity m_i. Then the number of possible permutations of M[i] is (source: Wikipedia 的列表）：

在最简单的情况下，输入流中的每个值都与其他值不同，匹配 M 中的每个候选解决方案 M[i] 最多有 15! = 1.307.674.368.000 个排列. 在您的应用程序中，攻击者是否有时间尝试所有这些？

逆向工程 Z3 SMT 求解器解决方案

Reverse Engineering Z3 SMT solver solutions

reverse-engineering

smt

z3

z3py