research-article

Thresher: precise refutations for heap reachability

Authors:

Sam Blackshear,

Bor-Yuh Evan Chang,

Manu SridharanAuthors Info & Claims

PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation

Pages 275 - 286

https://doi.org/10.1145/2491956.2462186

Published: 16 June 2013 Publication History

Abstract

We present a precise, path-sensitive static analysis for reasoning about heap reachability, that is, whether an object can be reached from another variable or object via pointer dereferences. Precise reachability information is useful for a number of clients, including static detection of a class of Android memory leaks. For this client, we found the heap reachability information computed by a state-of-the-art points-to analysis was too imprecise, leading to numerous false-positive leak reports. Our analysis combines a symbolic execution capable of path-sensitivity and strong updates with abstract heap information computed by an initial flow-insensitive points-to analysis. This novel mixed representation allows us to achieve both precision and scalability by leveraging the pre-computed points-to facts to guide execution and prune infeasible paths. We have evaluated our techniques in the Thresher tool, which we used to find several developer-confirmed leaks in Android applications.

References

[1]

L. O. Andersen. phProgram Analysis and Specialization for the C Programming Language. PhD thesis, University of Copenhagen, DIKU, 1994.

[2]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN, 2001.

Digital Library

[3]

T. Ball, O. Kupferman, and G. Yorsh. Abstraction for falsification. In CAV, 2005.

Digital Library

[4]

N. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In ISSTA, 2008.

Digital Library

[5]

J. Berdine, C. Calcagno, and P. W. O'Hearn. Symbolic execution with separation logic. In APLAS, 2005.

Digital Library

[6]

J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. W. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV, 2007.

Digital Library

[7]

D. Beyer, T. A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In PLDI, 2007.

Digital Library

[8]

S. Blackshear, B.-Y. E. Chang, S. Sankaranarayanan, and M. Sridharan. The flow-insensitive precision of andersen's analysis in practice. In SAS, 2011.

Digital Library

[9]

F. Bourdoncle. Abstract debugging of higher-order imperative languages. In PLDI, 1993.

Digital Library

[10]

C. Calcagno, D. Distefano, P. W. O'Hearn, and H. Yang. Compositional shape analysis by means of bi-abduction. In POPL, 2009.

Digital Library

[11]

S. Chandra, S. J. Fink, and M. Sridharan. Snugglebug: a powerful approach to weakest preconditions. In PLDI, 2009.

Digital Library

[12]

B.-Y. E. Chang and X. Rival. Relational inductive shape analysis. In POPL, 2008.

Digital Library

[13]

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM, 50 (5), 2003.

Digital Library

[14]

P. Cousot and R. Cousot. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977.

Digital Library

[15]

P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, and X. Rival. The ASTREÉ analyzer. In ESOP, 2005.

Digital Library

[16]

P. Cousot, P. Ganty, and J.-F. Raskin. Fixpoint-guided abstraction refinements. In SAS, 2007.

Digital Library

[17]

P. Cousot, R. Cousot, and F. Logozzo. Precondition inference from intermittent assertions and application to contracts on collections. In VMCAI, 2011.

Digital Library

[18]

M. Das, S. Lerner, and M. Seigle. ESP: Path-sensitive program verification in polynomial time. In PLDI, 2002.

Digital Library

[19]

I. M. de Moura and N. Bjørner. Z3: An efficient SMT solver. In TACAS, 2008.

Digital Library

[20]

I. Dillig, T. Dillig, and A. Aiken. Sound, complete and scalable path-sensitive analysis. In PLDI, 2008.

Digital Library

[21]

I. Dillig, T. Dillig, and A. Aiken. Fluid updates: Beyond strong vs. weak updates. In ESOP, 2010.

Digital Library

[22]

I. Dillig, T. Dillig, and A. Aiken. Precise reasoning for programs using containers. In POPL, 2011.

Digital Library

[23]

I. Dillig, T. Dillig, and A. Aiken. Automated error diagnosis using abductive inference. In PLDI, 2012.

Digital Library

[24]

D. Distefano and I. Filipović. Memory leaks detection in Java by bi-abductive inference. In FASE, 2010.

