Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Numerical Software Verification

Working Conference on Verified Software: Theories, Tools, and Experiments

NSV 2020, VSTTE 2020: Software Verification pp 3–20Cite as

SARL: OO Framework Specification for Static Analysis

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12549))

Abstract

Semantic static analysis allows sound verification of program properties, that is, to prove that a given property holds for all possible executions. However, modern object-oriented applications make heavy use of third-party frameworks. These provide various functionalities (like libraries), as well as an extension of the execution model of the program. Applying standard models to statically analyze software relying on such frameworks could be potentially unsound and imprecise.

In this paper we introduce SARL, a domain-specific language which allows one to specify the runtime behaviors of frameworks of object-oriented programs. Such specifications can be then applied to automatically generate annotations on program components of the application to model the framework runtime environment. In addition, SARL specifications document which aspects of a framework are supported by the static analyzer and how. We adopted SARL to model WindowsForms and ASP.NET, two of the most popular .NET frameworks in an existing industrial static analyzer (Julia). We then analyzed the three most popular GitHub repositories using these frameworks, comparing the results with and without SARL. Our experimental results show that the application of SARL sensibly improved the precision and soundness of the analysis without affecting its runtime performances.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    https://static.juliasoft.com/docs/2.7.0.3/frameworks.html.

  2. 2.

    The documentation of the available annotations is available at https://static.juliasoft.com/docs/2.7.0.3/annotations.html.

  3. 3.

    https://javacc.org/.

References

  1. Asp.net boilerplate. https://github.com/aspnetboilerplate/aspnetboilerplate

  2. Asp.net signalr. https://github.com/SignalR/SignalR

  3. Cefsharp. https://github.com/cefsharp/CefSharp

  4. Shadowsocks for windows. https://github.com/shadowsocks/shadowsocks-windows

  5. Sharex. https://github.com/ShareX/ShareX

  6. Umbraco CMS. https://github.com/umbraco/Umbraco-CMS

  7. Ali, K., Lhoták, O.: Averroes: whole-program analysis without the whole program. In: Castagna, G. (ed.) ECOOP 2013. LNCS, vol. 7920, pp. 378–400. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-39038-8_16

    Chapter  Google Scholar 

  8. Arzt, S., Bodden, E.: Stubdroid: automatic inference of precise data-flow summaries for the android framework. In: Proceedings of ICSE 2016. IEEE (2016)

    Google Scholar 

  9. ASP.NET (2018). https://www.asp.net/

  10. Ball, T., Rajamani, S.: Slic: a specification language for interface checking (of c). Technical report. MSR-TR-2001-21, January 2002

    Google Scholar 

  11. Centonze, P., Naumovich, G., Fink, S.J., Pistoia, M.: Role-based access control consistency validation. In: ISSTA (2006)

    Google Scholar 

  12. Ernst, M.D., Lovato, A., Macedonio, D., Spiridon, C., Spoto, F.: Boolean formulas for the static identification of injection attacks in Java. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 130–145. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48899-7_10

    Chapter  MATH  Google Scholar 

  13. Ferrara, P., Cortesi, A., Spoto, F.: Cil to Java-bytecode translation for static analysis leveraging. In: Proceedings of FormaliSE 2018. Springer (2018)

    Google Scholar 

  14. Forms, W.: (2018). https://docs.microsoft.com/it-it/dotnet/framework/winforms/

  15. Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39, 12 (2004)

    Article  Google Scholar 

  16. Toman, J., Grossman, D.: Concerto: a framework for combined concrete and abstract interpretation. In: Proceedings of the ACM on Programming Languages, vol. 3 (2019)

    Google Scholar 

  17. Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop 1998 (1998)

    Google Scholar 

  18. Lombok (2018). https://projectlombok.org/

  19. Palsberg, J., Schwartzbach, M.I.: Object-oriented type inference. In: Proceedings of OOPSLA 1991. ACM Press (1991)

    Google Scholar 

  20. Spoto, F.: Nullness analysis in Boolean form. In: Proceedings of SEFM 2008. IEEE (2008)

    Google Scholar 

  21. Spoto, F., Mesnard, F., Payet, E.: A termination analyzer for java bytecode based on path-length. ACM Trans. Program. Lang. Syst. (TOPLAS) 32(3), 1–70 (2010)

    Article  Google Scholar 

  22. Sridharan, M., Artzi, S., Pistoia, M., Guarnieri, S., Tripp, O., Berg, R.: F4f: taint analysis of framework-based web applications. In: Proceedings of the 2011 ACM International conference on Object-Oriented Programming, Systems, Languages, Languages, and Applications, vol. 16, pp. 1053–1068 (2011)

    Google Scholar 

  23. Tripp, O., Pistoia, M., Fink, S.J., Sridharan, M., Weisman, O.: TAJ: effective taint analysis of web application. In: PLDI. ACM (2009)

    Google Scholar 

  24. Unity (2018). https://unity3d.com/

  25. Wikipedia: Software framework. https://en.wikipedia.org/wiki/Software_framework

  26. Xamarin (2018). https://visualstudio.microsoft.com/xamarin/

Download references

Author information

Authors and Affiliations

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

    Pietro Ferrara & Luca Negrini

  2. JuliaSoft SRL, Verona, Italy

    Luca Negrini

Authors
  1. Pietro Ferrara
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Luca Negrini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pietro Ferrara .

Editor information

Editors and Affiliations

  1. MPI-SWS Kaiserslautern, Kaiserslautern, Germany

    Maria Christakis

  2. University of California, San Diego, La Jolla, CA, USA

    Nadia Polikarpova

  3. Computer Science, University of North Carolina at Chapel Hill, Chapel Hill, NC, USA

    Parasara Sridhar Duggirala

  4. Engineering and Informatics, University of Sussex, Brighton, UK

    Peter Schrammel

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ferrara, P., Negrini, L. (2020). SARL: OO Framework Specification for Static Analysis. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds) Software Verification. NSV VSTTE 2020 2020. Lecture Notes in Computer Science(), vol 12549. Springer, Cham. https://doi.org/10.1007/978-3-030-63618-0_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-63618-0_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-63617-3

  • Online ISBN: 978-3-030-63618-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation