Buffer overflow detection in C code using dynamic symbolic execution

Jun Xian Zhang; Zhou Jun Li

Buffer overflow detection in C code using dynamic symbolic execution

Jun Xian Zhang
, Zhou Jun Li

School of Computer Science and Engineering

Beihang University

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

1 Scopus citations

Abstract

Buffer overflow is a source of many security problems in C programs. A new tool named PathChecker to detect buffer overflows in C codes using dynamic symbolic execution method is proposed. PathChecker uses quantifier-free predicate formulas to describe the safety properties of buffer access operations and check these properties using a SMT solver. Experimental results show the effectiveness of this tool which is very easy to extend to check other safety properties.

Original language	English
Pages (from-to)	50-54
Number of pages	5
Journal	Beijing Youdian Xueyuan Xuebao/Journal of Beijing University of Posts And Telecommunications
Volume	39
State	Published - 1 Jun 2016

Keywords

Buffer overflow detection
Dynamic symbolic execution
Low level virtual machine byte code instrumentation
Satisfiability modulo theories solver

Cite this

@article{00d8737206764696b7165be6eaf41b14,

title = "Buffer overflow detection in C code using dynamic symbolic execution",

abstract = "Buffer overflow is a source of many security problems in C programs. A new tool named PathChecker to detect buffer overflows in C codes using dynamic symbolic execution method is proposed. PathChecker uses quantifier-free predicate formulas to describe the safety properties of buffer access operations and check these properties using a SMT solver. Experimental results show the effectiveness of this tool which is very easy to extend to check other safety properties.",

keywords = "Buffer overflow detection, Dynamic symbolic execution, Low level virtual machine byte code instrumentation, Satisfiability modulo theories solver",

author = "Zhang, \{Jun Xian\} and Li, \{Zhou Jun\}",

year = "2016",

month = jun,

day = "1",

language = "英语",

volume = "39",

pages = "50--54",

journal = "Beijing Youdian Xueyuan Xuebao/Journal of Beijing University of Posts And Telecommunications",

issn = "1007-5321",

publisher = "Beijing University of Posts and Telecommunications",

}

TY - JOUR

T1 - Buffer overflow detection in C code using dynamic symbolic execution

AU - Zhang, Jun Xian

AU - Li, Zhou Jun

PY - 2016/6/1

Y1 - 2016/6/1

N2 - Buffer overflow is a source of many security problems in C programs. A new tool named PathChecker to detect buffer overflows in C codes using dynamic symbolic execution method is proposed. PathChecker uses quantifier-free predicate formulas to describe the safety properties of buffer access operations and check these properties using a SMT solver. Experimental results show the effectiveness of this tool which is very easy to extend to check other safety properties.

AB - Buffer overflow is a source of many security problems in C programs. A new tool named PathChecker to detect buffer overflows in C codes using dynamic symbolic execution method is proposed. PathChecker uses quantifier-free predicate formulas to describe the safety properties of buffer access operations and check these properties using a SMT solver. Experimental results show the effectiveness of this tool which is very easy to extend to check other safety properties.

KW - Buffer overflow detection

KW - Dynamic symbolic execution

KW - Low level virtual machine byte code instrumentation

KW - Satisfiability modulo theories solver

UR - https://www.scopus.com/pages/publications/84982943076

M3 - 文章

AN - SCOPUS:84982943076

SN - 1007-5321

VL - 39

SP - 50

EP - 54

JO - Beijing Youdian Xueyuan Xuebao/Journal of Beijing University of Posts And Telecommunications

JF - Beijing Youdian Xueyuan Xuebao/Journal of Beijing University of Posts And Telecommunications

ER -

Buffer overflow detection in C code using dynamic symbolic execution

Abstract

Keywords

Other files and links

Fingerprint

Cite this