Reference Abstract Domains and Applications to String Analysis

• Autorzy: Amadini R. , Gange G. , Gauthier F. , Jordan A. , Schachte P. , Søndergaard H. , Stuckey P. J. , Zhang C.

Identyfikatory

DOI

10.3233/FI-2018-1650

• Języki publikacji: EN

Abstrakty

EN

Abstract interpretation is a well established theory that supports reasoning about the run-time behaviour of programs. It achieves tractable reasoning by considering abstractions of run-time states, rather than the states themselves. The chosen set of abstractions is referred to as the abstract domain. We develop a novel framework for combining (a possibly large number of) abstract domains. It achieves the effect of the so-called reduced product without requiring a quadratic number of functions to translate information among abstract domains. A central notion is a reference domain, a medium for information exchange. Our approach suggests a novel and simpler way to manage the integration of large numbers of abstract domains. We instantiate our framework in the context of string analysis. Browser-embedded dynamic programming languages such as JavaScript and PHP encourage the use of strings as a universal data type for both code and data values. The ensuing vulnerabilities have made string analysis a focus of much recent research. String analysis tends to combine many elementary string abstract domains, each designed to capture a specific aspect of strings. For this instance the set of regular languages, while too expensive to use directly for analysis, provides an attractive reference domain, enabling the efficient simulation of reduced products of multiple string abstract domains.

Słowa kluczowe

EN

programming languages; domain-specific programming languages; information sharing; javascript; dynamic programming

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2018
• Tom: Vol. 158, nr 4
• Strony: 297--326
• Opis fizyczny: Bibliogr. 37 poz., rys.

Twórcy

autor

Amadini R.

• School of Computing and Information Systems, The University of Melbourne, Australia

autor

Gange G.

• School of Computing and Information Systems, The University of Melbourne, Australia

autor

Gauthier F.

• Oracle Labs, Brisbane, Australia

autor

Jordan A.

• Oracle Labs, Brisbane, Australia

autor

Schachte P.

• School of Computing and Information Systems, The University of Melbourne, Australia

autor

Søndergaard H.

• School of Computing and Information Systems, The University of Melbourne, Australia

autor

Stuckey P. J.

• School of Computing and Information Systems, The University of Melbourne, Australia

autor

Zhang C.

• College of Information Science and Technology, Jinan University, Guangzhou, China

Bibliografia

