Geodesic
A SPIN-based approach for detecting vulnerabilities in С~programs
Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 131-143.

Voir la notice de l'article provenant de la source Math-Net.Ru

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.
Keywords: C Program, vulnerability, C language, model checking, SPIN. 
@article{MAIS_2011_18_4_a11,
     author = {N. G. Kushik and A. Mammar and A. Cavalli and N. V. Evtushenko and W. Jimenez and E. Montes de Oca},
     title = {A {SPIN-based} approach for detecting vulnerabilities in {{\CYRS}~programs}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {131--143},
     publisher = {mathdoc},
     volume = {18},
     number = {4},
     year = {2011},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a11/}
}
TY  - JOUR
AU  - N. G. Kushik
AU  - A. Mammar
AU  - A. Cavalli
AU  - N. V. Evtushenko
AU  - W. Jimenez
AU  - E. Montes de Oca
TI  - A SPIN-based approach for detecting vulnerabilities in С~programs
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2011
SP  - 131
EP  - 143
VL  - 18
IS  - 4
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a11/
LA  - ru
ID  - MAIS_2011_18_4_a11
ER  - 
%0 Journal Article
%A N. G. Kushik
%A A. Mammar
%A A. Cavalli
%A N. V. Evtushenko
%A W. Jimenez
%A E. Montes de Oca
%T A SPIN-based approach for detecting vulnerabilities in С~programs
%J Modelirovanie i analiz informacionnyh sistem
%D 2011
%P 131-143
%V 18
%N 4
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a11/
%G ru
%F MAIS_2011_18_4_a11
N. G. Kushik; A. Mammar; A. Cavalli; N. V. Evtushenko; W. Jimenez; E. Montes de Oca. A SPIN-based approach for detecting vulnerabilities in С~programs. Modelirovanie i analiz informacionnyh sistem, Tome 18 (2011) no. 4, pp. 131-143. http://geodesic.mathdoc.fr/item/MAIS_2011_18_4_a11/

[1] E. Kharitonova, Poisk uyazvimostei v programmakh s pomoschyu analizatorov koda http://www.codenet.ru/progr/other/code-analysers.php?rss=1

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

[3] Phil McMinn, “Search-based Software Test Data Generation: A Survey. Softw. Test”, Verif. Reliab., 14(2) (2004), 105–156 | DOI

[4] JPF. The swiss army knife of JavaTM verification http://javapathfinder.sourceforge.net/

[5] http://spinroot.com

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

[7] (Software Testing Glossary) www.aptest.com/glossary.htm#bvatesting

[8] V. P. Kotlyarov, T. V. Kolikova, Osnovy sovremennogo testirovaniya programmnogo obespecheniya, razrabotannogo na C#: Uchebnoe posobie, ed. V. P. Kotlyarova, SPb., 2004, 170 pp. | Zbl

[9] Anton Ermakov, Natalia Kushik, “Detecting C Program Vulnerabilities”, Proc. of the 5th Spring/Summer Young Researchers Colloquium on Software Engineering, 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, 213–228 | Zbl

[11] Alex Groce, Rajeev Joshi, “Extending model checking with dynamic analysis”, Proc. of the VMCAI, LNCS, 4905, 2008 | Zbl