逆向工程 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

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

---

我修复了你的模型以强制使用X_i >= 0，因为这是 cmets 的要求。

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)

这个简单的例子让我们可以进行以下观察：

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

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

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

给定一个由obfuscate() 生成的输出序列O，我们可以在我们的彩虹表 中寻找匹配M，其中M 是multisets 的列表，当用作输入时，将产生相同的输出O。让M[i] 成为M 中的i-th 输入集，其中包含n 元素，每个元素都具有多重性m_i。那么M[i]的可能排列数为（来源：Wikipedia）：

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