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

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

北京邮电大学学报 ›› 2016, Vol. 39 ›› Issue (s1): 50-54.doi: 10.13190/j.jbupt.2016.s.012

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

张俊贤, 李舟军

北京航空航天大学计算机学院, 北京 100191

收稿日期:2015-09-02 出版日期:2016-06-28 发布日期:2016-06-28
作者简介:张俊贤(1981-),男,博士生,E-mail:LoongWalker@163.com;李舟军(1963-),男,博士,教授,博士生导师.
基金资助:
国家自然科学基金项目（61170189，61370126）；国家高技术研究发展计划（863计划）项目（2015AA016004）

Buffer Overflow Detection in C Code Using Dynamic Symbolic Execution

ZHANG Jun-xian, LI Zhou-jun

School of Computer Science and Engineering, Beihang University, Beijing 100191, China

Received:2015-09-02 Online:2016-06-28 Published:2016-06-28

摘要/Abstract

摘要：

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

关键词: 缓冲区溢出检测, 动态符号执行, 可满足模型理论求解器, 底层虚拟机中间代码插桩

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.

Key words: buffer overflow detection, dynamic symbolic execution, satisfiability modulo theories solver, low level virtual machine byte code instrumentation

中图分类号:

TP309

张俊贤, 李舟军. 基于动态符号执行的C代码缓冲区溢出检测[J]. 北京邮电大学学报, 2016, 39(s1): 50-54.

ZHANG Jun-xian, LI Zhou-jun. Buffer Overflow Detection in C Code Using Dynamic Symbolic Execution[J]. JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM, 2016, 39(s1): 50-54.

[1]	张佳敏帅莉莎董高雅阳小龙. 面向道路实况的车联网共享消息可信评估模型[J]. 北京邮电大学学报, 2023, 46(4): 40-45.
[2]	吴玄姬伟峰翁江李映岐申秀雨. 面向网络切片的无证书切换认证与密钥协商协议[J]. 北京邮电大学学报, 2023, 46(4): 103-108.
[3]	任艳丽, 付燕霞, 李烨榕. 面向联邦学习的可验证安全聚合方案[J]. 北京邮电大学学报, 2023, 46(3): 49-55.
[4]	康海燕, 张沙沙. 云链协同的工业互联网数据共享访问控制方法[J]. 北京邮电大学学报, 2023, 46(3): 56-61.
[5]	宋成, 程道晨, 倪水平. 个性化差分隐私的 k 匿名轨迹隐私保护方案[J]. 北京邮电大学学报, 2023, 46(3): 109-114.
[6]	杜茂康彭俊杰胡勇进肖玲. 满足差分隐私的逻辑回归矩阵分解推荐算法[J]. 北京邮电大学学报, 2023, 46(3): 115-120.
[7]	任帅雷雪梅淡卓异何骁石磊. 一种基于三维模型顶点分区的多载体信息隐藏算法[J]. 北京邮电大学学报, 2023, 46(1): 109-114,126.
[8]	龙翔崔宝江吴佳桐. 一种UEFI DXE 驱动二进制模糊测试方法[J]. 北京邮电大学学报, 2023, 46(1): 121-126.
[9]	周景贤刘惠悦周亚建吕宗平. 面向区块链的航空自组网密钥管理方案[J]. 北京邮电大学学报, 2023, 46(1): 63-68.
[10]	李兆斌张璐赵洪魏占祯. 基于无证书的门限条件代理重加密方案[J]. 北京邮电大学学报, 2023, 46(1): 44-49,83.
[11]	吕博宇, 张劼. 基于QSA的量子密钥协商协议内部攻击分析[J]. 北京邮电大学学报, 2022, 45(3): 64-68,80.
[12]	彭维平, 韩宁, 宋成. 边缘计算环境下无证书车联网身份认证方案[J]. 北京邮电大学学报, 2022, 45(1): 46-51.
[13]	宋成, 许标, 贺军义. 差分隐私轨迹数据保护方案[J]. 北京邮电大学学报, 2022, 45(1): 13-18.
[14]	宋成, 金彤, 贺军义. 多值预测位置隐私保护机制[J]. 北京邮电大学学报, 2021, 44(6): 103-108.
[15]	张雷, 陈川, 谭淇匀, 郝茂鑫, 杨学康. 结合S盒与混沌映射的图像加密算法[J]. 北京邮电大学学报, 2021, 44(6): 40-47.

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

Buffer Overflow Detection in C Code Using Dynamic Symbolic Execution

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献

相关文章 15

编辑推荐

Metrics

本文评价