• [1] Amadini R, Jordan A, Gange G, Gauthier F, Schachte P, Søndergaard H, Stuckey PJ, and Zhang Ch. Combining string abstract domains for JavaScript analysis: An evaluation. In A. Legay and T. Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 10205 of Lecture Notes in Computer Science, pages 41-57. Springer, 2017. URL https://doi.org/10.1007/978-3-662-54577-5_3.
• [2] Bartzis C, and Bultan T. Widening arithmetic automata. In R. Alur and D. A. Peled, editors, Computer Aided Verification, volume 3114 of Lecture Notes in Computer Science, pages 321-333. Springer, 2004. URL https://doi.org/10.1007/978-3-540-27813-9_25.
• [3] Bisht P, Hinrichs TL, Skrupsky N, and Venkatakrishnan VN. WAPTEC: Whitebox analysis of web applications for parameter tampering exploit construction. In Proceedings of the 18th ACM Conference on Computer and Communications Security, pages 575-586. ACM Publ., 2011.
• [4] Bjørner N, Tillmann N, and Voronkov A. Path feasibility analysis for string-manipulating programs. In S. Kowalewski and A. Philippou, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 5505 of Lecture Notes in Computer Science, pages 307-321. Springer, 2009. URL https://doi.org/10.1007/978-3-642-00768-2_27.
• [5] Bruynooghe M. A practical framework for the abstract interpretation of logic programs. Journal of Logic Programming, 1991;10(2):91-124. doi:10.1016/0743-1066(91)80001-T.
• [6] Christensen AS, Møller A, and Schwartzbach MI. Precise analysis of string expressions. In R. Cousot, editor, Static Analysis, volume 2694 of Lecture Notes in Computer Science, pages 1-18. Springer, 2003. ISBN:3-540-40325-6.
• [7] Cortesi A, Costantini G, and Ferrara P. A survey on product operators in abstract interpretation. In Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, pages 325-336, 2013. doi:10.4204/EPTCS.129.19.
• [8] Cortesi A, Filé G, and Winsborough W. Comparison of abstract interpretations. In W. Kuich, editor, Automata, Languages and Programming: Proceedings of the 19th International Colloquium (ICALP’92), volume 623 of Lecture Notes in Computer Science, pages 521-532. Springer, 1992. URL https://doi.org/10.1007/3-540-55719-9_101.
• [9] Cortesi A, Le Charlier B, and Van Hentenryck P. Combinations of abstract domains for logic programming: Open product and generic pattern construction. Science of Computer Programming, 2000;38(1-3):27-71. URL https://doi.org/10.1016/S0167-6423(99)00045-3.
• [10] Costantini G. Lexical and numerical domains for abstract interpretation, PhD Thesis, Ca’ Foscari University of Venice, 2014.
• [11] Costantini G, Ferrara P, and Cortesi A. Static analysis of string values. In S. Qin and Z. Qiu, editors, Formal Methods and Software Engineering, volume 6991 of Lecture Notes in Computer Science, pages 505-521. Springer, 2011. URL https://doi.org/10.1007/978-3-642-24559-6_34.
• [12] Costantini G, Ferrara P, and Cortesi A. A suite of abstract domains for static analysis of string values. Software Practice and Experience, 2015;45(2):245-287. doi:10.1002/spe.2218.
• [13] Cousot P, and Cousot R. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the Fourth ACM Symposium on Principles of Programming Languages, pages 238-252. ACM Publ., 1977. doi:10.1145/512950.512973.
• [14] Cousot P, and Cousot R. Systematic design of program analysis frameworks. In Proceedings of the Sixth Annual ACM Symposium on Principles of Programming Languages, pages 269-282. ACM Publ., 1979. doi:10.1145/567752.567778.
• [15] Cousot P, and Cousot R. Abstract interpretation frameworks. Journal of Logic and Computation, 1992;2(4):511-547. doi:10.1093/logcom/2.4.511.
• [16] Cousot P, Cousot R, Feret J, Mauborgne L, Miné A, Monniaux D, and Rival X. Combination of abstractions in the ASTRÉE static analyzer. In M. Okada and I. Satoh, editors, Advances in Computer Science - ASIAN 2006. Secure Software and Related Issues, volume 4435 of Lecture Notes in Computer Science, pages 272-300. Springer, 2006. URL https://doi.org/10.1007/978-3-540-77505-8_23.
• [17] Patrick Cousot, Radhia Cousot, and Laurent Mauborgne. A framework for combining algebraic and logical abstract interpretations. September 2010. URL https://hal.inria.fr/inria-00543890.
• [18] Cousot P, and Halbwachs N. Automatic discovery of linear restraints among variables of a program. In Proceedings of the 5th Annual ACM Symposium on Principles of Programming Languages, pages 84-96. ACM Publ., 1978. doi:10.1145/512760.512770.
• [19] Emmi M, Majumdar R, and Sen K. Dynamic test input generation for database applications. In Proceedings of the 2007 International Symposium on Software Testing and Analysis, pages 151-162. ACM Publ., 2007. ISBN:978-1-59593-734-6. doi:10.1145/1273463.1273484.
• [20] Gange G, Navas JA, Schachte P, Søndergaard H, and Stuckey PJ. Abstract interpretation over non-lattice abstract domains. In F. Logozzo and M. Fähndrich, editors, Static Analysis, volume 7935 of Lecture Notes in Computer Science, pages 6-24. Springer, 2013. URL https://doi.org/10.1007/978-3-642-38856-9_3.
• [21] Gange G, Navas JA, Stuckey PJ, Søndergaard H, and Schachte P. Unbounded model-checking with interpolation for regular language constraints. In N. Piterman and S. Smolka, editors, Tools and Algorithms for the Construction and Analysis of Systems, volume 7795 of Lecture Notes in Computer Science, pages 277-291. Springer, 2013. URL https://doi.org/10.1007/978-3-642-36742-7_20.
• [22] Granger P. Improving the results of static analyses of programs by local decreasing iterations. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 68-79. Springer, 1992. URL https://doi.org/10.1007/3-540-56287-7_95.
• [23] Gulwani S, and Tiwari A. Combining abstract interpreters. In Proceedings of the 27th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 376-386. ACM Publ., 2006. doi:10.1145/1133255.1134026.
• [24] Jensen SH, Møller A, and Thiemann P. Type analysis for JavaScript. In J. Palsberg and Z. Su, editors, Static Analysis, volume 5673 of Lecture Notes in Computer Science, pages 238-255. Springer, 2009. ISBN: 978-3-642-03236-3. doi:10.1007/978-3-642-03237-0_17.
• [25] Karr M. Affine relationships among variables of a program. Acta Informatica, 1976;6:133-151. URL https://doi.org/10.1007/BF00268497.
• [26] Kashyap V, Dewey K, Kuefner EA, Wagner J, Gibbons K, Sarracino J, Wiedermann B, and Hardekopf B. JSAI: A static analysis platform for JavaScript. In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, pages 121-132. ACM Publ., 2014. ISBN: 978-1-4503-3056-5. doi:10.1145/2635868.2635904.
• [27] Kim S-W, Chin W, Park J, Kim J, and Ryu S. Inferring grammatical summaries of string values. In J. Garrigue, editor, Programming Languages and Systems: Proceedings of the 12th Asian Symposium (APLAS’14), volume 8858 of Lecture Notes in Computer Science, pages 372-391. Springer, 2014. URL https://doi.org/10.1007/978-3-319-12736-1_20.
• [28] Le Charlier B, and Van Hentenryck P. Reexecution in abstract interpretation of Prolog. In K. Apt, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium, pages 750-764. MIT Press, 1992.
• [29] Lee H, Won S, Jin J, Cho J, and Ryu S. SAFE: Formal specification and implementation of a scalable analysis framework for ECMAScript. In Proceedings of the 19th International Workshop on Foundations of Object-Oriented Languages (FOOL’12), 2012.
• [30] Madsen M, and Andreasen E. String analysis for dynamic field access. In A. Cohen, editor, Compiler Construction, volume 8409 of Lecture Notes in Computer Science, pages 197-217. Springer, 2014. URL https://doi.org/10.1007/978-3-642-54807-9_12.
• [31] Marriott K, and Søndergaard H. On propagation-based analysis of logic programs. In S. Michaylov and W. Winsborough, editors, Proceedings of the ILPS 93 Workshop on Global Compilation, pages 47-65, 1993.
• [32] Minamide Y. Static approximation of dynamically generated web pages. In Proceedings of the 14th International Conference on World Wide Web, pages 432-441. ACM Publ., 2005. ISBN:1-59593-046-9. doi:10.1145/1060745.1060809.
• [33] Park Ch, Im H, and Ryu S. Precise and scalable static analysis of jQuery using a regular expression domain. In Proceedings of the 12th Symposium on Dynamic Languages, pages 25-36. ACM Publ., 2016. ISBN: 978-1-4503-4445-6. doi:10.1145/2989225.2989228.
• [34] Polya G. How to Solve It. Doubleday Anchor Books, second edition, 1957.
• [35] Sedgewick R, and Wayne K. Algorithms. Addison-Wesley, fourth edition, 2011.
• [36] Sipser M. Introduction to the Theory of Computation. Thomson Course Technology, third edition, 2012. ISBN-10:113318779X, 13:978-1133187790.
• [37] Veanes M, de Halleux P, and Tillmann N. Rex: Symbolic regular expression explorer. In Proceedings of the Third International Conference on Software Testing, Verification and Validation, pages 498-507. IEEE Comp. Soc., 2010. doi:10.1109/ICST.2010.15.

Uwagi

Opracowanie rekordu w ramach umowy 509/P-DUN/2018 ze środków MNiSW przeznaczonych na działalność upowszechniającą naukę (2018).