Skip to main content
SpringerLink
Log in

Completeness of Abstract Domains for String Analysis of JavaScript Programs

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2019 (ICTAC 2019)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11884))

Included in the following conference series:

Abstract

Completeness in abstract interpretation is a well-known property, which ensures that the abstract framework does not lose information during the abstraction process, with respect to the property of interest. Completeness has been never taken into account for existing string abstract domains, due to the fact that it is difficult to prove it formally. However, the effort is fully justified when dealing with string analysis, which is a key issue to guarantee security properties in many software systems, in particular for JavaScript programs where poorly managed string manipulating code often leads to significant security flaws. In this paper, we address completeness for the main JavaScript-specific string abstract domains, we provide suitable refinements of them, and we discuss the benefits of guaranteeing completeness in the context of abstract-interpretation based string analysis of dynamic languages.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Closing the coalesced sum abstract domain by the powerset operation, a more precise abstract domain is obtained, called union type abstract domain [23], that tracks the set of types of a certain variable during program execution.

  2. 2.

    Floats normally are represented in programming languages in the IEEE 754 double precision format. For the sake of simplicity, we use instead decimal numbers.

  3. 3.

    We abuse notation denoting with \(\llbracket \cdot \rrbracket \) the additive lift to set of basic values of the concrete semantics, i.e., the collecting semantics.

