Document Open Access Logo

Taming the Static Analysis Beast

Authors John Toman, Dan Grossman

PDF
Thumbnail PDF

File

LIPIcs.SNAPL.2017.18.pdf
  • Filesize: 0.58 MB
  • 14 pages

Document Identifiers

Author Details

John Toman
Dan Grossman

Cite AsGet BibTex

John Toman and Dan Grossman. Taming the Static Analysis Beast. In 2nd Summit on Advances in Programming Languages (SNAPL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 71, pp. 18:1-18:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.SNAPL.2017.18

Abstract

While industrial-strength static analysis over large, real-world codebases has become commonplace, so too have difficult-to-analyze language constructs, large libraries, and popular frameworks. These features make constructing and evaluating a novel, sound analysis painful, error-prone, and tedious. We motivate the need for research to address these issues by highlighting some of the many challenges faced by static analysis developers in today's software ecosystem. We then propose our short- and long-term research agenda to make static analysis over modern software less burdensome.
Keywords
  • static analysis
  • frameworks
  • api knowledge
  • library specifications

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Aws Albarghouthi, Isil Dillig, and Arie Gurfinkel. Maximal specification synthesis. In POPL, 2016. Google Scholar
  2. Jade Alglave, Anthony Fox, Samin Ishtiaq, Magnus O. Myreen, Susmit Sarkar, Peter Sewell, and Francesco Zappa Nardelli. The semantics of Power and ARM multiprocessor machine code. In DAMP, 2009. Google Scholar
  3. Jade Alglave, Luc Maranget, Susmit Sarkar, and Peter Sewell. Fences in weak memory models. In CAV, 2010. Google Scholar
  4. Lars Ole Andersen. Program analysis and specialization for the C programming language. PhD thesis, University of Cophenhagen, 1994. Google Scholar
  5. Steven Arzt and Eric Bodden. Reviser: efficiently updating IDE-/IFDS-based data-flow analyses in response to incremental program changes. In ICSE, 2014. Google Scholar
  6. Steven Arzt and Eric Bodden. Stubdroid: automatic inference of precise data-flow summaries for the android framework. In ICSE, 2016. Google Scholar
  7. Steven Arzt, Siegfried Rasthofer, Christian Fritz, 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 PLDI, 2014. Google Scholar
  8. Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, and William Pugh. Using static analysis to find bugs. IEEE software, 25(5), 2008. Google Scholar
  9. Davide Balzarotti, Marco Cova, Vika Felmetsger, Nenad Jovanovic, Engin Kirda, Christopher Kruegel, and Giovanni Vigna. Saner: Composing static and dynamic analysis to validate sanitization in web applications. In Symposium on Security and Privacy, 2008. Google Scholar
  10. Osbert Bastani, Saswat Anand, and Alex Aiken. Specification inference using context-free language reachability. In POPL, 2015. Google Scholar
  11. Sam Blackshear, Alexandra Gendreau, and Bor-Yuh Evan Chang. Droidel: A general approach to android framework modeling. In Proceedings of the 4th ACM SIGPLAN International Workshop on State Of the Art in Program Analysis, 2015. Google Scholar
  12. Sam Blackshear and Shuvendu K. Lahiri. Almost-correct specifications: A modular semantic framework for assigning confidence to warnings. In PLDI, 2013. Google Scholar
  13. Eric Bodden, Andreas Sewe, Jan Sinschek, Hela Oueslati, and Mira Mezini. Taming reflection: Aiding static analysis in the presence of reflection and custom class loaders. In ICSE, 2011. Google Scholar
  14. James Bornholt and Emina Torlak. Synthesizing memory models from framework sketches and litmus tests. In PLDI, 2017. Google Scholar
  15. David Brumley, Ivan Jager, Thanassis Avgerinos, and Edward J Schwartz. Bap: A binary analysis platform. In CAV, 2011. Google Scholar
  16. Cristiano Calcagno and Dino Distefano. Infer: an automatic program verifier for memory safety of C programs. In NASA Formal Methods Symposium, 2011. Google Scholar
  17. Cristiano Calcagno, Dino Distefano, and Peter O'Hearn. Open-sourcing facebook infer: Identify bugs before you ship. https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/, 2015.
  18. Ravi Chugh, Jeffrey A. Meister, Ranjit Jhala, and Sorin Lerner. Staged information flow for Javascript. In PLDI, 2009. Google Scholar
  19. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement. In CAV, 2000. Google Scholar
  20. Patrick Cousot and Radhia Cousot. Modular static program analysis. In International Conference on Compiler Construction, 2002. Google Scholar
  21. Ankush Das, Shuvendu K. Lahiri, Akash Lal, and Yi Li. Angelic verification: Precise verification modulo unknowns. In CAV, 2015. Google Scholar
  22. Leonardo De Moura and Nikolaj Bjørner. Z3: An efficient smt solver. In TACAS, 2008. Google Scholar
  23. Isil Dillig, Thomas Dillig, and Alex Aiken. Precise reasoning for programs using containers. In POPL, 2011. Google Scholar
  24. Bruno Dufour, Barbara G. Ryder, and Gary Sevitsky. Blended analysis for performance understanding of framework-based applications. In ISSTA, 2007. Google Scholar
  25. William Enck, Peter Gilbert, Seungyeop Han, Vasant Tendulkar, Byung-Gon Chun, Landon P. Cox, Jaeyeon Jung, Patrick McDaniel, and Anmol N. Sheth. Taintdroid: an information-flow tracking system for realtime privacy monitoring on smartphones. ACM Transactions on Computer Systems (TOCS), 32(2), 2014. Google Scholar
  26. Stephen J. Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ACM Transactions on Software Engineering and Methodology (TOSEM), 17(2), 2008. Google Scholar
  27. Apache Foundation. Apache struts 2. URL: https://struts.apache.org/.
  28. Adam P. Fuchs, Avik Chaudhuri, and Jeffrey S. Foster. Scandroid: Automated security certification of android. Technical Report CS-TR-4991, University of Maryland, November 2009. Google Scholar
  29. Patrice Godefroid, Peli de Halleux, Aditya V. Nori, Sriram K. Rajamani, Wolfram Schulte, Nikolai Tillmann, and Michael Y. Levin. Automating software testing using program analysis. IEEE software, 25(5), 2008. Google Scholar
  30. Patrice Godefroid, Nils Klarlund, and Koushik Sen. Dart: Directed automated random testing. In PLDI, 2005. Google Scholar
  31. Michael I. Gordon, Deokhwan Kim, Jeff H. Perkins, Limei Gilham, Nguyen Nguyen, and Martin C. Rinard. Information flow analysis of android applications in droidsafe. In NDSS, 2015. Google Scholar
  32. Sumit Gulwani and Ashish Tiwari. Computing procedure summaries for interprocedural analysis. In ESOP, 2007. Google Scholar
  33. Ben Hardekopf and Calvin Lin. Flow-sensitive pointer analysis for millions of lines of code. In CGO, 2011. Google Scholar
  34. Ben Hardekopf, Ben Wiedermann, Berkeley Churchill, and Vineeth Kashyap. Widening for control-flow. In International Conference on Verification, Model Checking, and Abstract Interpretation, 2014. Google Scholar
  35. Brittany Johnson, Yoonki Song, Emerson Murphy-Hill, and Robert Bowdidge. Why don't software developers use static analysis tools to find bugs? In ICSE, 2013. Google Scholar
  36. Vineet Kahlon, Yu Yang, Sriram Sankaranarayanan, and Aarti Gupta. Fast and accurate static data-race detection for concurrent programs. In CAV, 2007. Google Scholar
  37. Vineeth Kashyap, Kyle Dewey, Ethan A. Kuefner, John Wagner, Kevin Gibbons, John Sarracino, Ben Wiedermann, and Ben Hardekopf. Jsai: a static analysis platform for javascript. In FSE, 2014. Google Scholar
  38. Yoonseok Ko, Hongki Lee, Julian Dolby, and Sukyoung Ryu. Practically tunable static analysis framework for large-scale javascript applications (t). In ASE, 2015. Google Scholar
  39. Shriram Krishnamurhti. Personal Communication, 2016. Google Scholar
  40. Daniel Kroening, Daniel Poetzl, Peter Schrammel, and Björn Wachter. Sound static deadlock analysis for c/pthreads. In ASE, 2016. Google Scholar
  41. Sulekha Kulkarni, Ravi Mangal, Xin Zhang, and Mayur Naik. Accelerating program analyses by cross-program training. In OOPSLA, 2016. Google Scholar
  42. Monica S. Lam, Michael Martin, Benjamin Livshits, and John Whaley. Securing web applications with static and dynamic information flow tracking. In Partial Evaluation and Semantics-based Program Manipulation, 2008. Google Scholar
  43. James R. Larus, Thomas Ball, Manuvir Das, Robert DeLine, Manuel Fahndrich, Jon Pincus, Sriram K. Rajamani, and Ramanathan Venkatapathy. Righting software. IEEE software, 21(3), 2004. Google Scholar
  44. Johannes Lerch, Johannes Späth, Eric Bodden, and Mira Mezini. Access-path abstraction: Scaling field-sensitive data-flow analysis with unbounded access paths. In ASE, 2015. Google Scholar
  45. Benjamin Livshits, Aditya V. Nori, Sriram K. Rajamani, and Anindya Banerjee. Merlin: Specification inference for explicit information flow problems. In PLDI, 2009. Google Scholar
  46. Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondrej Lhoták, JoséNelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis. In defense of soundiness: a manifesto. Commun. ACM, 58(2), 2015. Google Scholar
  47. Steffen Lortz, Heiko Mantel, Artem Starostin, Timo Bähr, David Schneider, and Alexandra Weber. Cassandra: Towards a certifying app store for android. In Proceedings of the 4th ACM Workshop on Security and Privacy in Smartphones &Mobile Devices, 2014. Google Scholar
  48. Long Lu, Zhichun Li, Zhenyu Wu, Wenke Lee, and Guofei Jiang. Chex: statically vetting android apps for component hijacking vulnerabilities. In Proceedings of the 2012 ACM conference on Computer and communications security, 2012. Google Scholar
  49. Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams. An axiomatic memory model for POWERmultiprocessors. In CAV, 2012. Google Scholar
  50. Scott McPeak, Charles-Henri Gros, and Murali Krishna Ramanathan. Scalable and incremental software bug detection. In FSE, 2013. Google Scholar
  51. Rashmi Mudduluru and Murali Krishna Ramanathan. Efficient incremental static analysis using path abstraction. In FASE, 2014. Google Scholar
  52. George C. Necula, Scott McPeak, Shree P. Rahul, and Westley Weimer. Cil: Intermediate language and tools for analysis and transformation of c programs. In International Conference on Compiler Construction, 2002. Google Scholar
  53. Jeremy W. Nimmer and Michael D. Ernst. Automatic generation of program specifications. In ISSTA, 2002. Google Scholar
  54. Scott Owens, Susmit Sarkar, and Peter Sewell. A better x86 memory model: x86-TSO. In TPHOLs, 2009. Google Scholar
  55. Lori L. Pollock and Mary Lou Soffa. An incremental version of iterative data flow analysis. IEEE Transactions on Software Engineering, 15(12), 1989. Google Scholar
  56. Murali Krishna Ramanathan, Ananth Grama, and Suresh Jagannathan. Static specification inference using predicate mining. In PLDI, 2007. Google Scholar
  57. Michael Reif, Michael Eichberg, Ben Hermann, Johannes Lerch, and Mira Mezini. Call graph construction for java libraries. In FSE, 2016. Google Scholar
  58. Atanas Rountev, Mariana Sharp, and Guoqing Xu. Ide dataflow analysis in the presence of large object-oriented libraries. In International Conference on Compiler Construction, 2008. Google Scholar
  59. Caitlin Sadowski, Jeffrey Van Gogh, Ciera Jaspan, Emma Söderberg, and Collin Winter. Tricorder: Building a program analysis ecosystem. In ICSE, 2015. Google Scholar
  60. Susmit Sarkar, Peter Sewell, Jade Alglave, Luc Maranget, and Derek Williams. Understanding POWER multiprocessors. In PLDI, 2011. Google Scholar
  61. Susmit Sarkar, Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Tom Ridge, Thomas Braibant, Magnus O. Myreen, and Jade Alglave. The semantics of x86-CC multiprocessor machine code. In POPL, 2009. Google Scholar
  62. Koushik Sen and Gul Agha. Cute and jcute: Concolic unit testing and explicit path model-checking tools. In CAV, 2006. Google Scholar
  63. Koushik Sen, Darko Marinov, and Gul Agha. Cute: A concolic unit testing engine for c. In Proceedings of the 10th European Software Engineering Conference Held Jointly with 13th ACM SIGSOFT International Symposium on Foundations of Software Engineering, 2005. Google Scholar
  64. Peter Sewell, Susmit Sarkar, Scott Owens, Francesco Zappa Nardelli, and Magnus O. Myreen. x86-TSO: A rigorous and usable programmer’s model for x86 multiprocessors. Commun. ACM, 53(7), 2010. Google Scholar
  65. Amie L. Souter and Lori L. Pollock. Incremental call graph reanalysis for object-oriented software maintenance. In ICSM, 2001. Google Scholar
  66. Spring framework. URL: http://spring.io/.
  67. Manu Sridharan, Shay Artzi, Marco Pistoia, Salvatore Guarnieri, Omer Tripp, and Ryan Berg. F4f: Taint analysis of framework-based web applications. In OOPSLA, 2011. Google Scholar
  68. Zachary Tatlock, Chris Tucker, David Shuffelton, Ranjit Jhala, and Sorin Lerner. Deep typechecking and refactoring. In OOPSLA, 2008. Google Scholar
  69. Omer Tripp, Marco Pistoia, Patrick Cousot, Radhia Cousot, and Salvatore Guarnieri. Andromeda: Accurate and scalable security analysis of web applications. In FASE, 2013. Google Scholar
  70. Omer Tripp, Marco Pistoia, Stephen J. Fink, Manu Sridharan, and Omri Weisman. Taj: Effective taint analysis of web applications. In PLDI, 2009. Google Scholar
  71. Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot-a java bytecode optimization framework. In Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, 1999. Google Scholar
  72. WALA - T. J. Watson Libraries for Analysis. URL: http://wala.sf.net/.
  73. Shiyi Wei and Barbara G Ryder. Practical blended taint analysis for javascript. In ISSTA, 2013. Google Scholar
  74. John Wickerson, Mark Batty, Tyler Sorensen, and George A Constantinides. Automatically comparing memory consistency models. In POPL, 2017. Google Scholar
  75. Shengqian Yang, Dacong Yan, Haowei Wu, Yan Wang, and Atanas Rountev. Static control-flow analysis of user-driven callbacks in android applications. In ICSE, 2015. Google Scholar
  76. Xin Zhang, Ravi Mangal, Mayur Naik, and Hongseok Yang. Hybrid top-down and bottom-up interprocedural analysis. In PLDI, 2014. Google Scholar
  77. Cong Zheng, Shixiong Zhu, Shuaifu Dai, Guofei Gu, Xiaorui Gong, Xinhui Han, and Wei Zou. Smartdroid: an automatic system for revealing ui-based trigger conditions in android applications. In Proceedings of the second ACM workshop on Security and privacy in smartphones and mobile devices, 2012. Google Scholar
  78. Haiyan Zhu, Thomas Dillig, and Isil Dillig. Automated inference of library specifications for source-sink property verification. In ASPLAS, 2013. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact