Сделать ограничение труднее решить для решателя ограничений? - PullRequest
Новая
       75

Сделать ограничение труднее решить для решателя ограничений?

0 голосов
/ 28 января 2019

Я новичок в решении SMT, и я пишу, чтобы узнать некоторые советы и указатели, чтобы понять, что действительно является difficult constraint для решения SMT, например Z3.

Я пытался настроитьдлина битовых векторов, например, следующим образом: 

>>> a = BitVec("a", 10000)
>>> b = BitVec("b", 10000)
>>> c = a >> 18 + 6 - 32 + 69 == b <<12 + 7 * 32
>>>
>>> s = Solver()
>>> s.add(c)
>>> s.check()

Хотя интуитивно это может привести к довольно большому пространству поиска, оказывается, что Z3 все еще выполняет довольно хорошую работу и быстро ее решает,

Мне известно, что некоторые крипто-хеш-функции или математические формулы (например, гипотеза Коллатца) могут затруднить решение ограничений.Но это кажется довольно экстремальным.С другой стороны, например, предположим, что у меня есть следующее ограничение: 

a * 4 != b + 5

Как я могу усложнить решение для решателя ограничений?Есть ли общий способ сделать это?У меня сложилось впечатление, что каким-то образом это ограничение оказывается «нелинейным», тогда это сложно.Но мне все еще неясно, как это работает.

================================

Спасибо за все добрые заметки и проницательные посты.Я очень ценю это!

Итак, вот несколько предварительных тестов по предложению @ usr: 

c = BitVec("c", 256)

for i in range(0, 10):
    c = c ^ (c << 13) + 0x51D36335;

s = Solver()
s.add(c == 0xdeadbeef)
print (s.check())
print (s.model())


➜  work time python test.py
sat
[c = 37865234442889991147654282251706833776025899459583617825773189302332620431087]
python test.py  0.38s user 0.07s system 81% cpu 0.550 total

Ответы [ 2 ]

0 голосов
/ 29 января 2019

Если вы просто хотите, чтобы Z3 «работал очень усердно», вы можете попробовать факторизацию чисел, например, a * b = constant и ввести простое число или большой состав.

Или создать простую хеш-функцию и получитьpre-image:

Что я сделал, чтобы увидеть, как определяется SHA-1 .Затем я реализовал простую версию этого.SHA-1 состоит из очень простых операций, таких как shift, add, xor.Из этого шаблона вы можете создать простую хеш-функцию для тестирования.Затем вы говорите y = hash(x) && y = 0x1234, а Z3 даст вам x, который является предварительным изображением.

Для вашего развлечения я на месте создам простую хэш-функцию: 

BitVec currentValue = input;

for (i = 0 to 10)
 currentValue = currentValue ^ (currentValue <<< 13) + 0x51D36335;

BitVec hash = currentValue;

Это действительно функциональная реализация хэша (но не безопасная).Вы можете играть с операциями, количеством раундов и размером битового вектора.Вы можете утверждать hash = someConstant, чтобы получить предварительное изображение.Например, пусть Z3 даст вам input, что приведет к нулевому хешу.

Вы также можете применить более причудливые ограничения, например input == hash или hash % 1234 == 0 && hash & 0xF == 7.Z3 может удовлетворять любым условиям при наличии достаточной вычислительной мощности.

Лично я нахожу эту возможность весьма захватывающей.

0 голосов
/ 28 января 2019

логика Битвектора всегда разрешима;поэтому, в то время как все может занять много времени, z3 может решить все проблемы с битвекторами.Конечно, если размеры битовых векторов велики, то решатель может занять очень много времени или исчерпать память, прежде чем найдет решение.Умножение и криптоалгоритмы являются типичными примерами, которые всегда вызывают трудности при увеличении размеров битов.

С другой стороны, у нас возникают нелинейные целочисленные задачи.Для них нет процедуры принятия решения, и, хотя z3 «старается изо всех сил», такие проблемы обычно выходят за рамки теоретических соображений.Вы можете найти много таких примеров в сообщениях о переполнении стека.Вот самое последнее: Z3 возвращает модель, недоступную

...