Skip to main content
SpringerLink
Log in

LiSA: A Generic Framework for Multilanguage Static Analysis

  • Chapter
  • First Online:
Challenges of Software Verification

Part of the book series: Intelligent Systems Reference Library ((ISRL,volume 238))

Abstract

Modern software engineering revolves around distributed applications. From IoT networks to client-server infrastructures, the application code is increasingly being divided into separate sub-programs interacting with each other. As they are completely independent from each other, each such program is likely to be developed in a separate programming language, choosing the best fit for the task to at hand. From a static program analysis perspective, taking on a mixture of languages is challenging. This paper defines a generic framework where modular multilanguage static analyses can be defined through the abstract interpretation theory. The framework has been implemented in LiSA (Library for Static Analysis), an open-source Java library that provides the complete infrastructure necessary for developing static analyzers. LiSA strives to be modular, ensuring that all components taking part in the analysis are both easy to develop and highly interchangeable. LiSA also ensures that components are parametric to all language-specific features: semantics, execution model, and memory model are not directly encoded within the components themselves. A proof-of-concept instantiation is provided, demonstrating LiSA’s capability to analyze multiple languages in a single analysis through the discovery of an IoT vulnerability spanning C++ and Java code.

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 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Allen, F.E.: Control flow analysis. In: Proceedings of a Symposium on Compiler Optimization, pp. 1–19. Association for Computing Machinery, New York, NY, USA (1970). https://doi.org/10.1145/800028.808479

  2. Andersen, L.O.: Program analysis and specialization for the c programming language. Ph.D. thesis, DIKU, University of Copenhagen (1994). https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.109.6502 &rep=rep1 &type=pdf

  3. Androulaki, E., Barger, A., Bortnikov, V., Cachin, C., Christidis, K., Caro, A.D., Enyeart, D., Ferris, C., Laventman, G., Manevich, Y., Muralidharan, S., Murthy, C., Nguyen, B., Sethi, M., Singh, G., Smith, K., Sorniotti, A., Stathakopoulou, C., Vukolic, M., Cocco, S.W., Yellick, J.: Hyperledger fabric: a distributed operating system for permissioned blockchains. In: Oliveira, R., Felber, P., Hu, Y.C. (eds.) Proceedings of the Thirteenth EuroSys Conference, EuroSys 2018, Porto, Portugal, 23–26 Apr. 2018, pp. 30:1–30:15. ACM (2018). https://doi.org/10.1145/3190508.3190538

  4. Arceri, V., Maffeis, S.: Abstract domains for type juggling. Electron. Notes Theor. Comput. Sci. 331, 41–55 (2017). DOI: 10.1016/j.entcs.2017.02.003.

    Article  MATH  Google Scholar 

  5. Bacon, D.F., Sweeney, P.F.: Fast static analysis of c++ virtual function calls. In: Proceedings of the 11th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ’96, pp. 324–341. Association for Computing Machinery, New York, NY, USA (1996). https://doi.org/10.1145/236337.236371

  6. Bagnara, R., Hill, P.M., Zaffanella, E.: The parma polyhedra library: toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems. Sci. Comput. Program. 72(1), 3–21 (2008). https://doi.org/10.1016/j.scico.2007.08.001. https://www.sciencedirect.com/science/article/pii/S0167642308000415. Special Issue on Second issue of experimental software and toolkits (EST)

  7. Buchman, E.: Tendermint: Byzantine fault tolerance in the age of blockchains. Ph.D. thesis, University of Guelph (2016). https://atrium.lib.uoguelph.ca/xmlui/handle/10214/9769

  8. Buro, S., Crole, R.L., Mastroeni, I.: On multi-language abstraction. In: Pichardie, D., Sighireanu, M. (eds.) Static Analysis, pp. 310–332. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-65474-0_14

  9. Buro, S., Mastroeni, I.: On the multi-language construction. In: Caires, L. (ed.) Programming Languages and Systems, pp. 293–321. Springer International Publishing, Cham (2019). https://doi.org/10.1007/978-3-030-17184-1_11

  10. Chen, L.: Microservices: Architecting for continuous delivery and devops. In: 2018 IEEE International Conference on Software Architecture (ICSA), pp. 39–397 (2018). https://doi.org/10.1109/ICSA.2018.00013

  11. Cortesi, A., Costantini, G., Ferrara, P.: A survey on product operators in abstract interpretation. Electronic Proceedings in Theoretical Computer Science 129, 325–336 (2013). https://doi.org/10.4204/eptcs.129.19

  12. Costantini, G., Ferrara, P., Cortesi, A.: A suite of abstract domains for static analysis of string values. Softw.: Pract. Exp. 45(2), 245–287 (2015). https://doi.org/10.1002/spe.2218. https://onlinelibrary.wiley.com/doi/abs/10.1002/spe.2218

  13. Cousot, P.: Principles of Abstract Interpretation. MIT Press (2021)

    Google Scholar 

  14. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Graham, R.M., Harrison, M.A., Sethi, R. (eds.) Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, CA, USA, Jan. 1977, pp. 238–252. ACM (1977). https://doi.org/10.1145/512950.512973

  15. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: Aho, A.V., Zilles, S.N., Rosen, B.K. (eds.) Conference Record of the Sixth Annual ACM Symposium on Principles of Programming Languages, San Antonio, Texas, USA, Jan. 1979, pp. 269–282. ACM Press (1979). https://doi.org/10.1145/567752.567778

  16. Cousot, P., Cousot, R.: Modular static program analysis. In: R.N. Horspool (ed.) Compiler Construction, pp. 159–179. Springer, Berlin, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_13

  17. Cousot, P., Halbwachs, N.: Automatic discovery of linear restraints among variables of a program. In: Aho, A.V., Zilles, S.N., Szymanski, T.G. (eds.) Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages, Tucson, Arizona, USA, Jan. 1978, pp. 84–96. ACM Press (1978). https://doi.org/10.1145/512760.512770

  18. Dean, J., Grove, D., Chambers, C.: Optimization of object-oriented programs using static class hierarchy analysis. In: Tokoro, M., Pareschi, R. (eds.) ECOOP’95—Object-Oriented Programming, 9th European Conference, Åarhus, Denmark, 7–11 Aug. 1995, pp. 77–101. Springer, Berlin, Heidelberg (1995). https://doi.org/10.1007/3-540-49538-X_5

  19. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976). https://doi.org/10.1145/360051.360056

  20. Distefano, D., Fähndrich, M., Logozzo, F., O’Hearn, P.W.: Scaling static analyses at facebook. Commun. the ACM 62(8), 62–70 (2019). https://doi.org/10.1145/3338112

    Article  Google Scholar 

  21. Ernst, M.D., Lovato, A., Macedonio, D., Spiridon, C., Spoto, F.: Boolean formulas for the static identification of injection attacks in java. In: Davis, A. Fehnker, A. McIver, A. Voronkov (eds.) Logic for Programming, Artificial Intelligence, and Reasoning, pp. 130–145. Springer, Berlin, Heidelberg (2015). 978-3-662-48899-7_10

    Google Scholar 

  22. Ferrara, P.: A generic framework for heap and value analyses of object-oriented programming languages. Theor. Comput. Sci. 631, 43–72 (2016). https://doi.org/10.1016/j.tcs.2016.04.001. www.sciencedirect.com/science/article/pii/S0304397516300299

  23. Ferrara, P., Cortesi, A., Spoto, F.: Cil to java-bytecode translation for static analysis leveraging. In: Proceedings of the 6th Conference on Formal Methods in Software Engineering, FormaliSE ’18, pp. 40–49. Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3193992.3193994

  24. Ferrara, P., Mandal, A.K., Cortesi, A., Spoto, F.: Cross-programming language taint analysis for the iot ecosystem. Electron. Commun. EASST 77 (2019). 10.14279/tuj.eceasst.77.1104

    Google Scholar 

  25. Ferrara, P., Negrini, L.: Sarl: Oo framework specification for static analysis. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds.) Software Verification, pp. 3–20. Springer International Publishing, Cham (2020). 10.1007/978-3-030-63618-0_1

    Google Scholar 

  26. Ferrara, P., Negrini, L., Arceri, V., Cortesi, A.: Static analysis for dummies: experiencing lisa. In: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2021, pp. 1–6. Association for Computing Machinery, New York, NY, USA (2021). https://doi.org/10.1145/3460946.3464316

  27. Furr, M., Foster, J.S.: Polymorphic type inference for the JNI. In: Sestoft, P. (ed.) Programming Languages and Systems, pp. 309–324. Springer, Berlin, Heidelberg (2006). https://doi.org/10.1007/11693024_21

  28. Furr, M., Foster, J.S.: Checking type safety of foreign function calls. ACM Trans. Program. Lang. Syst. 30(4) (2008). https://doi.org/10.1145/1377492.1377493

  29. Jeannet, B., Miné, A.: Apron: A library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, pp. 661–667. Springer, Berlin, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_52

  30. Journault, M., Miné, A., Monat, R., Ouadjaout, A.: Combinations of reusable abstract domains for a multilingual static analyzer. In: Chakraborty, S., Navas, J.A. (eds.) Verified Software. Theories, Tools, and Experiments, pp. 1–18. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-41600-3_1

  31. Khedker, U.P., Karkare, B.: Efficiency, precision, simplicity, and generality in interprocedural data flow analysis: Resurrecting the classical call strings method. In: Hendren, L. (ed.) Compiler Construction, pp. 213–228. Springer, Berlin, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78791-4_15

  32. Kwon, J.: Tendermint: Consensus Without Mining (2014). https://tendermint.com/static/docs/tendermint.pdf

  33. Kwon, J., Buchman, E.: Cosmos Whitepaper (2019). https://v1.cosmos.network/resources/whitepaper

  34. Lee, S., Lee, H., Ryu, S.: Broadening horizons of multilingual static analysis: semantic summary extraction from c code for JNI program analysis. In: Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering, ASE ’20, pp. 127–137. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3324884.3416558

  35. Li, S., Tan, G.: Finding bugs in exceptional situations of JNI programs. In: Proceedings of the 16th ACM Conference on Computer and Communications Security, CCS’09, pp. 442–452. Association for Computing Machinery, New York, NY, USA (2009). https://doi.org/10.1145/1653662.1653716

  36. Mell, P., Grance, T., et al.: The nist definition of cloud computing. Natl. Inst. Sci. Technol. Spec. Publ. 800(2011), 145 (2011)

    Google Scholar 

  37. Miné, A.: The octagon abstract domain. Higher-order and symbolic computation 19(1), 31–100 (2006). https://doi.org/10.1007/s10990-006-8609-1

    Article  MATH  Google Scholar 

  38. Monat, R., Ouadjaout, A., Miné, A.: A multilanguage static analysis of python programs with native c extensions. In: Drăgoi, C., Mukherjee, S., Namjoshi, K. (eds.) Static Analysis, pp. 323–345. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-88806-0_16

  39. Negrini, L.: A generic framework for multilanguage analysis. Ph.D. thesis, Universitá Ca’ Foscari Venezia (2023)

    Google Scholar 

  40. Negrini, L., Arceri, V., Ferrara, P., Cortesi, A.: Twinning automata and regular expressions for string static analysis. In: Verification, Model Checking, and Abstract Interpretation: 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, 17–19 Jan. 2021, Proceedings, pp. 267–290. Springer, Berlin, Heidelberg (2021). https://doi.org/10.1007/978-3-030-67067-2_13

  41. Pinto, P., Carvalho, T., AO Bispo, J., Ramalho, M.A., AO M.P. Cardoso. J.: Aspect composition for multiple target languages using lara. Comput. Lang. Syst. Struct. 53, 1–26 (2018). https://doi.org/10.1016/j.cl.2017.12.003. www.sciencedirect.com/science/article/pii/S147784241730115X

  42. Porru, S., Pinna, A., Marchesi, M., Tonelli, R.: Blockchain-oriented software engineering: challenges and new directions. In: 2017 IEEE/ACM 39th International Conference on Software Engineering Companion (ICSE-C), pp. 169–171 (2017). https://doi.org/10.1109/ICSE-C.2017.142

  43. Rival, X., Mauborgne, L.: The trace partitioning abstract domain. ACM Trans Program. Lang. Syst. (TOPLAS) 29(5), 26—es (2007). https://doi.org/10.1145/1275497.1275501

  44. Sabelfeld, A., Myers, A.: Language-based information-flow security. IEEE Journal on Selected Areas in Communications 21(1), 5–19 (2003). https://doi.org/10.1109/JSAC.2002.806121

    Article  Google Scholar 

  45. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002). https://doi.org/10.1145/514188.514190

  46. Sharir, M., Pnueli, A., et al.: Two approaches to interprocedural data flow analysis. New York University. Courant Institute of Mathematical Sciences (1978)

    Google Scholar 

  47. Spoto, F.: The julia static analyzer for java. In: Rival, X. (ed.) Static Analysis, pp. 39–57. Springer, Berlin, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_3

  48. Sundaresan, V., Hendren, L., Razafimahefa, C., Vallée-Rai, R., Lam, P., Gagnon, E., Godin, C.: Practical virtual method call resolution for java. In: Proceedings of the 15th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA ’00, pp. 264–280. Association for Computing Machinery, New York, NY, USA (2000). https://doi.org/10.1145/353171.353189

  49. Tan, G., Morrisett, G.: Ilea: Inter-language analysis across java and c. In: Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA ’07, pp. 39–56. Association for Computing Machinery, New York, NY, USA (2007). https://doi.org/10.1145/1297027.1297031

  50. Teixeira, G., Bispo, J.a., Correia, F.F.: Multi-language static code analysis on the lara framework. In: Proceedings of the 10th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis, SOAP 2021, pp. 31–36. Association for Computing Machinery, New York, NY, USA (2021). https://doi.org/10.1145/3460946.3464317

  51. Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: Taj: effective taint analysis of web applications. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, 15–21 June 2009, pp. 87–97. ACM (2009). https://doi.org/10.1145/1542476.1542486

  52. Vongsingthong, S., Smanchat, S.: Internet of things: a review of applications and technologies. Suranaree J. Sci. Technol. 21(4), 359–374 (2014)

    Google Scholar 

  53. Wei, F., Lin, X., Ou, X., Chen, T., Zhang, X.: Jn-saf: Precise and efficient NDK/JNI-aware inter-language static analysis framework for security vetting of android applications with native code. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, CCS ’18, pp. 1137–1150. Association for Computing Machinery, New York, NY, USA (2018). https://doi.org/10.1145/3243734.3243835

