Вопрос или проблема
Для задачи CTF мне нужно восстановить массив байтов, основываясь на нескольких ограничениях для каждого байта. Однако, поиграв немного с битовыми векторами в Z3, я заметил, что solver.check() возвращает unsat, как только я добавляю более одного ограничения. Вот пример кода для воспроизводимости:
from z3 import *
# Создаем решатель
solver = Solver()
# Объявляем битовый вектор длиной 8 бит
x = BitVec('x', 8)
# Добавляем несколько ограничений
solver.add(x >= 0) # x должно быть больше или равно 0
solver.add(x <= 128) # x должно быть меньше или равно 128
# Проверяем, удовлетворимы ли ограничения
if solver.check() == sat:
model = solver.model()
print(f'Решение найдено: x = {model[x]}')
else:
print('Решение не найдено')
В этом случае я ожидал, что битовому вектору “x” будет присвоено значение между 0 и 128. Но при выполнении этот код выдает Решение не найдено.
Я пытался отладить эту проблему, добавляя по одному ограничению за раз и проверяя их удовлетворимость (например, закомментировав либо solver.add(x >= 0), либо solver.add(x <= 128)). В результате я обнаружил, что каждое ограничение само по себе работает как и ожидалось. Однако в сочетании оба не работают, что не имеет для меня смысла.
Я также пытался найти какие-либо ответы в интернете и спрашивал ChatGPT о помощи, но даже последний не смог сказать, почему это не работает.
Обновление:
Я выяснил, что это работает, если я использую 127 в качестве верхнего предела.
Так что если я использую следующие 2 ограничения, я получаю x = 0 в качестве решения, хотя до сих пор не знаю, почему это работает только при этих условиях (если я не ошибаюсь, 8 бит должно быть достаточно, чтобы представлять значения до 255):
solver.add(x >= 0)
solver.add(x <= 127)
Операторы сравнения по умолчанию рассматривают BitVec как знаковый, т.е. 128 = −128 для этого 8-битного целого числа в дополнительном коде. (Использование любого значения меньше 128 сделает существующие ограничения знакового целого числа удовлетворимыми.)
https://ericpony.github.io/z3py-tutorial/guide-examples.htm#:~:text=Machine%20Arithmetic
В отличие от языков программирования, таких как C, C++, C#, Java, нет различия между знаковыми и беззнаковыми битовыми векторами как числами. Вместо этого Z3 предоставляет специальные знаковые версии арифметических операций, где имеет значение, рассматривается ли битовый вектор как знаковый или беззнаковый. В Z3Py операторы
<,<=,>,>=,/,%и>>соответствуют знаковым версиям. Соответствующие беззнаковые операторы – этоULT,ULE,UGT,UGE,UDiv,URemиLShR.
Используйте беззнаковые ограничения ≥/≤:
# Добавляем несколько ограничений
solver.add(UGE(x, 0)) # x должно быть больше или равно 0
solver.add(ULE(x, 128)) # x должно быть меньше или равно 128
Решение найдено: x = 128
Ответ или решение
Проблема, с которой вы столкнулись, связана с тем, как Z3 обрабатывает битовые векторы, и в частности, с тем, что операции сравнения по умолчанию трактуют битовые векторы как знаковые числа.
Когда вы объявляете битовый вектор x с размером 8 бит, он может представлять значения в диапазоне от -128 до 127, если воспринимать его как знаковый двумерный комплемент (signed two’s complement). Следовательно, когда вы добавляете условие x <= 128, Z3 интерпретирует это как x <= -128, что является противоречивым ограничением, поскольку 8-битное знаковое представление не может содержать таких значений. Именно поэтому solver.check() возвращает unsat (несовместимо).
Ваш вывод о том, что использование 127 как верхнего предела работает, связан с тем, что 127 является допустимым значением для знакового представления, и в этом случае не возникает противоречия.
Чтобы устранить эту проблему и использовать операции сравнения для беззнаковых (unsigned) битовых векторов, вам следует использовать специальные операторы, предоставляемые Z3 для работы с беззнаковыми числами. В частности, используйте операторы UGE (беззнаковое больше или равно) и ULE (беззнаковое меньше или равно). Таким образом, ваши ограничения будут выглядеть следующим образом:
from z3 import *
# Создание решателя
solver = Solver()
# Объявление беззнакового битового вектора размером 8 бит
x = BitVec('x', 8)
# Добавление нескольких ограничений с использованием беззнаковых операторов
solver.add(UGE(x, 0)) # x должно быть больше или равно 0
solver.add(ULE(x, 128)) # x должно быть меньше или равно 128
# Проверка на существование решения
if solver.check() == sat:
model = solver.model()
print(f'Найдено решение: x = {model[x]}')
else:
print('Решение не найдено')После выполнения этого кода вы должны получить корректное решение, например, x = 128. Важно помнить, что в Z3 нет строгого различия между знаковыми и беззнаковыми битовыми векторами в синтаксисе; следует различать их на уровне операций. Ваша проблема могла бы быть решена с самого начала, если бы вы использовали беззнаковые операции с самого начала.
Таким образом, для избежания путаницы и корректного решения задач, связанных с битовыми векторами, всегда обращайте внимание на трактовку знаковости и используйте соответствующие операции.