A SPIN-based Approach for Detecting Vulnerabilities in C Programs
Abstract
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.
About the Authors
N. G. Kushik
Томский государственный университет
Russian Federation
Russian Federation
A. . Mammar
Институт телекоммуникаций и менеджмента Франции
Russian Federation
Russian Federation
A. . Cavalli
Институт телекомуникаций и менеджемнта Франции
Russian Federation
Russian Federation
N. V. Yevtushenko
Томский государственный университет
Russian Federation
Russian Federation
W. . Jimenez
Институт телекомуникаций и менеджмента Франции
Russian Federation
Russian Federation
E. . Montes De Oca
Монтимаж
Russian Federation
Russian Federation
References
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.
Review
For citations:
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.)
Views:
713
Email this article 