Publication Type
Journal Article
Version
acceptedVersion
Publication Date
4-2024
Abstract
Memory allocation is a fundamental operation for managing memory objects in many programming languages. Misusing allocated memory objects (e.g., buffer overflow and use-after-free) can lead to catastrophic consequences. Symbolic execution-based approaches are often used to detect such memory errors, leveraging their capabilities in automatic path exploration and test case generation. However, existing symbolic execution engines face significant limitations in modeling dynamic memory layouts. These engines either represent memory object locations as concrete addresses, limiting analyses to specific address layouts and missing errors that occur at special addresses, or represent locations as simple symbolic variables without sufficient constraints, resulting in memory state explosion during read/write operations involving symbolic addresses. These challenges hinder effective detection of certain memory errors.In this study, we propose SYMLOC, a symbolic execution-based approach that employs concretely mapped symbolic memory locations to address these limitations. SYMLOC integrates three novel techniques: (1) symbolizing addresses and encoding symbolic addresses into path constraints, (2) performing symbolic memory read/write operations using a symbolic-concrete memory map, and (3) automatically tracking the use of symbolic memory locations. Built on the KLEE symbolic execution engine, SYMLOC demonstrates improved memory error detection and code coverage capabilities.Evaluation results show that SYMLOC detects 23 additional address-specific spatial memory errors in GNU Coreutils, Make, and m4 programs compared to other approaches and achieves 15%-48% higher unique code coverage. For temporal memory errors, SYMLOC detects 8%-64% more errors in the Juliet Test Suite than various state-of-the-art detectors. Additionally, two case studies illustrate memory errors detected by SYMLOC, their root causes, and implications.
Keywords
Software Reliability, Software Security, Memory Errors, Program Analysis, Symbolic Execution
Discipline
Software Engineering
Research Areas
Software and Cyber-Physical Systems
Areas of Excellence
Digital transformation
Publication
IEEE Transactions on Software Engineering
Volume
50
Issue
7
First Page
1747
Last Page
1767
ISSN
0098-5589
Identifier
10.1109/TSE.2024.3395412
Publisher
Institute of Electrical and Electronics Engineers
Citation
TU, Haoxin; JIANG, Lingxiao; HONG, Jiaqi; DING, Xuhua; and JIANG, He.
Concretely mapped symbolic memory locations for memory error detection. (2024). IEEE Transactions on Software Engineering. 50, (7), 1747-1767.
Available at: https://ink.library.smu.edu.sg/sis_research/9890
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1109/TSE.2024.3395412
