Concerto: a framework for combined concrete and abstract interpretation

Abstract

Abstract interpretation promises sound but computable static summarization of program behavior. However, modern software engineering practices pose significant challenges to this vision, specifically the extensive use of frameworks and complex libraries. Frameworks heavily use reflection, metaprogramming, and multiple layers of abstraction, all of which confound even state-of-the-art abstract interpreters. Sound but conservative analysis of frameworks is impractically imprecise, and unsoundly ignoring reflection and metaprogramming is untenable given the prevalence of these features. Manually modeling framework behaviors offers excellent precision, at the cost of immense effort by the tool designer.

To overcome the above difficulties, we present Concerto, a system for analyzing framework-based applications by soundly combining concrete and abstract interpretation. Concerto analyzes framework implementations using concrete interpretation, and application code using abstract interpretation. This technique is possible in practice as framework implementations typically follow a single path of execution when provided a concrete, application-specific configuration file which is often available at analysis time. Concerto exploits this configuration information to precisely resolve reflection and other metaprogramming idioms during concrete execution. In contrast, application code may have infinitely many paths of execution, so Concerto switches to abstract interpretation to analyze application code. Concerto is an analysis framework, and can be instantiated with any abstract interpretation that satisfies a small set of preconditions. In addition, unlike manual modeling, Concerto is not specialized to any specific framework implementation. We have formalized our approach and proved several important properties including soundness and termination. In addition, we have implemented an initial proof of concept prototype of Concerto for a subset of Java, and found that our combined interpretation significantly improves analysis precision and performance.

References

1. Steven Arzt, Siegfried Rasthofer, Christian Fritz, Eric Bodden, Alexandre Bartel, Jacques Klein, Yves Le Traon, Damien Octeau, and Patrick McDaniel. 2014. FlowDroid: Precise Context, Flow, Field, Object-sensitive and Lifecycle-aware Taint Analysis for Android Apps. In PLDI.
2. Thanassis Avgerinos, Alexandre Rebert, Sang Kil Cha, and David Brumley. 2014. Enhancing symbolic execution with veritesting. In ICSE.
3. Davide Balzarotti, Marco Cova, Vika Felmetsger, Nenad Jovanovic, Engin Kirda, Christopher Kruegel, and Giovanni Vigna. 2008. Saner: Composing static and dynamic analysis to validate sanitization in web applications. In Symposium on Security and Privacy .
4. Paulo Barros, René Just, Suzanne Millstein, Paul Vines, Werner Dietl, Michael D Ernst, et al. 2015. Static analysis of implicit control flow: Resolving Java reflection and Android intents. In ASE.
5. Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang. 2015. Droidel: A general approach to android framework modeling. In SOAP.
6. Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati, and Mira Mezini. 2011. Taming reflection: Aiding static analysis in the presence of reflection and custom class loaders. In ICSE.
7. François Bourdoncle. 1993. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and their Applications .
8. Guillaume Brat, Klaus Havelund, SeungJoon Park, and Willem Visser. 2000. Java PathFinder-second generation of a Java model checker. In Workshop on Advances in Verification.
9. Jörg Brauer, Thomas Noll, and Bastian Schlich. 2010. Interval analysis of microcontroller code using abstract interpretation of hardware and software. In Workshop on Software & Compilers for Embedded Systems.
10. Matt Brown and Jens Palsberg. 2017. Jones-optimal partial evaluation by specialization-safe normalization. Proc. ACM Program. Lang. 2, POPL (2017), 14.
11. Cristian Cadar, Daniel Dunbar, Dawson R Engler, et al. 2008. KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs. In OSDI.
12. Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: A Platform for In-vivo Multi-path Analysis of Software Systems. In ASPLOS.
13. Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, and Sorin Lerner. 2009. Staged Information Flow for Javascript. In PLDI.
14. Patrick Cousot. 1977. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice. Res. rep. RR 88 (1977).
15. Patrick Cousot and Radhia Cousot. 1977. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL.
16. Patrick Cousot and Radhia Cousot. 1979a. Constructive versions of Tarski’s fixed point theorems. Pacific journal of Mathematics 82, 1 (1979).
17. Patrick Cousot and Radhia Cousot. 1979b. Systematic design of program analysis frameworks. In POPL. ACM.
18. Patrick Cousot and Radhia Cousot. 1992a. Abstract interpretation and application to logic programs. The Journal of Logic Programming 13, 2-3 (1992), 103–179.
19. Patrick Cousot and Radhia Cousot. 1992b. Abstract interpretation frameworks. Journal of logic and computation 2, 4 (1992).
20. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2005. The ASTRÉE analyzer. In ESOP.
21. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. 2006. Combination of abstractions in the ASTRÉE static analyzer. In Annual Asian Computing Science Conference.
22. Christoph Csallner, Yannis Smaragdakis, and Tao Xie. 2008. DSD-Crasher: A hybrid analysis tool for bug finding. TOSEM 17, 2 (2008), 8.
23. Dorothy E Denning. 1976. A lattice model of secure information flow. Commun. ACM 19, 5 (1976).
24. Alain Deutsch. 1994. Interprocedural May-alias Analysis for Pointers: Beyond K-limiting. In PLDI.
25. Bruno Dufour, Barbara G. Ryder, and Gary Sevitsky. 2007. Blended analysis for performance understanding of frameworkbased applications. In ISSTA.
26. Manuel Fähndrich and Francesco Logozzo. 2010. Static contract checking with abstract interpretation. In Formal Verification of Object-Oriented Software .
27. Pietro Ferrara. 2010. Static type analysis of pattern matching by abstract interpretation. In Formal Techniques for Distributed Systems . Springer, 186–200.
28. Pietro Ferrara. 2014. Generic combination of heap and value analyses in abstract interpretation. In VMCAI.
29. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. 2008. Effective typestate verification in the presence of aliasing. TOSEM 17, 2 (2008).
30. Martin Fowler. 2004. Inversion of control containers and the dependency injection pattern. (2004).
31. Yoshihiko Futamura. 1999. Partial evaluation of computation process–an approach to a compiler-compiler. Higher-Order and Symbolic Computation 12, 4 (1999), 381–391.
32. Patrice Godefroid, Nils Klarlund, and Koushik Sen. 2005. DART: Directed Automated Random Testing. In PLDI.
33. Neville Grech, George Fourtounis, Adrian Francalanza, and Yannis Smaragdakis. 2017. Heaps Don’t Lie: Countering Unsoundness with Heap Snapshots. Proc. ACM Program. Lang. 1, OOPSLA, Article 68 (2017).
34. Neil D Jones, Carsten K Gomard, and Peter Sestoft. 1993. Partial evaluation and automatic program generation. Peter Sestoft.
35. Neil D Jones and Steven S Muchnick. 1979. Flow analysis and optimization of LISP-like structures. In POPL.
36. John B Kam and Jeffrey D Ullman. 1977. Monotone data flow analysis frameworks. Acta Informatica 7, 3 (1977), 305–317.
37. Yoonseok Ko, Hongki Lee, Julian Dolby, and Sukyoung Ryu. 2015. Practically Tunable Static Analysis Framework for LargeScale JavaScript Applications. In ASE.
38. Monica S. Lam, Michael Martin, Benjamin Livshits, and John Whaley. 2008. Securing web applications with static and dynamic information flow tracking. In Partial Evaluation and Semantics-based Program Manipulation.
39. Vincent Laviron and Francesco Logozzo. 2009. Subpolyhedra: A (more) scalable approach to infer linear inequalities. In VMCAI .
40. Yue Li, Tian Tan, and Jingling Xue. 2015. Effective soundness-guided reflection analysis. In SAS.
41. Francesco Logozzo and Manuel Fähndrich. 2008. Pentagons: a weakly relational abstract domain for the efficient validation of array accesses. In Symposium on Applied Computing.
42. Torben Mogensen. 1995. Self-applicable online partial evaluation of the pure lambda calculus. In Symposium on Partial Evaluation and Semantics-based Program Manipulation .
43. Flemming Nielson. 1985. Tensor products generalize the relational data flow analysis method. In 4th Hungarian Computer Science Conference . 211–225.
44. Brianna M. Ren and Jeffrey S. Foster. 2016. Just-in-time Static Type Checking for Dynamic Languages. In PLDI.
45. Koushik Sen and Gul Agha. 2006. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools. In CAV.
46. Koushik Sen, Darko Marinov, and Gul Agha. 2005. CUTE: A Concolic Unit Testing Engine for C. In ESEC/FSE.
47. Yannis Smaragdakis, George Balatsouras, George Kastrinis, and Martin Bravenboer. 2015. More sound static handling of Java reflection. In ASPLAS.
48. Manu Sridharan, Shay Artzi, Marco Pistoia, Salvatore Guarnieri, Omer Tripp, and Ryan Berg. 2011. F4F: Taint Analysis of Framework-based Web Applications. In OOPSLA.
49. Gregory T Sullivan. 2001. Dynamic partial evaluation. In Programs as Data Objects. 238–256.
50. Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vallée-Rai, Patrick Lam, Etienne Gagnon, and Charles Godin. 2000. Practical Virtual Method Call Resolution for Java. In OOPSLA.
51. Alfred Tarski. 1955. A lattice-theoretical fixpoint theorem and its applications. Pacific journal of Mathematics 5, 2 (1955).
52. Antoine Toubhans, Bor-Yuh Evan Chang, and Xavier Rival. 2013. Reduced product combination of abstract domains for shapes. In VMCAI.
53. Shiyi Wei and Barbara G Ryder. 2013. Practical blended taint analysis for JavaScript. In ISSTA.
54. Matteo Zanioli, Pietro Ferrara, and Agostino Cortesi. 2012. SAILS: Static Analysis of Information Leakage with Sample. In Symposium on Applied Computing .

Index Terms

• Software and its engineering

  • Software notations and tools

    • General programming languages

      • Language features

        • Frameworks

  • Software organization and properties

    • Software functional properties

      • Formal methods

        • Automated static analysis