Skip to main content

Runtime Instrumentation for Precise Flow-Sensitive Type Analysis

  • Conference paper
Runtime Verification (RV 2010)

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

Included in the following conference series:

Abstract

We describe a combination of runtime information and static analysis for checking properties of complex and configurable systems. The basic idea of our approach is to 1) let the program execute and thereby read the important dynamic configuration data, then 2) invoke static analysis from this runtime state to detect possible errors that can happen in the continued execution. This approach improves analysis precision, particularly with respect to types of global variables and nested data structures. It also enables the resolution of modules that are loaded based on dynamically computed information.

We describe an implementation of this approach in a tool that statically computes possible types of variables in PHP applications, including detailed types of nested maps (arrays). PHP is a dynamically typed language; PHP programs extensively use nested value maps, as well as ’include’ directives whose arguments are dynamically computed file names. We have applied our analysis tool to over 50’000 lines of PHP code, including the popular DokuWiki software, which has a plug-in architecture. The analysis identified 200 problems in the code and in the type hints of the original source code base. Some of these problems can cause exploits, infinite loops, and crashes. Our experiments show that dynamic information simplifies the development of the analysis and decreases the number of false alarms compared to a purely static analysis approach.

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

Access this chapter

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aiken, A., Wimmers, E.L., Lakshman, T.K.: Soft typing with conditional types. In: POPL (1994)

    Google Scholar 

  2. Chandra, S., Reps, T.: Physical type checking for C. In: Workshop on Program analysis for software tools and engineering, PASTE (1999)

    Google Scholar 

  3. Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI (1990)

    Google Scholar 

  4. Patrick Cousot. Types as abstract interpretations. In POPL, 1997.

    Google Scholar 

  5. Fagan, M.: Soft Typing: An Approach to Type Checking for Dynamically Typed Languages. PhD thesis, Rice University (1992)

    Google Scholar 

  6. Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional must program analysis: unleashing the power of alternation. In: POPL (2010)

    Google Scholar 

  7. Huang, Y.-W., Yu, F., Hang, C., Tsai, C.-H., Lee, D.T., Kuo, S.-Y.: Securing web application code by static analysis and runtime protection. In: WWW (2004)

    Google Scholar 

  8. Jensen, S.H., Møller, A., Thiemann, P.: Type analysis for JavaScript. In: Palsberg, J., Su, Z. (eds.) Static Analysis. LNCS, vol. 5673, pp. 238–255. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  9. Jhala, R., Majumdar, R., Xu, R.-G.: State of the union: Type inference via craig interpolation. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 553–567. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  10. Jovanovic, N., Kruegel, C., Kirda, E.: Pixy: A static analysis tool for detecting web application vulnerabilities. In: IEEE Symp. Security and Privacy (2006)

    Google Scholar 

  11. Komondoor, R., Ramalingam, G., Chandra, S., Field, J.: Dependent types for program understanding. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 157–173. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  12. Pasareanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: ISSTA (2008)

    Google Scholar 

  13. Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. In: IEEE TSE (January 1986)

    Google Scholar 

  14. Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI (2007)

    Google Scholar 

  15. Yabandeh, M., Knežević, N., Kostić, D., Kuncak, V.: Predicting and preventing inconsistencies in deployed distributed systems. ACM Transactions on Computer Systems 28(1) (2010)

    Google Scholar 

  16. Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together? In: ISSTA, pp. 145–156 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kneuss, E., Suter, P., Kuncak, V. (2010). Runtime Instrumentation for Precise Flow-Sensitive Type Analysis. In: Barringer, H., et al. Runtime Verification. RV 2010. Lecture Notes in Computer Science, vol 6418. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-16612-9_23

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-16612-9_23

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-16611-2

  • Online ISBN: 978-3-642-16612-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics