Тестирование безопасности программного обеспечения на языке С с использованием верификатора 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.)

Просмотров: 26

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

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


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


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