Document Open Access Logo

Eventually Sound Points-To Analysis with Specifications

Authors Osbert Bastani, Rahul Sharma, Lazaro Clapp, Saswat Anand, Alex Aiken

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2019.11.pdf
  • Filesize: 0.68 MB
  • 28 pages

Document Identifiers

Author Details

Osbert Bastani
  • University of Pennsylvania, Philadelphia, USA
Rahul Sharma
  • Microsoft Research, Bangalore, India
Lazaro Clapp
  • Stanford University, USA
Saswat Anand
  • Stanford University, USA
Alex Aiken
  • Stanford University, USA

Acknowledgements

This work was supported by NSF grant CCF-1160904, and is also based on research sponsored by the Air Force Research Laboratory, under agreement number FA8750-12-2-0020. The U.S. Government is authorized to reproduce and distribute reprints for Governmental purposes notwithstanding any copyright notation thereon.

Cite AsGet BibTex

Osbert Bastani, Rahul Sharma, Lazaro Clapp, Saswat Anand, and Alex Aiken. Eventually Sound Points-To Analysis with Specifications. In 33rd European Conference on Object-Oriented Programming (ECOOP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 134, pp. 11:1-11:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ECOOP.2019.11

Abstract

Static analyses make the increasingly tenuous assumption that all source code is available for analysis; for example, large libraries often call into native code that cannot be analyzed. We propose a points-to analysis that initially makes optimistic assumptions about missing code, and then inserts runtime checks that report counterexamples to these assumptions that occur during execution. Our approach guarantees eventual soundness, which combines two guarantees: (i) the runtime checks are guaranteed to catch the first counterexample that occurs during any execution, in which case execution can be terminated to prevent harm, and (ii) only finitely many counterexamples ever occur, implying that the static analysis eventually becomes statically sound with respect to all remaining executions. We implement Optix, an eventually sound points-to analysis for Android apps, where the Android framework is missing. We show that the runtime checks added by Optix incur low overhead on real programs, and demonstrate how Optix improves a client information flow analysis for detecting Android malware.

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
Keywords
  • specification inference
  • static points-to analysis
  • runtime monitoring

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. Karim Ali and Ondřej Lhoták. Averroes: Whole-program analysis without the whole program. In ECOOP, 2013. Google Scholar
  3. Lars Ole Andersen. Program analysis and specialization for the C programming language. PhD thesis, University of Cophenhagen, 1994. Google Scholar
  4. Steven Arzt and Eric Bodden. StubDroid: automatic inference of precise data-flow summaries for the android framework. In Software Engineering (ICSE), 2016 IEEE/ACM 38th International Conference on, pages 725-735. IEEE, 2016. Google Scholar
  5. 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. PLDI, 2014. Google Scholar
  6. Thomas H Austin and Cormac Flanagan. Multiple facets for dynamic information flow. In POPL, 2012. Google Scholar
  7. Osbert Bastani, Saswat Anand, and Alex Aiken. Interactively verifying absence of explicit information flows in Android apps. OOPSLA, 2015. Google Scholar
  8. Osbert Bastani, Saswat Anand, and Alex Aiken. Specification inference using context-free language reachability. In POPL, 2015. Google Scholar
  9. Osbert Bastani, Rahul Sharma, Alex Aiken, and Percy Liang. Active Learning of Points-To Specifications. In PLDI, 2018. Google Scholar
  10. 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
  11. Maria Christakis, Peter Müller, and Valentin Wüstholz. Collaborative verification and testing with explicit assumptions. In International Symposium on Formal Methods, pages 132-146. Springer, 2012. Google Scholar
  12. Lazaro Clapp, Saswat Anand, and Alex Aiken. Modelgen: mining explicit information flow specifications from concrete executions. In ISSTA, 2015. Google Scholar
  13. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL, 1977. Google Scholar
  14. Willem De Groef, Dominique Devriese, Nick Nikiforakis, and Frank Piessens. FlowFox: a web browser with flexible and precise information flow control. In CCS, 2012. Google Scholar
  15. David Devecsery, Peter M Chen, Jason Flinn, and Satish Narayanasamy. Optimistic Hybrid Analysis: Accelerating Dynamic Analysis through Predicated Static Analysis. In Proceedings of the Twenty-Third International Conference on Architectural Support for Programming Languages and Operating Systems, pages 348-362. ACM, 2018. Google Scholar
  16. Dominique Devriese and Frank Piessens. Noninterference through Secure Multi-execution. In IEEE Symposium on Security and Privacy, 2010. Google Scholar
  17. Manuel Egele, David Brumley, Yanick Fratantonio, and Christopher Kruegel. An empirical study of cryptographic misuse in android applications. In CCS, 2013. Google Scholar
  18. 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. TOCS, 2014. Google Scholar
  19. Facebook. Adding models, 2017. URL: http://fbinfer.com/docs/adding-models.html.
  20. Sascha Fahl, Marian Harbach, Thomas Muders, Lars Baumgärtner, Bernd Freisleben, and Matthew Smith. Why Eve and Mallory love Android: An analysis of Android SSL (in) security. In CCS, 2012. Google Scholar
  21. Yu Feng, Saswat Anand, Isil Dillig, and Alex Aiken. Apposcopy: Semantics-based detection of android malware through static analysis. In FSE, 2014. Google Scholar
  22. Cormac Flanagan. Hybrid type checking. In POPL, 2006. Google Scholar
  23. Adam P Fuchs, Avik Chaudhuri, and Jeffrey S Foster. Scandroid: Automated security certification of android, 2009. Google Scholar
  24. Google. UI/Application Exerciser Monkey, 2016. URL: https://developer.android.com/studio/test/monkey.html.
  25. 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. Citeseer, 2015. Google Scholar
  26. Ben Gruver. Smali project homepage, 2016. URL: https://github.com/JesusFreke/smali.
  27. Sumit Gulwani. Automating string processing in spreadsheets using input-output examples. In POPL, 2011. Google Scholar
  28. Stefan Heule, Manu Sridharan, and Satish Chandra. Mimic: Computing models for opaque code. In FSE, 2015. Google Scholar
  29. Martin Hirzel, Daniel Von Dincklage, Amer Diwan, and Michael Hind. Fast online pointer analysis. TOPLAS, 2007. Google Scholar
  30. Wei Jin and Alessandro Orso. BugRedux: reproducing field failures for in-house debugging. In ICSE, 2012. Google Scholar
  31. Wei Jin and Alessandro Orso. F3: fault localization for field failures. In Proceedings of the 2013 International Symposium on Software Testing and Analysis, pages 213-223. ACM, 2013. Google Scholar
  32. Tessa Lau, Pedro Domingos, and Daniel S Weld. Learning programs from traces using version space algebra. In International Conference on Knowledge Capture, 2003. Google Scholar
  33. Ben Liblit, Alex Aiken, Alice X Zheng, and Michael I Jordan. Bug isolation via remote program sampling. In PLDI, 2003. Google Scholar
  34. Benjamin Livshits, Manu Sridharan, Yannis Smaragdakis, Ondřej Lhoták, J. Nelson Amaral, Bor-Yuh Evan Chang, Samuel Z. Guyer, Uday P. Khedker, Anders Møller, and Dimitrios Vardoulakis. In Defense of Soundiness: A Manifesto. CACM, 2015. Google Scholar
  35. V Benjamin Livshits and Monica S Lam. Finding Security Vulnerabilities in Java Applications with Static Analysis. In Usenix Security, 2005. Google Scholar
  36. Ana Milanova, Atanas Rountev, and Barbara G Ryder. Parameterized object sensitivity for points-to and side-effect analyses for Java. In Software Engineering Notes, 2002. Google Scholar
  37. Bimal Kumar Mishra and Navnit Jha. Fixed period of temporary immunity after run of anti-malicious software on computer nodes. Applied Mathematics and Computation, 2007. Google Scholar
  38. Markus Mock, Manuvir Das, Craig Chambers, and Susan J Eggers. Dynamic points-to sets: A comparison with static analyses and potential applications in program understanding and optimization. In PASTE, 2001. Google Scholar
  39. Patrick Mutchler, Yeganeh Safaei, Adam Doupé, and John C. Mitchell. Target Fragmentation in Android Apps. In IEEE Security and Privacy Workshops, 2016. Google Scholar
  40. Mayur Naik, Alex Aiken, and John Whaley. Effective static race detection for Java. ACM, 2006. Google Scholar
  41. Aseem Rastogi, Nikhil Swamy, Cédric Fournet, Gavin Bierman, and Panagiotis Vekris. Safe & efficient gradual typing for TypeScript. In POPL, volume 50, pages 167-180, 2015. Google Scholar
  42. Andrei Sabelfeld and Andrew C Myers. Language-based information-flow security. IEEE Journal on selected areas in communications, 2003. Google Scholar
  43. Olin Shivers. Control-flow analysis of higher-order languages. PhD thesis, Carnegie Mellon University, 1991. Google Scholar
  44. Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, volume 6, pages 81-92, 2006. Google Scholar
  45. Manu Sridharan and Rastislav Bodík. Refinement-based context-sensitive points-to analysis for Java. In PLDI, 2006. Google Scholar
  46. Manu Sridharan, Denis Gopan, Lexin Shan, and Rastislav Bodík. Demand-driven points-to analysis for Java. In ACM SIGPLAN Notices, volume 40 (10), pages 59-76. ACM, 2005. Google Scholar
  47. Omer Tripp, Marco Pistoia, Stephen J Fink, Manu Sridharan, and Omri Weisman. TAJ: effective taint analysis of web applications. In PLDI, 2009. Google Scholar
  48. Raja Vallée-Rai, Phong Co, Etienne Gagnon, Laurie Hendren, Patrick Lam, and Vijay Sundaresan. Soot-a Java bytecode optimization framework. In Conference of the Centre for Advanced Studies on Collaborative Research, 1999. Google Scholar
  49. John Whaley and Monica S Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI, 2004. Google Scholar
  50. Robert P Wilson and Monica S Lam. Efficient context-sensitive pointer analysis for C programs. In PLDI, 1995. Google Scholar
  51. Yichen Xie and Alex Aiken. Static Detection of Security Vulnerabilities in Scripting Languages. In USENIX Security, 2006. Google Scholar
  52. Haiyan Zhu, Thomas Dillig, and Isil Dillig. Automated inference of library specifications for source-sink property verification. In APLAS, 2013. Google Scholar
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact