逆向工程Z3 SMT求解器解决方案
逆向工程Z3 SMT求解器解决方案
提问于 2020-03-26 16:50:59
在一定的约束条件下，我使用Z3 SMT求解器从给定的向量中生成一组新的随机数。我这样做是为了隐藏我的输入流。相应的代码可以在下面找到：
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的可能集中获取输入流的每个值。根据我的理解，找到输入流的唯一方法是对结果流执行蛮力。在这种情况下，我想知道是否可以从相应的输出流反向工程输入流。
回答 1
Stack Overflow用户
回答已采纳
发布于 2020-03-27 12:55:04
正如评论中提到的，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)通过这个简单的例子，我们可以进行以下观察：
- 输出由输入中的值决定，但不受其顺序的影响。
- 混淆过程可能对输入流中的变化很敏感。
因此，即使攻击者试图使用彩虹表来查找生成输出序列的潜在输入多集，他们仍然无法找到输入流中值的确切顺序。
让我们忽略这样一个事实，即构建这样的彩虹表是不切实际的，因为大量的大小为15的输入序列可以用一个2^25候选值池生成(一个松散的上限是2^375)，并且假设我们有一种有效访问它的方法。
给定用O生成的输出序列obfuscate()，我们可以在彩虹表中查找匹配的M，其中M是一个多集列表，当用作输入时，会产生相同的输出O。让M[i]是包含n元素的M中的i-th输入集，每个元素都具有多重性m_i。那么M[i]的可能排列数是(来源：维基百科)：
在最简单的场景中，输入流中的每个值都与其他值不同，在match M中，每个候选解决方案M[i]都有最多的M排列。在您的应用程序中，攻击者是否有时间尝试所有这些？
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/60872189
复制相关文章
相似问题
腾讯云开发者
Copyright © 2013 - 2026 Tencent Cloud. All Rights Reserved. 腾讯云 版权所有
深圳市腾讯计算机系统有限公司 ICP备案/许可证号：粤B2-20090059 
粤公网安备44030502008569号
腾讯云计算（北京）有限责任公司 京ICP证150476号 | 京ICP备11018762号