References

  1. Abdulla, P.A., et al.: Norn: an SMT solver for string constraints. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 462–469. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_29

    Chapter  Google Scholar 

  2. Amadini, R., et al.: Reference abstract domains and applications to string analysis. Fundam. Inform. 158(4), 297–326 (2018)

    Article  MathSciNet  Google Scholar 

  3. Amadini, R., Gange, G., Stuckey, P.J., Tack, G.: A novel approach to string constraint solving. In: Beck, J.C. (ed.) CP 2017. LNCS, vol. 10416, pp. 3–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66158-2_1

    Chapter  Google Scholar 

  4. Amadini, R., et al.: Combining string abstract domains for Javascript analysis: an evaluation. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 41–57. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_3

    Chapter  Google Scholar 

  5. Arceri, V., Maffeis, S.: Abstract domains for type Juggling. Electr. Notes Theor. Comput. Sci. 331, 41–55 (2017)

    Article  Google Scholar 

  6. Arceri, V., Mastroeni, I.: Static Program Analysis for String Manipulation Languages. In: VPT 2019 (2019, to appear)

    Article  Google Scholar 

  7. Bultan, T., Yu, F., Alkhalaf, M., Aydin, A.: String Analysis for Software Verification and Security. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68670-7

    Book  Google Scholar 

  8. Chen, L., Miné, A., Cousot, P.: A sound floating-point polyhedra abstract domain. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 3–18. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89330-1_2

    Chapter  Google Scholar 

  9. Christensen, A.S., Møller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol. 2694, pp. 1–18. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-44898-5_1

    Chapter  MATH  Google Scholar 

  10. Clarisó, R., Cortadella, J.: The octahedron abstract domain. Sci. Comput. Program. 64(1), 115–139 (2007)

    Article  MathSciNet  Google Scholar 

  11. Cortesi, A., Olliaro, M.: M-string segmentation: a refined abstract domain for string analysis in C programs. In: TASE 2018, pp. 1–8 (2018)

    Google Scholar 

  12. Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw. Pract. Exper. 45(2), 245–287 (2015)

    Article  Google Scholar 

  13. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL 1977, pp. 238–252 (1977)

    Google Scholar 

  14. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL 1979, pp. 269–282 (1979)

    Google Scholar 

  15. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: POPL 1978, pp. 84–96 (1978)

    Google Scholar 

  16. Filaretti, D., Maffeis, S.: An executable formal semantics of PHP. In: ECOOP 2014 - Object-Oriented Programming - 28th European Conference, Uppsala, Sweden, July 28 - August 1, 2014. Proceedings, pp. 567–592 (2014)

    Google Scholar 

  17. Giacobazzi, R., Ranzato, F., Scozzari, F.: Making abstract interpretations complete. J. ACM 47(2), 361–416 (2000)

    Article  MathSciNet  Google Scholar 

  18. Granger, P.: Static analysis of arithmetical congruences. Int. J. Comput. Math. - IJCM 30, 165–190 (1989)

    Article  Google Scholar 

  19. Granger, P.: Static analysis of linear congruence equalities among variables of a program. In: Abramsky, S., Maibaum, T.S.E. (eds.) CAAP 1991. LNCS, vol. 493, pp. 169–192. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53982-4_10

    Chapter  Google Scholar 

  20. Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03237-0_17

    Chapter  Google Scholar 

  21. Kashyap, V., et al.: JSAI: a static analysis platform for JavaScript. In: FSE 2014, pp. 121–132 (2014)

    Google Scholar 

  22. Kim, S.-W., Chin, W., Park, J., Kim, J., Ryu, S.: Inferring grammatical summaries of string values. In: Garrigue, J. (ed.) APLAS 2014. LNCS, vol. 8858, pp. 372–391. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-12736-1_20

    Chapter  Google Scholar 

  23. Kneuss, E., Suter, P., Kuncak, V.: Phantm: PHP analyzer for type mismatch. In: FSE 2010, pp. 373–374 (2010)

    Google Scholar 

  24. Lee, H., Won, S., Jin, J., Cho, J., Ryu, S.: SAFE: formal specification and implementation of a scalable analysis framework for ECMAScript. In: FOOL 2012 (2012)

    Google Scholar 

  25. Liang, T., Reynolds, A., Tsiskaridze, N., Tinelli, C., Barrett, C., Deters, M.: An efficient SMT solver for string constraints. Formal Methods Syst. Des. 48(3), 206–234 (2016)

    Article  Google Scholar 

  26. Madsen, M., Andreasen, E.: String analysis for dynamic field access. In: CC 2014, pp. 197–217 (2014)

    Google Scholar 

  27. Maffeis, S., Mitchell, J.C., Taly, A.: An operational semantics for JavaScript. In: Ramalingam, G. (ed.) APLAS 2008. LNCS, vol. 5356, pp. 307–325. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-89330-1_22

    Chapter  Google Scholar 

  28. Minamide, Y.: Static approximation of dynamically generated web pages. In: WWW 2005, pp. 432–441 (2005)

    Google Scholar 

  29. Miné, A.: The octagon abstract domain. Higher-Order Symbol. Comput. 19(1), 31–100 (2006)

    Article  Google Scholar 

  30. Oucheikh, R., Berrada, I., Hichami, O.E.: The 4-octahedron abstract domain. In: NETYS 2016, pp. 311–317 (2016)

    Chapter  Google Scholar 

  31. Park, C., Im, H., Ryu, S.: Precise and scalable static analysis of jQuery using a regular expression domain. In: DLS 2016, pp. 25–36 (2016)

    Google Scholar 

  32. Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for JavaScript. In: S&P 2010, pp. 513–528 (2010)

    Google Scholar 

  33. Simon, A., King, A., Howe, J.M.: Two variables per linear inequality as an abstract domain. In: LOPSTR 2002, pp. 71–89 (2002)

    Chapter  Google Scholar 

  34. Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: ICST 2010, pp. 498–507 (2010)

    Google Scholar 

  35. Ward, M.: The closure operators of a lattice. Ann. Math. 43(2), 191–196 (1942)

    Article  MathSciNet  Google Scholar 

  36. Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI 2007, pp. 32–41 (2007)

    Article  Google Scholar 

  37. Yu, F., Alkhalaf, M., Bultan, T., Ibarra, O.H.: Automata-based symbolic string analysis for vulnerability detection. Formal Meth. Syst. Des. 44(1), 44–70 (2014)

    Article  Google Scholar 

  38. Yu, F., Bultan, T., Cova, M., Ibarra, O.H.: Symbolic string verification: an automata-based approach. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 306–324. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-85114-1_21

    Chapter  Google Scholar 

  39. Yu, F., Bultan, T., Hardekopf, B.: String abstractions for string verification. In: Groce, A., Musuvathi, M. (eds.) SPIN 2011. LNCS, vol. 6823, pp. 20–37. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22306-8_3

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Verona, Verona, Italy

    Vincenzo Arceri & Isabella Mastroeni

  2. Ca’ Foscari University of Venice, Venice, Italy

    Martina Olliaro & Agostino Cortesi

  3. Masaryk University of Brno, Brno, Czech Republic

    Martina Olliaro

Authors
  1. Vincenzo Arceri
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Martina Olliaro
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Agostino Cortesi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Isabella Mastroeni
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Vincenzo Arceri , Martina Olliaro , Agostino Cortesi or Isabella Mastroeni .

Editor information

Editors and Affiliations

  1. University of Sheffield, Sheffield, UK

    Robert Mark Hierons

  2. University of Bordeaux, Talence, France

    Mohamed Mosbah

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Arceri, V., Olliaro, M., Cortesi, A., Mastroeni, I. (2019). Completeness of Abstract Domains for String Analysis of JavaScript Programs. In: Hierons, R., Mosbah, M. (eds) Theoretical Aspects of Computing – ICTAC 2019. ICTAC 2019. Lecture Notes in Computer Science(), vol 11884. Springer, Cham. https://doi.org/10.1007/978-3-030-32505-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-32505-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-32504-6

  • Online ISBN: 978-3-030-32505-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation