Selective control-flow abstraction via jumping

Abstract

We present jumping, a form of selective control-flow abstraction useful for improving the scalability of goal-directed static analyses. Jumping is useful for analyzing programs with complex control-flow such as event-driven systems. In such systems, accounting for orderings between certain events is important for precision, yet analyzing the product graph of all possible event orderings is intractable. Jumping solves this problem by allowing the analysis to selectively abstract away control-flow between events irrelevant to a goal query while preserving information about the ordering of relevant events. We present a framework for designing sound jumping analyses and create an instantiation of the framework for per- forming precise inter-event analysis of Android applications. Our experimental evaluation showed that using jumping to augment a precise goal-directed analysis with inter-event reasoning enabled our analysis to prove 90–97% of dereferences safe across our benchmarks.

References

1. Hopper. https://github.com/cuplv/hopper, 2015.
2. Nit: Nullability inference tool. http://nit.gforge.inria. fr/, 2015.
3. T.J. Watson Libraries for Analysis (WALA). http://wala. sf.net, 2015.
4. Josh Berdine, Cristiano Calcagno, and Peter W. O’Hearn. Symbolic execution with separation logic. In Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2005.
5. Stephen M. Blackburn, Robin Garner, Chris Hoffmann, Asjad M. Khan, Kathryn S. McKinley, Rotem Bentzur, Amer Diwan, Daniel Feinberg, Daniel Frampton, Samuel Z. Guyer, Martin Hirzel, Antony L. Hosking, Maria Jump, Han Bok Lee, J. Eliot B. Moss, Aashish Phansalkar, Darko Stefanovic, Thomas VanDrunen, Daniel von Dincklage, and Ben Wiedermann. The DaCapo benchmarks: Java benchmarking development and analysis. In Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2006.
6. Sam Blackshear. Flexible Goal-Directed Abstraction. PhD thesis, University of Colorado Boulder, 2015.
7. Sam Blackshear, Bor-Yuh Evan Chang, and Manu Sridharan. Thresher: Precise refutations for heap reachability. In Programming Language Design and Implementation (PLDI), 2013.
8. Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang. Droidel: A general approach to Android framework modeling. In State of the Art in Program Analysis (SOAP), 2015.
9. Franc¸ois Bourdoncle. Abstract debugging of higher-order imperative languages. In Programming Language Design and Implementation (PLDI), 1993.
10. Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), 2010.
11. Cristiano Calcagno, Dino Distefano, Jérémy Dubreil, Dominik Gabi, Pieter Hooimeijer, Martino Luca, Peter W. O’Hearn, Irene Papakonstantinou, Jim Purbrick, and Dulma Rodriguez. Moving fast with software verification. In NASA Formal Methods (NFM), 2015.
12. Devin Coughlin and Bor-Yuh Evan Chang. Fissile type analysis: Modular checking of almost everywhere invariants. In Principles of Programming Languages (POPL), 2014.
13. Patrick Cousot, Radhia Cousot, Manuel Fähndrich, and Francesco Logozzo. Automatic inference of necessary preconditions. In Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013.
14. Leonardo Mendonc¸a de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2008.
15. Isil Dillig, Thomas Dillig, and Alex Aiken. Sound, complete and scalable path-sensitive analysis. In Programming Language Design and Implementation (PLDI), 2008.
16. Isil Dillig, Thomas Dillig, and Alex Aiken. Precise reasoning for programs using containers. In Principles of Programming Languages (POPL), 2011.
17. Azadeh Farzan, Zachary Kincaid, and Andreas Podelski. Inductive data flow graphs. In Principles of Programming Languages (POPL), 2013.
18. Christian Fritz, Steven Arzt, Siegfried Rasthofer, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves le Traon, Damien Octeau, and Patrick McDaniel. FlowDroid: Precise context, flow, field, object-sensitive and lifecycle-aware taint analysis for Android apps. In Conference on Programming Language Design and Implementation (PLDI), 2014.
19. Ranjit Jhala and Rupak Majumdar. Interprocedural analysis of asynchronous programs. In ACM Symposium on Principles of Programming Languages (POPL), 2007.
20. Adam Kiezun, Vijay Ganesh, Shay Artzi, Philip J. Guo, Pieter Hooimeijer, and Michael D. Ernst. HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol., 21(4), 2012.
21. Shuying Liang, Andrew W. Keep, Matthew Might, Steven Lyde, Thomas Gilray, Petey Aldous, and David Van Horn. Sound and precise malware analysis for Android via pushdown reachability and entry-point saturation. In Security and Privacy in Smartphones and Mobile Devices (SPSM@CCS), 2013.
22. Alexey Loginov, Eran Yahav, Satish Chandra, Stephen Fink, Noam Rinetzky, and Mangala Gowri Nanda. Verifying dereference safety via expanding-scope analysis. In Software Testing and Analysis (ISSTA), 2008.
23. Ravichandhran Madhavan and Raghavan Komondoor. Null dereference verification via over-approximated weakest preconditions analysis. In Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2011.
24. Amogh Margoor and Raghavan Komondoor. Two techniques to improve the precision of a demand-driven null-dereference verification approach. Sci. Comput. Program., 98, 2015.
25. Mangala Gowri Nanda and Saurabh Sinha. Accurate interprocedural null-dereference analysis for Java. In International Conference on Software Engineering (ICSE), 2009.
26. Hakjoo Oh, Wonchan Lee, Kihong Heo, Hongseok Yang, and Kwangkeun Yi. Selective context-sensitivity guided by impact pre-analysis. In Conference on Programming Language Design and Implementation (PLDI), 2014.
27. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In Logic in Computer Science (LICS), 2002.
28. Xavier Rival. Understanding the origin of alarms in Astrée. In Static Analysis (SAS), 2005.
29. Yannis Smaragdakis, George Kastrinis, and George Balatsouras. Introspective analysis: context-sensitivity, across the board. In Conference on Programming Language Design and Implementation (PLDI), 2014.
30. Manu Sridharan and Rastislav Bod´ık. Refinement-based context-sensitive points-to analysis for java. In Programming Language Design and Implementation (PLDI), 2006.
31. Frank Tip. A survey of program slicing techniques. J. Prog. Lang., 3(3), 1995.
32. Shengqian Yang, Dacong Yan, Haowei Wu, Yan Wang, and Atanas Rountev. Static control-flow analysis of user-driven callbacks in Android applications. In International Conference on Software Engineering (ICSE), 2015.
33. Xin Zhang, Ravi Mangal, Radu Grigore, Mayur Naik, and Hongseok Yang. On abstraction refinement for program analyses in Datalog. In Conference on Programming Language Design and Implementation (PLDI), 2014.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Verification

• Software and its engineering

  • Software creation and management

    • Software development process management

    • Software verification and validation

      • Formal software verification

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Software verification

• Theory of computation

  • Semantics and reasoning

    • Program reasoning

      • Program verification