ВЫЯВЛЕНИЕ СКРЫТЫХ УЯЗВИМОСТЕЙ В ИСХОДНОМ КОДЕ МНОГОПОТОЧНЫХ ПРОГРАММ ПОСРЕДСТВОМ АНАЛИЗА ФУНКЦИОНАЛЬНЫХ ПЕРЕХОДОВ

Аннотация

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