Concretely Mapped Symbolic Memory Locations for Memory Error Detection
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 have catastrophic consequences. Symbolic execution-based approaches have been used to detect such memory errors, benefiting from their capabilities in automatic path exploration and test case generation. However, existing symbolic execution engines still suffer from fundamental limitations in modeling dynamic memory layouts; they either represent the locations of memory objects as concrete addresses and thus limit their analyses only to specific address layouts and miss errors that may only occur when the objects are located at special addresses, or represent the locations as simple symbolic variables without sufficient constraints and thus suffer from memory state explosion when they execute read/write operations involving symbolic addresses. Such limitations hinder the existing symbolic execution engines from effectively detecting certain memory errors. This paper proposes SymLoc, a symbolic execution-based approach that uses concretely mapped symbolic memory locations to alleviate the limitations mentioned above. Specifically, a new integration of three techniques is designed in SymLoc: (1) the symbolization of addresses and encoding of symbolic addresses into path constraints, (2) the symbolic memory read/write operations using a symbolic-concrete memory map, and (3) the automatic tracking of the uses of symbolic memory locations. We build SymLoc on top of the well-known symbolic execution engine KLEE and demonstrate its benefits in terms of memory error detection and code coverage capabilities. Our evaluation results show that: for address-specific spatial memory errors, SymLoc is able to detect 23 more errors in GNU Coreutils, Make, and m4 programs that are difficult for other approaches to detect, and cover 15% and 48% more unique lines of code in the programs than two baseline approaches; for temporal memory errors, SymLoc is able to detect 8%-64% more errors in the Juliet Test Suite than various existing state-of-the-art memory error detectors. We also present two case studies to show sample memory errors detected by SymLoc along with their root causes and implications.
Thu 31 OctDisplayed time zone: Pacific Time (US & Canada) change
13:30 - 15:00 | Bug detection and predictionResearch Papers / Journal-first Papers at Compagno Chair(s): Tim Menzies North Carolina State University | ||
13:30 15mTalk | Towards Effective Static Type-Error Detection for Python Research Papers | ||
13:45 15mTalk | Detecting Element Accessing Bugs in C++ Sequence Containers Research Papers | ||
14:00 15mTalk | Concretely Mapped Symbolic Memory Locations for Memory Error Detection Journal-first Papers Haoxin Tu Singapore Management University, Singapore, Lingxiao Jiang Singapore Management University, Jiaqi Hong Independent Researcher, Xuhua Ding Singapore Management University, He Jiang Dalian University of Technology | ||
14:15 15mTalk | NeuroJIT: Improving Just-In-Time Defect Prediction Using Neurophysiological and Empirical Perceptions of Modern Developers Research Papers |