Buffer Overflow Detection in C Code Using Dynamic Symbolic Execution

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

JOURNAL OF BEIJING UNIVERSITY OF POSTS AND TELECOM ›› 2016, Vol. 39 ›› Issue (s1): 50-54.doi: 10.13190/j.jbupt.2016.s.012

• Papers • Previous Articles Next Articles

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

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

CLC Number:

TP309

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]	ZHANG Jiamin, SHUAI Lisha, DONG Gaoya, YANG Xiaolong. A Truth-Oriented Trust Evaluation Model of Shared Messages about Road Events in Internet of Vehicles [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(4): 40-45.
[2]	WU Xuan, JI Weifeng, WENG Jiang, LI Yingqi, SHEN Xiuyu. Certificateless Handover Authentication and Key Agreement Protocol for Network Slicing [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(4): 103-108.
[3]	REN Yanli, FU Yanxia, LI Yerong. Verifiable and Secure Aggregation Scheme for Federated Learning [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(3): 49-55.
[4]	KANG Haiyan, ZHANG Shasha. Cloud Storage and Blockchain Collaborative Access Control Method for Industrial Internet Data Sharing [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(3): 56-61.
[5]	SONG Cheng, CHENG Daochen, NI Shuiping. k Anonymous Trajectory Privacy Protection Scheme of Personalized Differential Privacy [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(3): 109-114.
[6]	DU Maokang, PENG Junjie, HU Yongjin, Xiao Ling. Logistic Regression Matrix Factorization Recommendation Algorithm for Differential Privacy [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(3): 115-120.
[7]	REN Shuai, LEI Xuemei, DAN Zhuoyi, HE Xiao, SHI Lei. Multi-Carrier Information Hiding Algorithm Based on Vertex Partition of 3D Model [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(1): 109-114,126.
[8]	LONG Xiang, CUI Baojiang, WU Jiatong. A Binary Fuzzy Test Method for UEFI DXE Drivers [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(1): 121-126.
[9]	ZHOU Jingxian, LIU Huiyue, ZHOU Yajian, LYU Zongping. Blockchain-Oriented Key Management Scheme for Aeronautical Ad Hoc Networks [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(1): 63-68.
[10]	LI Zhaobin, ZHANG Lu, ZHAO Hong, WEI Zhanzhen. Certificateless Threshold-Based Conditional Proxy Re-Encryption Scheme [J]. Journal of Beijing University of Posts and Telecommunications, 2023, 46(1): 44-49,83.
[11]	Lü Boyu, ZHANG Jie. Internal Attack Analysis of Quantum Key Agreement Protocol Based on Quantum Search Algorithm [J]. Journal of Beijing University of Posts and Telecommunications, 2022, 45(3): 64-68,80.
[12]	PENG Weiping, HAN Ning, SONG Cheng. Certificateless Identity Authentication Scheme for Internet of Vehicles in Edge Computing Environment [J]. Journal of Beijing University of Posts and Telecommunications, 2022, 45(1): 46-51.
[13]	SONG Cheng, XU Biao, HE Junyi. Differential Privacy Trajectory Data Protection Scheme [J]. Journal of Beijing University of Posts and Telecommunications, 2022, 45(1): 13-18.
[14]	SONG Cheng, JIN Tong, HE Jun-yi. A Multi-Value Prediction Location Privacy Protection Mechanism [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(6): 103-108.
[15]	ZHANG Lei, CHEN Chuan, TAN Qi-yun, HAO Mao-xin, YANG Xue-kang. An Image Encryption Algorithm Combining S-Box and Chaotic Mapping [J]. Journal of Beijing University of Posts and Telecommunications, 2021, 44(6): 40-47.

Buffer Overflow Detection in C Code Using Dynamic Symbolic Execution

PDF

Knowledge

Abstract

Cite this article

share this article

References

Related Articles 15

Recommended Articles

Metrics

Comments