Рубрика «z3»

Преамбула

image

"Человеческий мозг это пустой чердак. Дурак так и делает: тащит туда нужное и не нужное. И наконец наступает момент, когда самую необходимую вещь туда не запихнешь, или наоборот не достанешь..."

В.Б. Ливанов (из к/ф "Шерлок Холмс и доктор Ватсон")

Данное руководство не охватывает весь функционал SMT решателя. Оно написано для таких ситуаций, когда человеку срочно нужно вспомнить, подсмотреть как реализовать ту или иную его идею, не тратя много времени на поиск информации, отладку и т.д. Иными словами это руководство — шпаргалка, затрагивающая лишь часто применяемое.

Читать полностью »

Во втором туре выборов губернатора Приморского края 16 сентября 2018 года встречались действующий и.о. губернатора Андрей Тарасенко и занявший второе место в первом туре коммунист Андрей Ищенко. В ходе подсчета голосов на сайте ЦИК РФ отображалась информационная панель с растущим числом обработанных протоколов и голосов за кандидатов.

Публикация подробных данных по участкам на официальном сайте ЦИК www.izbirkom.ru замерла после ввода 1484 (95.74%) протоколов и не возобновлялась до самого конца. Поэтому когда в трансляции лидер голосования вдруг поменялся с Ищенко на Тарасенко, было неясно, как именно это могло произойти. В СМИ просто писали «после обработки 99,03% протоколов лидер сменился».

Однако, располагая промежуточными суммарными данными из информационной панели, с помощью простой математики и программирования можно подробно установить, что именно происходило с протоколами в ночь после выборов. Используем Python, Colab от Google и Z3 theorem prover от Microsoft Research. Ну и добьём всё обычной дедукцией.

Математическое расследование, как подделывали выборы губернатора в Приморье 16 сентября 2018 года - 1
Читать полностью »

На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.

Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.

Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.

Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.

Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.

Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.

Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.

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

А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.

Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.

Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.

А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.

Задача о 8 ферзях (Взята из англоязычного мануала).

Формальная верификация на примере задачи о волке, козе и капусте - 1
Читать полностью »

На Software Engineering Stack Exchange я увидел такой вопрос: «Что мешает широкому внедрению формальных методов?» Вопрос был закрыт как предвзятый, а большинство ответов представляли собой комментарии типа «Слишком дорого!!!» или «Сайт — это не самолёт!!!» В каком-то смысле это верно, но мало что объясняет. Я написал эту статью, чтобы дать более широкую историческую картину формальных методов (FM), почему они на самом деле не используются и что мы делаем для исправления ситуации.

Прежде чем начать, нужно сформулировать некоторые условия. На самом деле существует не так много формальных методов: всего несколько крошечных групп. Это означает, что разные группы по-разному применяют термины. В широком смысле есть две группы формальных методов: формальная спецификация изучает запись точных, однозначных спецификаций, а формальная проверка — методы доказательства. Сюда входят и код, и абстрактные системы. Мало того, что мы используем разные термины для кода и систем, мы часто используем разные инструменты для их верификации. Чтобы ещё больше всё запутать, если кто-то говорит, что создаёт формальную спецификацию, обычно это означает и верификацию дизайна. А если кто-то говорит, что делает формальную верификацию, обычно это относится к верификации кода.
Читать полностью »

Triton vs Kao’s Toy Project. Продолжаем хорошую традицию - 1

В данной статье речь пойдет про SMT-решатели. Так сложилось, что в исследовательских материалах, посвященных данной теме, появилась хорошая традиция. Уже несколько раз в качестве подопытного алгоритма для SMT-решателей разные исследователи выбирали один и тот же пример – крякми, придуманное некогда человеком с ником kao. Что ж, продолжим эту традицию и попробуем использовать для решения этого крякми еще один инструмент для символьных вычислений – Triton.

Читать полностью »


https://ajax.googleapis.com/ajax/libs/jquery/3.4.1/jquery.min.js