全部 标题 作者
关键词 摘要

OALib Journal期刊
ISSN: 2333-9721
费用:99美元

查看量下载量

相关文章

更多...
-  2016 

基于动态符号执行的C代码缓冲区溢出检测

DOI: 10.13190/j.jbupt.2016.s.012

Keywords: 缓冲区溢出检测, 动态符号执行, 可满足模型理论求解器, 底层虚拟机中间代码插桩
Key words: buffer overflow detection dynamic symbolic execution satisfiability modulo theories solver low level virtual machine byte code instrumentation

Full-Text   Cite this paper   Add to My Lib

Abstract:

摘要 缓冲区溢出是C程序中众多安全隐患的根源之一,以C程序代码为目标对象,提出了一个基于底层虚拟机中间代码的缓冲区溢出检测工具PathChecker.该工具基于动态符号执行方法,使用无量词谓词公式刻画缓冲区操作的安全性质,并利用可满足模型理论求解器技术检验缓冲区操作的安全性.实验结果表明,该工具能有效检测C代码中的缓冲区溢出漏洞,且易于推广至其他高级程序语言代码和其他类型安全漏洞的检测.
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.

Full-Text

Contact Us

service@oalib.com

QQ:3279437679

WhatsApp +8615387084133