ПРИМЕНЕНИЕ SMT-РЕШАТЕЛЕЙ В ВЕРИФИКАЦИИ ПРОГРАММНОГО ОБЕСПЕЧЕНИЯ

APPLICATION OF SMT SOLVERS IN SOFTWARE VERIFICATION

Darya Aksenova

student, Department of Informatics and Computer Science, Povolzhskiy State University of Telecommunications and Informatics

Russia, Samara

АННОТАЦИЯ

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

ABSTRACT

Software verification is an important component to ensure its reliability, security and correct operation. This paper applies SMT solvers to various areas of static software verification, including program model checking, static analysis, and deductive verification. Particular attention is paid to the use of SMT solutions to find errors and inconsistencies in program code, as well as formal verification of program models.

Ключевые слова: Верификация программного обеспечения, SMT-решатели, статическая верификация, проверка моделей программ, дедуктивная верификация, формальная верификация.

Keywords: Software verification, SMT software solvers, static verification, program model checking, deductive verification, formal verification.

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

Задача SMT (Satisfiability Modulo Theories) — одна из классических задач математической логики, представляющая собой задачу разрешимости логической формулы в логике первого порядка при наличии в ней предикатов, использующих дополнительные теории. Широкое использование SMT в различных областях информатики связано с тем, что она является одной из наиболее изученных NP-полных задач и, в то же время, достаточно удобной для формализации и сведения к ней других вычислительных задач. Это привело к активной разработке различных средств решения задачи SMT, SMT решателей, предоставляющих эффективные способы ее решения. В общем случае решение задачи SMT за приемлемое время является невозможным, но результаты исследований последних лет говорят о возможности эффективного решения достаточно широкого класса практически интересных подмножеств SMT.

Решатели логических формул в теориях широко используются во всех рассмотренных группах инструментов статической верификации, кроме реализаций языков с зависимыми типами и инструментов интерактивного доказательства теорем. В инструментах проверки моделей программ (англ. software model checkers) решатели формул в теориях используются для поиска контрпримеров во всем пространстве состояний модели, представленном в виде логической формулы, проверки осуществимости трасс выполнения, ведущих к ошибочным состояниям, автоматического построения предикатных абстракций и т.д.

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

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

SMT-решатели могут использоваться для поиска ошибок и несоответствий в программном коде. Например, они могут проверять наличие недостижимых участков кода, проверять правильность использования указателей или выявлять некорректные операции с данными. Проверка моделей программ с использованием SMT позволяет формально анализировать и верифицировать модели программ на соответствие некоторым свойствам или спецификациям. В этом контексте SMT-решатели играют ключевую роль, поскольку они специализированы на решении проблем удовлетворимости модулей теорий. Сначала необходимо сформулировать модель программы в виде логических формул. Это может включать в себя описание состояний программы, операций и переходов между состояниями, а также спецификации требований или свойств, которым должна удовлетворять модель. Затем модель программы переводится в логическую форму, которая состоит из набора утверждений или формул в логике высказываний или предикатной логике. После этого SMT-решатель используется для проверки удовлетворимости логической формулы, которая представляет модель программы. SMT-решатель пытается найти значения переменных, при которых формула является истинной (удовлетворимой). В зависимости от результата решения SMT-решателя, можно делать выводы о корректности модели программы. Если формула удовлетворима, то модель программы удовлетворяет своим спецификациям. В противном случае, если формула не удовлетворима, это указывает на наличие ошибок или несоответствий в модели.

Список литературы:

1. Шарков, В. В. (2015). Статический анализ и верификация программного обеспечения. СПб.: БХВ-Петербург. 44-59 с.
2. Джексон, Д. (2015). Верификация и тестирование программного обеспечения. СПб.: Символ-Плюс.17-21 с.
3. Мошков, М. Ю., & Мошков, С. В. (2017). Введение в SMT-решатели. Труды Института системного программирования РАН, 29(4), 97-108 с.