Transcript
Краткое введение в SAT/SMT-солверы и символьное исполнение Денис Юричев dennis(a)yurichev.com Декабрь 2015 май 2017 Содержание 1 Это черновик! 3 2 Благодарности 3 3 Введение 3 4 Это хайп? Очередная мода? 4 5 SMT 1 -солверы Система уравнений уровня школы Еще одна система уравнений уровня школы Связь между SAT 2 и SMT солверами Головоломка зебры (AKA 3 Загадка Эйнштейна) Головоломка Судоку Первая идея Вторая идея Вывод Домашная работа Дальнейшее чтение Судоку как SAT-проблема Решение Problem Euler 31: Coin sums Использование доказывателя теорем Z3 для доказательства эквивалентности одной странной альтернативы XOR В виде SMT-LIB Используя универсальный квантификатор Как работает это выражение Формула Dietz-а Взлом LCG 4 при помощи Z Решение головоломки трубы используя Z3 SMT-солвер Создание Решение Взлом Сапёра при помощи Z3 SMT-солвера Метод Код Пересчет упрощенной электронной таблицы используя Z3Py Unsat core Нагрузочное тестирование Файлы Satisfiability modulo theories 2 Boolean satisfiability problem 3 Also Known As 4 Linear congruential generator 1 6 Синтез программы Синтез простой программы используя Z Некоторые замечания Код Донгла Rockey: поиск неизвестного алгоритма используя только входные/выходные пары Вывод Файлы Дальнейшая работа Игрушечный декомпилятор Введение Структура данных Простые примеры Работа с оптимизациями компилятора Деление используя умножение Обфускация/деобфускация Тесты Вычисление выражения Использование Z3 SMT-солвера для тестирования Мои другие реализации игрушечного декомпилятора Даже еще более простой игрушечный декомпилятор Разница между игрушечным декомпилятором и коммерческим Дальнейшее чтение Файлы Символьное исполнение Символьные вычисления Дробный (rational) тип данных Символьное исполнение (symbolic execution) Обмен значений используя исключающее ИЛИ Смена порядка байт (endianness) Быстрое преобразование Фурье Циклический избыточный код (CRC 5 ) Линейный конгруэнтный генератор Констрайнт пути (path constraint) Деление на ноль Сортировка слиянием (merge sort) Расширение класса Expr Вывод Дальнейшее чтение KLEE Инсталляция Школьное уравнение Головоломка зебры Судоку Unit-тест: цвет в HTML/CSS Unit-тест: ф-ция strcmp() Дата и время в UNIX Обратная ф-ция base64-декодера CRC (Циклический избыточный код) Пример изменения буфера # Пример изменения буфера # Восстановление входного буфера для заданного значения CRC В сравнении с другими алгоритмами хэширования Декомпрессор LZSS strtodx() из RetroBSD Unit-тестирование: простой калькулятор Регулярные выражения Cyclic redundancy check 2 9.14Упражнение (Любительская) криптография Серьезная криптография Попытки взлома серьезных шифров Любительская криптография Ошибки XOR-шифры Другие особенности Примеры Пример: простая хэш-функция Ручная декомпиляция Попробуем Z SAT-солверы CNF форма Пример: двухбитный сумматор MiniSat CryptoMiniSat Взлом Сапёра при помощи SAT Простая ф-ция подсчета бит (population count) Сапёр Игра Жизнь Конвея Откатывание состояния игры Жизнь назад Поиск натюрмортов Исходный код Acronyms used Это черновик! Это еще пока ранний черновик, но всё же может быть кому-то интересен. Последняя версия всегда доступна на Англоязычная версия: Версия этого текста: 8 мая 2017 г.. Для получения новостей об обновлениях, можете подписаться на мой twitter 6, facebook 7, или репозиторий на github Благодарности Leonardo de Moura и Nikolaj Bjorner, за помощь. 3. Введение SAT/SMT солверы можно рассматривать как солверы огромных систем уравнений. Разница в том, что SMT-солверы берут системы в произвольном формате, в то время как SAT-солверы ограничены булевыми уравнениями вида CNF 9. Огромное количество проблем их практики можно представить как проблемы решения систем уравнений. 6 https://twitter.com/yurichev 7 https://www.facebook.com/dennis.yurichev.5 8 https://github.com/dennis714/sat_smt_article 9 Conjunctive normal form 3 4. Это хайп? Очередная мода? Некоторые люди говорят, что это очередной хайп. Нет, SAT достаточно стар, чтобы быть фундаментальным в CS 10. Причина повышенного интереса в том, что компьютеры стали работать быстрее, так что теперь больше попыток решать старые проблемы используя SAT/SMT, которые раннее были недоступны. 5. SMT-солверы 5.1. Система уравнений уровня школы Я скопипастил эту школьную систему уравнений из Wikipedia: 11 : Можно ли её решить используя Z3? Вот: #!/usr/bin/python from z3 import * x = Real('x') y = Real('y') z = Real('z') s = Solver() s.add(3*x + 2*y z == 1) s.add(2*x 2*y + 4*z == 2) s.add( x + 0.5*y z == 0) print s.check() print s.model() После запуска, увидим: sat [z = 2, y = 2, x = 1] 3x + 2y z = 1 2x 2y + 4z = 2 x y z = 0 Если мы изменим любое уравнение так, что оно не будет иметь решений, s.check() вернет unsat. Я использовал Real sort (что-то вроде типа данных в SMT-солверах) потому что последнее выражение равно 1 2, что, само собой, вещественное число. Для целочисленной системы уравнений, подойдет Int sort. Питоновский интерфейс (как и для других высокоуровневых ЯП вроде C#) очень популярен, потому что практичен, но на самом деле, имеется стандартный язык для SMT-солверов называющийся SMT- LIB 12. Наш пример переписанный на него выглядит так: (declare const x Real) (declare const y Real) (declare const z Real) (assert (=( (+(* 3 x) (* 2 y)) z) 1)) (assert (=(+( (* 2 x) (* 2 y)) (* 4 z)) 2)) (assert (=( (+ ( 0 x) (* 0.5 y)) z) 0)) (check sat) (get model) Этот язык очень близок к LISP-у, но для нетренированных глаз читать тяжеловато. Запускаем: % z3 smt2 example.smt sat (model (define fun z () Real ( 2.0)) 10 Computer science 11 https://en.wikipedia.org/wiki/system_of_linear_equations 12 4 ) (define fun y () Real ( 2.0)) (define fun x () Real 1.0) Так что когда вы вернетесь к Питоновскому коду, вы можете подумать, что эти 3 выражения могут быть исполнены. Это не так: Z3Py API предлагает перегруженные операторы, так что выражения конструируются и передаются внутрь Z3 без исполнения 13. Я бы назвал это встроенным DSL 14. Та же история и для Z3 C++ API, вы можете найти там объявления operator+ и многих других 15. Z3 API 16 для Java, ML и.net также существуют 17. Краткое введение в Z3Py: https://github.com/ericpony/z3py-tutorial. Введение в Z3, использующее язык SMT-LIB: Еще одна система уравнений уровня школы Я нашел это где-то в Фейсбуке: Её легко решить при помощи Z3: #!/usr/bin/python from z3 import * Рис. 1: Система уравнений circle, square, triangle = Ints('circle square triangle') s = Solver() s.add(circle+circle==10) s.add(circle*square+square==12) s.add(circle*square triangle*circle==circle) print s.check() print s.model() sat [triangle = 1, square = 2, circle = 5] 5.3. Связь между SAT и SMT солверами Ранние SMT-солверы были фронтендами для SAT-солверов, т.е., они транслировали SMT выражения в CNF и подавали их на вход SAT-солверу. Процесс трансляции иногда называется bit blasting. Некоторые SMT-солверы до сих пор так и работают: STP использует MiniSAT или CryptoMiniSAT как бакэнд. 13 https://github.com/z3prover/z3/blob/6e852762baf568af2aad1e35019fdf41189e4e12/src/api/python/z3.py 14 Domain-specific language 15 https://github.com/z3prover/z3/blob/6e852762baf568af2aad1e35019fdf41189e4e12/src/api/c%2b%2b/z3%2b%2b.h 16 Application programming interface 17 https://github.com/z3prover/z3/tree/6e852762baf568af2aad1e35019fdf41189e4e12/src/api 5 Некоторые другие SMT-солверы более продвинутые (как Z3), так что они используют что-то более сложное Головоломка зебры (AKA Загадка Эйнштейна) Головоломка зебры это популярная головоломка, определяется так: 1. На улице стоят пять домов. 2. Англичанин живёт в красном доме. 3. У испанца есть собака. 4. В зелёном доме пьют кофе. 5. Украинец пьёт чай. 6. Зелёный дом стоит сразу справа от белого дома. 7. Тот, кто курит Old Gold, разводит улиток. 8. В жёлтом доме курят Kool. 9. В центральном доме пьют молоко. 10. Норвежец живёт в первом доме. 11. Сосед того, кто курит Chesterfield, держит лису. 12. В доме по соседству с тем, в котором держат лошадь, курят Kool. 13. Тот, кто курит Lucky Strike, пьёт апельсиновый сок. 14. Японец курит Parliament. 15. Норвежец живёт рядом с синим домом. Кто пьёт воду? Кто держит зебру? В целях ясности следует добавить, что каждый из пяти домов окрашен в свой цвет, а их жители разных национальностей, владеют разными животными, пьют разные напитки и курят разные марки американских сигарет. Ещё одно замечание: в утверждении 6 справа означает справа относительно вас. ( (Wikipedia) ) Это очень хороший пример CSP 18. Мы можем закодировать каждый объект как целочисленную переменную, определяющую номер дома. Тогда, чтобы определить, что англичанин живет в крамном доме, мы добавим этот констрайнт: Englishman == Red, означающий, что номер дома, где живет англичанин, и номер дома окрашенный в красный один и тот же. Мы определяем что норвежец живет в соседнем доме с синим домом, но мы точно не знаем, слева от синего дома, или справа, но мы знаем что номер дома будет отличается на 1. Так что определим такой констрайнт: Norwegian==Blue-1 OR Norwegian==Blue+1. Также нужно ограничить номера всех домов, чтобы они были в пределах Мы также будем использовать Distinct, чтобы показать, что все различные объекты одного типа должны находиться в домах с разными номерами. #!/usr/bin/env python from z3 import * Yellow, Blue, Red, Ivory, Green=Ints('Yellow Blue Red Ivory Green') Norwegian, Ukrainian, Englishman, Spaniard, Japanese=Ints('Norwegian Ukrainian Englishman Spaniard Japanese') Water, Tea, Milk, OrangeJuice, Coffee=Ints('Water Tea Milk OrangeJuice Coffee') Kools, Chesterfield, OldGold, LuckyStrike, Parliament=Ints('Kools Chesterfield OldGold LuckyStrike Parliament') Fox, Horse, Snails, Dog, Zebra=Ints('Fox Horse Snails Dog Zebra') s = Solver() # colors are distinct for all 5 houses: s.add(distinct(yellow, Blue, Red, Ivory, Green)) 18 Constraint satisfaction problem 6 # all nationalities are living in different houses: s.add(distinct(norwegian, Ukrainian, Englishman, Spaniard, Japanese)) # so are beverages: s.add(distinct(water, Tea, Milk, OrangeJuice, Coffee)) # so are cigarettes: s.add(distinct(kools, Chesterfield, OldGold, LuckyStrike, Parliament)) # so are pets: s.add(distinct(fox, Horse, Snails, Dog, Zebra)) # limits. # adding two constraints at once (separated by comma) is the same # as adding one And() constraint with two subconstraints s.add(yellow =1, Yellow =5) s.add(blue =1, Blue =5) s.add(red =1, Red =5) s.add(ivory =1, Ivory =5) s.add(green =1, Green =5) s.add(norwegian =1, Norwegian =5) s.add(ukrainian =1, Ukrainian =5) s.add(englishman =1, Englishman =5) s.add(spaniard =1, Spaniard =5) s.add(japanese =1, Japanese =5) s.add(water =1, Water =5) s.add(tea =1, Tea =5) s.add(milk =1, Milk =5) s.add(orangejuice =1, OrangeJuice =5) s.add(coffee =1, Coffee =5) s.add(kools =1, Kools =5) s.add(chesterfield =1, Chesterfield =5) s.add(oldgold =1, OldGold =5) s.add(luckystrike =1, LuckyStrike =5) s.add(parliament =1, Parliament =5) s.add(fox =1, Fox =5) s.add(horse =1, Horse =5) s.add(snails =1, Snails =5) s.add(dog =1, Dog =5) s.add(zebra =1, Zebra =5) # main constraints of the puzzle: # 2.The Englishman lives in the red house. s.add(englishman==red) # 3.The Spaniard owns the dog. s.add(spaniard==dog) # 4.Coffee is drunk in the green house. s.add(coffee==green) # 5.The Ukrainian drinks tea. s.add(ukrainian==tea) # 6.The green house is immediately to the right of the ivory house. s.add(green==ivory+1) # 7.The Old Gold smoker owns snails. s.add(oldgold==snails) # 8.Kools are smoked in the yellow house. s.add(kools==yellow) # 9.Milk is drunk in the middle house. s.add(milk==3) # i.e., 3rd house # 10.The Norwegian lives in the first house. s.add(norwegian==1) # 11.The man who smokes Chesterfields lives in the house next to the man with the fox. 7 s.add(or(chesterfield==fox+1, Chesterfield==Fox 1)) # left or right # 12.Kools are smoked in the house next to the house where the horse is kept. s.add(or(kools==horse+1, Kools==Horse 1)) # left or right # 13.The Lucky Strike smoker drinks orange juice. s.add(luckystrike==orangejuice) # 14.The Japanese smokes Parliaments. s.add(japanese==parliament) # 15.The Norwegian lives next to the blue house. s.add(or(norwegian==blue+1, Norwegian==Blue 1)) # left or right r=s.check() print r if r==unsat: exit(0) m=s.model() print(m) Запускаем и получаем корректный результат: sat [Snails = 3, Blue = 2, Ivory = 4, OrangeJuice = 4, Parliament = 5, Yellow = 1, Fox = 1, Zebra = 5, Horse = 2, Dog = 4, Tea = 2, Water = 1, Chesterfield = 2, Red = 3, Japanese = 5, LuckyStrike = 4, Norwegian = 1, Milk = 3, Kools = 1, OldGold = 3, Ukrainian = 2, Coffee = 5, Green = 5, Spaniard = 4, Englishman = 3] 5.5. Головоломка Судоку Головоломка Судоку это решетка 9*9, некоторые ячейки заполнены значениями, некоторые пустые: 8 Нерешенная Судоку Числа в каждом ряду должны быть уникальными, т.е., каждый ряд должен содержать 9 чисел в пределах 1..9 без повторений. Та же история и для каждого столбца и каждого квадрата 3*3. Головоломка представляет собой хороший кандидат, на котором можно попробовать SMT-солвер, потому что это, в общем-то, просто нерешенная система уравнений Первая идея Всё что нужно решить, это как определять в одном выражении, содержат ли 9 переменных все 9 уникальных чисел? Они ведь не упорядочены и не отсортированы, все-таки. Из школьной арифметики, мы можем найти такую идею: 10 i i i 9 = (1) }{{} 9 Берете каждую входную переменную, вычисляете 10 i и суммируете. Если все входные значения уникальны, каждая найдет свое собственное место. И даже более того: не будет дыр, т.е., не будет пропущенных значений. Так что, в случае Судоку, число будет конечным результатом, означающим, что все входные 9 переменных уникальны, в пределах Возведение в степень это тяжелая операция, можно ли использовать двоичные операции? Да, просто замените 10 на 2: 2 i i i 9 = }{{} 2 (2) 9 Эффект тот же, но результат будет в двоичной системе а не в десятичной. Вот рабочий пример: import sys from z3 import * coordinates: s=solver() 9 # using Python list comprehension, construct array of arrays of BitVec instances: cells=[[bitvec('cell%d%d' % (r, c), 16) for c in range(9)] for r in range(9)] # # news/worlds hardest sudoku can you puzzle= # process text line: current_column=0 current_row=0 for i in puzzle: if i!='.': s.add(cells[current_row][current_column]==bitvecval(int(i),16)) current_column=current_column+1 if current_column==9: current_column=0 current_row=current_row+1 one=bitvecval(1,16) mask=bitvecval(0b ,16) # for all 9 rows for r in range(9): s.add(((one cells[r][0]) + (one cells[r][1]) + (one cells[r][2]) + (one cells[r][3]) + (one cells[r][4]) + (one cells[r][5]) + (one cells[r][6]) + (one cells[r][7]) + (one cells[r][8]))==mask) # for all 9 columns for c in range(9): s.add(((one cells[0][c]) + (one cells[1][c]) + (one cells[2][c]) + (one cells[3][c]) + (one cells[4][c]) + (one cells[5][c]) + (one cells[6][c]) + (one cells[7][c]) + (one cells[8][c]))==mask) # enumerate all 9 squares for r in range(0, 9, 3): for c in range(0, 9, 3): # add constraints for each 3*3 square: s.add((one cells[r+0][c+0]) + (one cells[r+0][c+1]) + (one cells[r+0][c+2]) + (one cells[r+1][c+0]) + (one cells[r+1][c+1]) + (one cells[r+1][c+2]) + (one cells[r+2][c+0]) + (one cells[r+2][c+1]) + (one cells[r+2][c+2])==mask) #print s.check() s.check() #print s.model() m=s.model() for r in range(9): for c in range(9): sys.stdout.write (str(m[cells[r][c]])+ ) print ( https://github.com/dennis714/sat_smt_article/blob/master/smt/sudoku_plus.py ) % time python sudoku_plus.py real user sys 0m11.717s 0m10.896s 0m0.068s И даже более того, можно заменить суммирование на логическое ИЛИ: import sys from z3 import * coordinates: s=solver() 2 i 1 2 i 2 2 i 9 }{{} = (3) 9 # using Python list comprehension, construct array of arrays of BitVec instances: cells=[[bitvec('cell%d%d' % (r, c), 16) for c in range(9)] for r in range(9)] # # news/worlds hardest sudoku can you puzzle= # process text line: current_column=0 current_row=0 for i in puzzle: if i!='.': s.add(cells[current_row][current_column]==bitvecval(int(i),16)) current_column=current_column+1 if current_column==9: current_column=0 current_row=current_row+1 one=bitvecval(1,16) mask=bitvecval(0b ,16) # for all 9 rows for r in range(9): s.add(((one cells[r][0]) (one cells[r][1]) (one cells[r][2]) (one cells[r][3]) (one cells[r][4]) (one cells[r][5]) (one cells[r][6]) (one cells[r][7]) (one cells[r][8]))==mask) # for all 9 columns for c in range(9): s.add(((one cells[0][c]) (one cells[1][c]) 11 (one cells[2][c]) (one cells[3][c]) (one cells[4][c]) (one cells[5][c]) (one cells[6][c]) (one cells[7][c]) (one cells[8][c]))==mask) # enumerate all 9 squares for r in range(0, 9, 3): for c in range(0, 9, 3): # add constraints for each 3*3 square: s.add(one cells[r+0][c+0] one cells[r+0][c+1] one cells[r+0][c+2] one cells[r+1][c+0] one cells[r+1][c+1] one cells[r+1][c+2] one cells[r+2][c+0] one cells[r+2][c+1] one cells[r+2][c+2]==mask) #print s.check() s.check() #print s.model() m=s.model() for r in range(9): for c in range(9): sys.stdout.write (str(m[cells[r][c]])+ ) print ( https://github.com/dennis714/sat_smt_article/blob/master/smt/sudoku_or.py ) Теперь работает намного быстрее. Наверное, Z3 лучше поддерживает операцию ИЛИ над битовыми векторами, чем сложение? % time python sudoku_or.py real user sys 0m1.429s 0m1.393s 0m0.036s Головоломка, которую я использовал как пример, известна как самая трудная из известных 19 (по крайней мере для людей). Для решения понадобилось 1.4 секунды на моем ноутбуке Intel Core i3-3110m 2.4GHz Вторая идея Мой первый подход далек от эффективного, я сделал то что первым пришло в голову, и оно заработало. Другой подход это использовать команду distinct в SMTLIB, которая говорит Z3, что некоторые переменные должны быть отличны друг от друга (или уникальны). Эта команда также имеется в питоновском интерфейсе к Z3. Я переписал мой первый солвер Судоку, теперь он работает над sort-ом Int, и имеет команды distinct вместо битовых операций, и еще один констрайнт добавлен: значение каждой ячейки должно быть в пределах 1..9, потому что, иначе, Z3 предложит (хотя и корректное) решение с очень большими и/или отрицательными числами. import sys from z3 import * s=solver() # using Python list comprehension, construct array of arrays of BitVec instances: cells=[[int('cell%d%d' % (r, c)) for c in range(9)] for r in range(9)] # # news/worlds hardest sudoku can you puzzle= # process text line: current_column=0 current_row=0 for i in puzzle: if i!='.': s.add(cells[current_row][current_column]==int(i)) current_column=current_column+1 if current_column==9: current_column=0 current_row=current_row+1 # this is important, because otherwise, Z3 will report correct solutions with too big and/or negative numbers in cells for r in range(9): for c in range(9): s.add(cells[r][c] =1) s.add(cells[r][c] =9) # for all 9 rows for r in range(9): s.add(distinct(cells[r][0], cells[r][1], cells[r][2], cells[r][3], cells[r][4], cells[r][5], cells[r][6], cells[r][7], cells[r][8])) # for all 9 columns for c in range(9): s.add(distinct(cells[0][c], cells[1][c], cells[2][c], cells[3][c], cells[4][c], cells[5][c], cells[6][c], cells[7][c], cells[8][c])) # enumerate all 9 squares for r in range(0, 9, 3): for c in range(0, 9, 3): # add constraints for each 3*3 square: s.add(distinct(cells[r+0][c+0], cells[r+0][c+1], cells[r+0][c+2], cells[r+1][c+0], cells[r+1][c+1], 13 cells[r+1][c+2], cells[r+2][c+0], cells[r+2][c+1], cells[r+2][c+2])) #print s.check() s.check() #print s.model() m=s.model() for r in range(9): for c in range(9): sys.stdout.write (str(m[cells[r][c]])+ ) print ( https://github.com/dennis714/sat_smt_article/blob/master/smt/sudoku2.py ) % time python sudoku2.py real user sys 0m0.382s 0m0.346s 0m0.036s Это намного быстрее Вывод SMT-солверы настолько удобны, что в нашем солвере Судоку нет ничего больше ничего, мы просто определили отношения между
