Разработка и исследование синтетического метода верификации программы с помощью SMT-решателей

Разработка и исследование синтетического метода верификации программы…

ISSN 0236-3933. Вестник МГТУ им. Н.Э. Баумана. Сер. Приборостроение. 2016. № 4







 



 





: 4

\ ,

m if i

then m k k else m k k m

pc m pc m same V k i



 





    

  



 



 





\ ,

b pc m pc m same V k i

      









*2,

m k k m m k k m



  



Поиск контрпримера осуществляется в соответствии со следующими пра-

вилами:

– с помощью конъюнкции к сумме предикатов переходов программы до-

бавляем отрицание проверяемого условия









;

Programm

Condition

   

R R R

– анализ программы с помощью SMT-решателя;

SMT-решатель строит модель данных, на которых проверяемое условие не-

выполнимо.

Анализ инварианта программы с помощью SMT-решателя.

SMT — это

задача разрешимости для логических формул с учетом лежащих в их основе

теорий: SMT-формула — это формула в логике первого порядка, где функции и

предикатные символы имеют дополнительную интерпретацию, основной ее за-

дачей является возможность определения выполнимости или невыполнимости

этой формулы. Формула содержит произвольные переменные, а предикатами

являются булевы функции от этих переменных. SMT включает в себя теорию

массивов и списков и теорию битовых секторов. Также решатель обеспечивает

поиск уязвимостей, генерацию эксплойтов, анализ механизмов защиты и гене-

рацию полезной нагрузки.

SMT-решатели — это алгоритмы, которые принимают на выход задачу раз-

решимости (вопрос, сформулированный в рамках какой-либо формальной си-

стемы и требующий ответа «Да» или «Нет»), выдают на выходе соответствую-

щий корректный результат. Задача или вопрос представляют собой некую логи-

ческую формулу, в нашем случае инвариант программы, выраженную на языке

SMT–LIB; SMT-решатели обладают высокой математической точностью и выра-

зительной силой.

Сравнение предложенного синтетического метода верификации про-

граммы с уже существующими методами.

В настоящее время существует ряд

инструментов, которые используют внутреннее представление кода для реали-

зации задач верификации ПО: LLBMC [15]; Pagai [16].

Инструмент LLBMC осуществляет полностью автоматический статический

анализ кода. Для преобразования кода в SMT-формулу инструмент использует

представление LLVMIR. Такой подход позволяет осуществить следующие про-

верки: целочисленные переполнения; деление на ноль; недопустимые битовые

сдвиги; недопустимый доступ к памяти (выход за границы массива, неверный

доступ с помощью указателя и т. д.); двойное освобождение области памяти

(doublefree); пользовательские проверки с помощью команд assume и assert.