maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1104Research ArticleОригинальные статьиArticlesТестирование безопасности программного обеспечения на языке С с использованием верификатора SPINA SPIN-based Approach for Detecting Vulnerabilities in C ProgramsКушикНаталья ГеннадьевнаKushikN. G.noemail@neicon.ruМаммарАмельMammarA. .amel.mammar@it-sudparis.euКаваллиАнаCavalliA. .noemail@neicon.ruЕвтушенкоНина ВладимировнаYevtushenkoN. V.ninayevtushenko@yahoo.comДжиминезВиллиJimenezW. .noemail@neicon.ruМонте Де ОкаЭдгардоMontes De OcaE. .edgardo.montesdeoca@montimage.comТомский государственный университетRussian FederationИнститут телекоммуникаций и менеджмента ФранцииRussian FederationИнститут телекомуникаций и менеджемнта ФранцииRussian FederationИнститут телекомуникаций и менеджмента ФранцииRussian FederationМонтимажRussian Federation201120122011184131143Copyright © Кушик Н.Г., Маммар А..., Кавалли А..., Евтушенко Н.В., Джиминез В..., Монте Де Ока Э..., 20112011Кушик Н.Г., Маммар А., Кавалли А., Евтушенко Н.В., Джиминез В., Монте Де Ока Э.Kushik N.G., Mammar A..., Cavalli A..., Yevtushenko N.V., Jimenez W..., Montes De Oca E...Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/1104

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

The C language is widely used for developing tools in various application areas, and a number of C software tools are used for critical systems, such as medicine, transport, etc. Correspondingly, the security of such programs should be thoroughly tested, i.e., it is important to develop techniques for detecting vulnerabilities in C programs. In this paper we present an approach for dynamic detection of software vulnerabilities using the SPIN model checker. We discuss how this approach can be implemented in order to detect automatically C code vulnerabilities and illustrate a proposed technique for a number of C programs which are widely used in a number of applications.

программауязвимостьязык СверификацияSPINC ProgramvulnerabilityC languagemodel checkingSPINReferencesWilly Jimenez, Amel Mammar, Ana R. Cavalli. Software Vulnerabilities, Prevention and Detection Methods. A Review, SEC-MDA workshop, Enschede, The Netherlands (24 June 2009).Willy Jimenez, Amel Mammar, Ana R. Cavalli. Software Vulnerabilities, Prevention and Detection Methods. A Review, SEC-MDA workshop, Enschede, The Netherlands (24 June 2009).Харитонова Е. Поиск уязвимостей в программах с помощью анализаторов кода [Электрон. статья]. Режим доступа: <http://www.codenet.ru/progr/other/code-> analysers.php?rss=1, свободный.Харитонова Е. Поиск уязвимостей в программах с помощью анализаторов кода [Электрон. статья]. Режим доступа: <http://www.codenet.ru/progr/other/code-> analysers.php?rss=1, свободный.Phil McMinn. Search-based Software Test Data Generation: A Survey. Softw. Test., Verif. Reliab. 2004. 14(2). P. 105-156.Phil McMinn. Search-based Software Test Data Generation: A Survey. Softw. Test., Verif. Reliab. 2004. 14(2). P. 105-156.JPF. The swiss army knife of JavaTM verification [Электрон. статья]. Режим доступа: <http://javapathfinder.sourceforge.net/>, свободный.JPF. The swiss army knife of JavaTM verification [Электрон. статья]. Режим доступа: <http://javapathfinder.sourceforge.net/>, свободный.SPIN [Электронный ресурс]. Режим доступа: <http://spinroot.com>, свободный.SPIN [Электронный ресурс]. Режим доступа: <http://spinroot.com>, свободный.Holzmann Gerard J. SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional. Published Sep. 2003. 4.Holzmann Gerard J. SPIN Model Checker: The Primer and Reference Manual. Addison-Wesley Professional. Published Sep. 2003. 4.Software Testing Glossary [Электронный ресурс]. Режим доступа: www.aptest.com/glossary.htm#bvatesting <http://www.aptest.com/glossary.htm%23bvatesting>.Software Testing Glossary [Электронный ресурс]. Режим доступа: www.aptest.com/glossary.htm#bvatesting <http://www.aptest.com/glossary.htm%23bvatesting>.Котляров В.П., Коликова Т.В. Основы современного тестирования программного обеспечения, разработанного на C#: Учебное пособие / под редакцией В.П. Котлярова. СПб., 2004. 170 с.Котляров В.П., Коликова Т.В. Основы современного тестирования программного обеспечения, разработанного на C#: Учебное пособие / под редакцией В.П. Котлярова. СПб., 2004. 170 с.Ermakov Anton, Kushik Natalia. Detecting C Program Vulnerabilities // Proc. of the 5th Spring/Summer Young Researchers Colloquium on Software Engineering. P. 61-64.Ermakov Anton, Kushik Natalia. Detecting C Program Vulnerabilities // Proc. of the 5th Spring/Summer Young Researchers Colloquium on Software Engineering. P. 61-64.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.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.Alex Groce, Rajeev Joshi. Extending model checking with dynamic analysis // Proc. of the VMCAI. 2008. LNCS 4905.Alex Groce, Rajeev Joshi. Extending model checking with dynamic analysis // Proc. of the VMCAI. 2008. LNCS 4905.

The authors declare that there are no conflicts of interest present.