Digital Library

[25]

N. Dor, S. Adams, M. Das, and Z. Yang. Software validation via scalable path-sensitive value flow analysis. In ISSTA, 2004.

Digital Library

[26]

S. J. Fink, E. Yahav, N. Dor, G. Ramalingam, and E. Geay. Effective typestate verification in the presence of aliasing. ACM Trans. Softw. Eng. Methodol., 17 (2), 2008.

Digital Library

[27]

C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for Java. In PLDI, 2002.

Digital Library

[28]

S. Z. Guyer and C. Lin. Error checking with client-driven pointer analysis. Sci. Comput. Program., 58 (1--2), 2005.

Digital Library

[29]

B. Hackett and A. Aiken. How is aliasing used in systems software? In FSE, 2006.

Digital Library

[30]

W. R. Harris, S. Sankaranarayanan, F. Ivancic, and A. Gupta. Program analysis via satisfiability modulo path programs. In POPL, 2010.

Digital Library

[31]

T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002.

Digital Library

[32]

S. S. Ishtiaq and P. W. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001.

Digital Library

[33]

S. Khurshid, C. S. Pasareanu, and W. Visser. Generalized symbolic execution for model checking and testing. In TACAS, 2003.

Digital Library

[34]

A. S. Köksal, P. Suter, and V. Kuncak. Scala to the Power of Z3: Integrating SMT and Programming. In CADE, 2011.

[35]

K. R. M. Leino and F. Logozzo. Loop invariants on demand. In APLAS, 2005.

Digital Library

[36]

P. Liang and M. Naik. Scaling abstraction refinement via pruning. In PLDI, 2011.

Digital Library

[37]

P. Liang, O. Tripp, M. Naik, and M. Sagiv. A dynamic evaluation of the precision of static heap abstractions. In OOPSLA, 2010.

Digital Library

[38]

P. Liang, O. Tripp, and M. Naik. Learning minimal abstractions. In POPL, 2011.

Digital Library

[39]

R. Manevich, M. Sridharan, S. Adams, M. Das, and Z. Yang. PSE: explaining program failures via postmortem static analysis. In FSE, 2004.

Digital Library

[40]

A. Milanova, A. Rountev, and B. G. Ryder. Parameterized object sensitivity for points-to analysis for Java. ACM Trans. Softw. Eng. Methodol., 14 (1), 2005.

Digital Library

[41]

J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, 2002.

Digital Library

[42]

X. Rival. Understanding the origin of alarms in Astrée. In SAS, 2005.

Digital Library

[43]

M. Sagiv, T. Reps, and R. Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Trans. Program. Lang. Syst., 20 (1), 1998.

Digital Library

[44]

M. Sridharan and R. Bodik. Refinement-based context-sensitive points-to analysis for Java. In PLDI, 2006.

Digital Library

[45]

B. Woolf. Null object. In Pattern languages of program design 3. Addison-Wesley Longman Publishing Co., Inc., 1997.

Digital Library

Cited By

Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Meier SMover SKaki GChang B(2023)Historia: Refuting Callback Reachability with Message-History LogicsProceedings of the ACM on Programming Languages10.1145/36228657:OOPSLA2(1905-1934)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622865
Tan XZhang YLu JXiong XLiu ZYang MMeng WJensen CCremers CKirda E(2023)SyzDirect: Directed Greybox Fuzzing for Linux KernelProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623146(1630-1644)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623146
Show More Cited By

Index Terms

Thresher: precise refutations for heap reachability

Recommendations

Thresher: precise refutations for heap reachability
PLDI '13

We present a precise, path-sensitive static analysis for reasoning about heap reachability, that is, whether an object can be reached from another variable or object via pointer dereferences. Precise reachability information is useful for a number of ...
Tracking pointers with path and context sensitivity for bug detection in C programs

This paper proposes a pointer alias analysis for automatic error detection. State-of-the-art pointer alias analyses are either too slow or too imprecise for finding errors in real-life programs. We propose a hybrid pointer analysis that tracks actively ...
Tracking pointers with path and context sensitivity for bug detection in C programs
ESEC/FSE-11: Proceedings of the 9th European software engineering conference held jointly with 11th ACM SIGSOFT international symposium on Foundations of software engineering

