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

Наталья Геннадьевна Кушик; Амель Маммар; Ана Кавалли; Нина Владимировна Евтушенко; Вилли Джиминез; Эдгардо Монте Де Ока

doi:10.18255/1818-1015-2011-4-131-143

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

Наталья Геннадьевна Кушик, Амель Маммар, Ана Кавалли, Нина Владимировна Евтушенко, Вилли Джиминез, Эдгардо Монте Де Ока

https://doi.org/10.18255/1818-1015-2011-4-131-143

Полный текст:

Аннотация

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

Ключ. слова

программа, уязвимость, язык С, верификация, SPIN,

УДК: 004.492+519.7

Об авторах

Наталья Геннадьевна Кушик

Томский государственный университет
Россия

Амель Маммар

Институт телекоммуникаций и менеджмента Франции
Россия

Ана Кавалли

Институт телекомуникаций и менеджемнта Франции
Россия

Нина Владимировна Евтушенко

Томский государственный университет
Россия

Вилли Джиминез

Институт телекомуникаций и менеджмента Франции
Россия

Эдгардо Монте Де Ока

Монтимаж
Россия

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

1. Willy Jimenez, Amel Mammar, Ana R. Cavalli. Software Vulnerabilities, Prevention and Detection Methods. A Review, SEC-MDA workshop, Enschede, The Netherlands (24 June 2009).

2. Харитонова Е. Поиск уязвимостей в программах с помощью анализаторов кода [Электрон. статья]. Режим доступа: <http://www.codenet.ru/progr/other/code-> analysers.php?rss=1, свободный.

3. Phil McMinn. Search-based Software Test Data Generation: A Survey. Softw. Test., Verif. Reliab. 2004. 14(2). P. 105-156.

4. JPF. The swiss army knife of JavaTM verification [Электрон. статья]. Режим доступа: <http://javapathfinder.sourceforge.net/>, свободный.

5. SPIN [Электронный ресурс]. Режим доступа: <http://spinroot.com>, свободный.

6. Holzmann Gerard J. SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional. Published Sep. 2003. 4.

7. Software Testing Glossary [Электронный ресурс]. Режим доступа: www.aptest.com/glossary.htm#bvatesting <http://www.aptest.com/glossary.htm%23bvatesting>.

8. Котляров В.П., Коликова Т.В. Основы современного тестирования программного обеспечения, разработанного на C#: Учебное пособие / под редакцией В.П. Котлярова. СПб., 2004. 170 с.

9. Ermakov Anton, Kushik Natalia. Detecting C Program Vulnerabilities // Proc. of the 5th Spring/Summer Young Researchers Colloquium on Software Engineering. P. 61-64.

10. George C. Necula, Scott McPeak, Shree P. Rahul, Westley Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs // International Conference on Compiler Construction. 2002. P. 213-228.

11. Alex Groce, Rajeev Joshi. Extending model checking with dynamic analysis // Proc. of the VMCAI. 2008. LNCS 4905.

Дополнительные файлы

Для цитирования: Кушик Н.Г., Маммар А., Кавалли А., Евтушенко Н.В., Джиминез В., Монте Де Ока Э. Тестирование безопасности программного обеспечения на языке С с использованием верификатора SPIN. Моделирование и анализ информационных систем. 2011;18(4):131-143. https://doi.org/10.18255/1818-1015-2011-4-131-143

For citation: Kushik N.G., Mammar A..., Cavalli A..., Yevtushenko N.V., Jimenez W..., Montes De Oca E... A SPIN-based Approach for Detecting Vulnerabilities in C Programs. Modeling and Analysis of Information Systems. 2011;18(4):131-143. (In Russ.) https://doi.org/10.18255/1818-1015-2011-4-131-143

Обратные ссылки

Обратные ссылки не определены.

Контент доступен под лицензией Creative Commons Attribution 4.0 License.

ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)

Логин
Пароль