Тестирование безопасности программного обеспечения на языке С с использованием верификатора SPIN
Аннотация
Предлагается метод тестирования безопасности С программ с использованием широко известного верификатора SPIN. Обсуждаются классы уязвимостей в С программах, которые могут быть обнаружены с использованием предложенного подхода. Приводятся результаты компьютерных экспериментов по обнаружению уязвимостей в студенческих программных реализациях алгоритмов работы с массивами.
Об авторах
Наталья Геннадьевна Кушик
Томский государственный университет
Россия
Россия
Амель Маммар
Институт телекоммуникаций и менеджмента Франции
Россия
Россия
Ана Кавалли
Институт телекомуникаций и менеджемнта Франции
Россия
Россия
Нина Владимировна Евтушенко
Томский государственный университет
Россия
Россия
Вилли Джиминез
Институт телекомуникаций и менеджмента Франции
Россия
Россия
Эдгардо Монте Де Ока
Монтимаж
Россия
Россия
Список литературы
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.
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.)
Просмотров: 439
Послать статью по эл. почте 