This paper proposes a pointer alias analysis for automatic error detection. State-of-the-art pointer alias analyses are either too slow or too imprecise for finding errors in real-life programs. We propose a hybrid pointer analysis that tracks actively ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLDI '13: Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation

June 2013

546 pages

ISBN:9781450320146

DOI:10.1145/2491956

General Chair:
Hans-J. Boehm
HP Labs
,
Program Chair:
Cormac Flanagan
University of California, Santa Cruz

ACM SIGPLAN Notices Volume 48, Issue 6
PLDI '13
June 2013
515 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2499370
Issue’s Table of Contents

Copyright © 2013 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 16 June 2013

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PLDI '13

Sponsor:

SIGPLAN

PLDI '13: ACM SIGPLAN Conference on Programming Language Design and Implementation

June 16 - 19, 2013

Washington, Seattle, USA

Acceptance Rates

PLDI '13 Paper Acceptance Rate 46 of 267 submissions, 17%;

Overall Acceptance Rate 406 of 2,067 submissions, 20%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

49
Total Citations
View Citations
477
Total Downloads

Downloads (Last 12 months)36
Downloads (Last 6 weeks)2

Reflects downloads up to 03 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Guo YYao PZhang CChristakis MPradel M(2024)Precise Compositional Buffer Overflow Detection via Heap DisjointnessProceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis10.1145/3650212.3652110(63-75)Online publication date: 11-Sep-2024
https://dl.acm.org/doi/10.1145/3650212.3652110
Meier SMover SKaki GChang B(2023)Historia: Refuting Callback Reachability with Message-History LogicsProceedings of the ACM on Programming Languages10.1145/36228657:OOPSLA2(1905-1934)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622865
Tan XZhang YLu JXiong XLiu ZYang MMeng WJensen CCremers CKirda E(2023)SyzDirect: Directed Greybox Fuzzing for Linux KernelProceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security10.1145/3576915.3623146(1630-1644)Online publication date: 15-Nov-2023
https://dl.acm.org/doi/10.1145/3576915.3623146
Wang CWang WYao PShi QZhou JXiao XZhang C(2023) Anchor: Fast and Precise Value-flow Analysis for Containers via Memory OrientationACM Transactions on Software Engineering and Methodology10.1145/356580032:3(1-39)Online publication date: 26-Apr-2023
https://dl.acm.org/doi/10.1145/3565800
Utture ALiu SKalhauge CPalsberg JDwyer MDamian DZeller A(2022)Striking a balanceProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510166(2043-2055)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510166
Utture APalsberg JDwyer MDamian DZeller A(2022)Fast and precise application code analysis using a partial libraryProceedings of the 44th International Conference on Software Engineering10.1145/3510003.3510046(934-945)Online publication date: 21-May-2022
https://dl.acm.org/doi/10.1145/3510003.3510046
Huang HGuo YShi QYao PWu RZhang C(2022)BEACON: Directed Grey-Box Fuzzing with Provable Path Pruning2022 IEEE Symposium on Security and Privacy (SP)10.1109/SP46214.2022.9833751(36-50)Online publication date: May-2022
https://doi.org/10.1109/SP46214.2022.9833751
Park JLee HRyu S(2021)A Survey of Parametric Static AnalysisACM Computing Surveys10.1145/346445754:7(1-37)Online publication date: 18-Jul-2021
https://dl.acm.org/doi/10.1145/3464457
Shivakumar ABositty APeters NPei Y(2020)Real-Time Interruption Management System for Efficient Distributed Collaboration in Multi-tasking EnvironmentsProceedings of the ACM on Human-Computer Interaction10.1145/33928444:CSCW1(1-23)Online publication date: 29-May-2020
https://dl.acm.org/doi/10.1145/3392844
Zhu TLiu GChen G(2020)Social Collaborative Mutual Learning for Item RecommendationACM Transactions on Knowledge Discovery from Data10.1145/338716214:4(1-19)Online publication date: 30-May-2020
https://dl.acm.org/doi/10.1145/3387162
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten