Н. Г. Кушик, А. Маммар, А. Кавалли, Н. В. Евтушенко, В. Джиминез, Э. Монте де Ока, “Тестирование безопасности программного обеспечения на языке С с использованием верификатора SPIN”, Модел. и анализ информ. систем, 2011, том 18, номер 4,страницы 131

Тестирование безопасности программного обеспечения на языке С с использованием верификатора SPIN

Н. Г. Кушик^a, А. Маммар^b, А. Кавалли^b, Н. В. Евтушенко^a, В. Джиминез^b, Э. Монте де Ока^c

^a Томский государственный университет
^b Институт телекоммуникаций и менеджмента Франции
^c Компания Монтимаж

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

Ключевые слова: программа, уязвимость, язык С, верификация, SPIN.

УДК: 004.492+519.7

Поступила в редакцию: 20.09.2011