Download references

Acknowledgements

Work partially supported by SPIN-2021 projects ‘Ressa-Rob’ and ‘Static Analysis for Data Scientists’, and Fondi di primo insediamento 2019 project ‘Static Taint Analysis for IoT Software’ funded by Ca’Foscari University, and by iNEST-Interconnected NordEst Innovation Ecosystem, funded by PNRR (Mission 4.2, Investment 1.5), NextGeneration EU—Project ID: ECS 00000043.”

Author information

Authors and Affiliations

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

    Luca Negrini, Pietro Ferrara & Agostino Cortesi

  2. Corvallis SRL, Padova, Italy

    Luca Negrini

  3. University of Parma, Parma, Italy

    Vincenzo Arceri

Authors
  1. Luca Negrini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pietro Ferrara
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Vincenzo Arceri
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Agostino Cortesi
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Luca Negrini .

Editor information

Editors and Affiliations

  1. Department of Mathematical, Physical, and Computer Sciences, University of Parma, Parma, Italy

    Vincenzo Arceri

  2. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Agostino Cortesi

  3. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Pietro Ferrara

  4. Department of Environmental Sciences, Informatics and Statistics, Ca’ Foscari University of Venice, Venice, Italy

    Martina Olliaro

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Negrini, L., Ferrara, P., Arceri, V., Cortesi, A. (2023). LiSA: A Generic Framework for Multilanguage Static Analysis. In: Arceri, V., Cortesi, A., Ferrara, P., Olliaro, M. (eds) Challenges of Software Verification. Intelligent Systems Reference Library, vol 238. Springer, Singapore. https://doi.org/10.1007/978-981-19-9601-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-981-19-9601-6_2

  • Published:

  • Publisher Name: Springer, Singapore

  • Print ISBN: 978-981-19-9600-9

  • Online ISBN: 978-981-19-9601-6

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation