Per-Dereference Verification of Temporal Heap Safety via Adaptive Context-Sensitive Analysis

Publication Type:
Conference Proceeding
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2019, 11822 LNCS pp. 48 - 72
Issue Date:
Full metadata record
© Springer Nature Switzerland AG 2019. We address the problem of verifying the temporal safety of heap memory at each pointer dereference. Our whole-program analysis approach is undertaken from the perspective of pointer analysis, allowing us to leverage the advantages of and advances in pointer analysis to improve precision and scalability. A dereference (Forumala Presented)., say, via pointer q is unsafe iff there exists a deallocation (Forumala Presented)., say, via pointer p such that on a control-flow path (Forumala Presented).,p aliases with q (with both pointing to an object o representing an allocation), denoted, and (Forumala Presented). reaches (Forumala Presented). via control flow, denoted. Applying directly any existing pointer analysis, which is typically solved separately with an associated control-flow reachability analysis, will render such verification highly imprecise, since (i.e., (Forumala Presented). does not distribute over (Forumala Presented). ). For precision, we solve, with a control-flow path (Forumala Presented). containing an allocation o, a deallocation (Forumala Presented). and a dereference (Forumala Presented). abstracted by a tuple of three contexts. For scalability, a demand-driven full context-sensitive (modulo recursion) pointer analysis, which operates on pre-computed def-use chains with adaptive context-sensitivity, is used to infer, without losing soundness or precision. Our evaluation shows that our approach can successfully verify the safety of 81.3% (or (Forumala Presented).) of all the dereferences in a set of ten C programs totalling 1,166 KLOC.
Please use this identifier to cite or link to this item: