A SPIN-based approach for detecting vulnerabilities in C programs

N. G. Kushik; A. Mammar; A. Cavalli; N. V. Yevtushenko; W. Jimenez; E. Montes De Oca

doi:10.3103/S0146411612070115

A SPIN-based approach for detecting vulnerabilities in C programs

N. G. Kushik
, A. Mammar
, A. Cavalli
, N. V. Yevtushenko
, W. Jimenez
, E. Montes De Oca

Tomsk State University
CNRS SAMOVAR UMR 5157
Montimage

Research output: Contribution to journal › Article › peer-review

1 Citation (Scopus)

Abstract

An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student-made software tools implementing array processing algorithms.

Original language	English
Pages (from-to)	379-386
Number of pages	8
Journal	Automatic Control and Computer Sciences
Volume	46
Issue number	7
DOIs	https://doi.org/10.3103/S0146411612070115
Publication status	Published - 1 Nov 2012
Externally published	Yes

Keywords

C language
C program
Model checking
SPIN
Vulnerability

Access to Document

10.3103/S0146411612070115

Cite this

@article{3d40cf0493d34f4dba9e572ba08297aa,

title = "A SPIN-based approach for detecting vulnerabilities in C programs",

abstract = "An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student-made software tools implementing array processing algorithms.",

keywords = "C language, C program, Model checking, SPIN, Vulnerability",

author = "Kushik, \{N. G.\} and A. Mammar and A. Cavalli and Yevtushenko, \{N. V.\} and W. Jimenez and \{Montes De Oca\}, E.",

year = "2012",

month = nov,

day = "1",

doi = "10.3103/S0146411612070115",

language = "English",

volume = "46",

pages = "379--386",

journal = "Automatic Control and Computer Sciences",

issn = "0146-4116",

publisher = "Pleiades Publishing",

number = "7",

}

TY - JOUR

T1 - A SPIN-based approach for detecting vulnerabilities in C programs

AU - Kushik, N. G.

AU - Mammar, A.

AU - Cavalli, A.

AU - Yevtushenko, N. V.

AU - Jimenez, W.

AU - Montes De Oca, E.

PY - 2012/11/1

Y1 - 2012/11/1

N2 - An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student-made software tools implementing array processing algorithms.

AB - An approach is presented for the detection of software vulnerabilities using the widely known SPIN model checker. Classes of vulnerabilities in C programs that can be detected using the presented approach are discussed. We present the results of experiments on detecting vulnerabilities in student-made software tools implementing array processing algorithms.

KW - C language

KW - C program

KW - Model checking

KW - SPIN

KW - Vulnerability

U2 - 10.3103/S0146411612070115

DO - 10.3103/S0146411612070115

M3 - Article

AN - SCOPUS:84894636442

SN - 0146-4116

VL - 46

SP - 379

EP - 386

JO - Automatic Control and Computer Sciences

JF - Automatic Control and Computer Sciences

IS - 7

ER -

A SPIN-based approach for detecting vulnerabilities in C programs

Abstract

Keywords

Access to Document

Fingerprint

Cite this