A SPIN-based approach for detecting vulnerabilities in С programs
N. G. Kushika, A. Mammarb, A. Cavallib, N. V. Evtushenkoa, W. Jimenezb, E. Montes de Ocac
a Tomsk State University
b Institut des télécommunications et de gestion en France
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.
C Program, vulnerability, C language, model checking, SPIN.
PDF file (477 kB)
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”, Model. Anal. Inform. Sist., 18:4 (2011), 131–143
Citation in format AMSBIB
\by N.~G.~Kushik, A.~Mammar, A.~Cavalli, N.~V.~Evtushenko, W.~Jimenez, E.~Montes de Oca
\paper A SPIN-based approach for detecting vulnerabilities in С~programs
\jour Model. Anal. Inform. Sist.
Citing articles on Google Scholar:
Related articles on Google Scholar:
|Number of views:|