Формальная модель обнаружения программных ошибок с помощью символьного исполнения программ

Автоматическое обнаружение ошибок в программах является крайне востребованным направлением современных исследований и разработок в области обеспечения безопасности и устойчивости программного обеспечения. В рамках проекта 17-07-00702 Российского фонда фундаментальных исследований исследовались направления применения комбинированных методов анализа программ, совмещающих динамическое символьное исполнение, рандомизированное тестирование и статический анализ программ. Разработаны методы направленного анализа программ, основанные на совмещении статического анализа и динамического символьного исполнения, совмещения рандомизированного тестирования и динамического символьного исполнения программы. В данной статье рассматривается формальная модель обнаружения ошибок в программах методом символьного исполнения программ и её реализация для обнаружения ошибок выхода за границы буфера в памяти. Приводится формальная модель символьного исполнения программ, формулируется и доказывается теорема об обнаружении ошибки в программе, основанная на нарушении области определения операции вычислительной системы. Приводится описание реализации анализатора нарушения границ буфера в памяти в процессе динамического символьного исполнения программы и результаты применения реализованного прототипа анализатора на наборе программ из поставки Debian Linux, подтверждающих применимость предложенного метода обнаружения ошибок.