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

计算机学院

Beihang University

科研成果: 期刊稿件 › 文章 › 同行评审

1 引用（Scopus）

摘要

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.

源语言	英语
页（从-至）	50-54
页数	5
期刊	Beijing Youdian Xueyuan Xuebao/Journal of Beijing University of Posts And Telecommunications
卷	39
出版状态	已出版 - 1 6月 2016

其它文件与链接

链接到 Scopus 的出版物

引用此

@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

摘要

其它文件与链接

指纹

引用此