Concretely mapped symbolic memory locations for memory error detection

• Main Authors: TU, Haoxin, JIANG, Lingxiao, HONG, Jiaqi, DING, Xuhua, JIANG, He
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2024
• Subjects: Software Reliability; Software Security; Memory Errors; Program Analysis; Symbolic Execution; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/9890; https://ink.library.smu.edu.sg/context/sis_research/article/10890/viewcontent/TSE2024SymLoc.pdf
• Institution: Singapore Management University

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.