Как упомянуто в комментариях, решателям 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)
Этот простой пример позволяет нам сделать следующие наблюдения:
- вывод определяется значениями на входе, но это не зависит от их порядка
- процедура запутывания может быть чувствительной к изменениям во входном потоке
Поэтому, даже если злоумышленник пытается использовать радужные таблицы , чтобы найти потенциальный вход multiset , который сгенерировал выходную последовательность, они все еще не могут найти точный порядок значений во входном потоке.
Давайте не будем учитывать тот факт, что создание таких радужных таблиц нецелесообразно из-за большого количества входных последовательностей размера 15, которые могут быть сгенерированы с пулом 2^25 значения кандидата s (свободная верхняя граница будет 2^375), и предположим, что у нас есть способ получить к нему эффективный доступ.
Учитывая выходную последовательность O, сгенерированную с помощью obfuscate(), мы можем искать совпадение M внутри нашей радужной таблицы , где M - это список мультимножеств , который при использовании в качестве входных данных приведет к тому же результату O. Пусть M[i] будет i -ым входным набором в M, содержащим n элементов, каждый с кратностью m_i. Тогда число возможных перестановок M[i] равно (источник: Википедия ):
В простейшем сценарии, в котором каждое значение во входном потоке отличается от других, существует до 15! = 1.307.674.368.000 перестановок для каждого варианта решения M[i] в совпадении M. В вашем приложении у злоумышленника будет время попробовать их все?