[Из песочницы] Формальная верификация на примере задачи о волке, козе и капусте
На мой взгляд, в русскоязычном секторе интернета тематика формальной верификации освещена недостаточно, и особенно не хватает простых и наглядных примеров.
Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.
Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.
Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.
Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.
В случае невозможности нахождения ответа, зачастую можно переработать неясные места программы, уменьшив их алгоритмическую сложность, для того чтобы получить конкретный ответ да либо нет.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.
А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.
Задача о 8 ферзях (Взята из англоязычного мануала).
Читать дальше →
Я приведу такой пример из зарубежного источника, и дополню собственным решением известной задачи о переправе волка, козы и капусты на другую сторону реки.
Но вначале вкратце опишу, что из себя представляет формальная верификация и зачем она нужна.
Под формальной верификацией обычно понимают проверку одной программы либо алгоритма с помощью другой.
Это нужно для того, чтобы удостовериться, что поведение программы соответствует ожидаемому, а также обеспечить её безопасность.
Формальная верификация является самым мощным средством поиска и устранения уязвимостей: она позволяет найти все существующие дыры и баги в программе, либо же доказать, что их нет.
Стоит заметить, что в некоторых случаях это бывает невозможно, как например, в задаче о 8 ферзях с шириной доски 1000 клеток: всё упирается в алгоритмическую сложность либо проблему остановки.
Однако в любом случае будет получен один из трёх ответов: программа корректна, некорректна, или же — вычислить ответ не удалось.
В случае невозможности нахождения ответа, зачастую можно переработать неясные места программы, уменьшив их алгоритмическую сложность, для того чтобы получить конкретный ответ да либо нет.
А применяется формальная верификация, например, в ядре Windows и операционных системах беспилотников Darpa, для обеспечения максимального уровня защиты.
Мы будем использовать Z3Prover, очень мощный инструмент для автоматизированного доказательства теорем и решения уравнения.
Причём Z3 именно решает уравнения, а не подбирает их значения грубым брутфорсом.
Это означает, что он способен находить ответ, даже в случаях когда комбинаций входных вариантов и 10^100.
А ведь это всего лишь около дюжины входных аргументов типа Integer, и подобное зачастую встречается на практике.
Задача о 8 ферзях (Взята из англоязычного мануала).
Читать дальше →
Источник: Хабрахабр
Похожие новости
- [Перевод] Обход двухфакторной аутентификации в публичной баг-баунти программе: путь к $6000
- Кратко про XHTTP для VLESS: что, зачем и как
- [Перевод] Как я нашёл уязвимость в ядре Linux при помощи модели o3
- SelfCoerce для локального повышения привилегий на Windows 10
- Теория мертвого 2GIS
- Постквантовые криптостандарты США на алгоритмы электронной подписи на основе хеш-функций с сохранением состояния
- Новые возможности менеджера секретов Deckhouse Stronghold: пространства имён, резервные копии и репликация данных
- [Перевод] Single Sign-On c OpenAM и OpenIG: практические примеры реализации
- Безопасность по ГОСТу: процесс интеграции HSM отечественного производства
- Каких коммуникаторов не хватает PR-индустрии?