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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Aiken, A., Wimmers, E.L., Lakshman, T.K.: Soft typing with conditional types. In: POPL (1994)
Chandra, S., Reps, T.: Physical type checking for C. In: Workshop on Program analysis for software tools and engineering, PASTE (1999)
Chase, D.R., Wegman, M., Zadeck, F.K.: Analysis of pointers and structures. In: PLDI (1990)
Patrick Cousot. Types as abstract interpretations. In POPL, 1997.
Fagan, M.: Soft Typing: An Approach to Type Checking for Dynamically Typed Languages. PhD thesis, Rice University (1992)
Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional must program analysis: unleashing the power of alternation. In: POPL (2010)
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)
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)
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)
Jovanovic, N., Kruegel, C., Kirda, E.: Pixy: A static analysis tool for detecting web application vulnerabilities. In: IEEE Symp. Security and Privacy (2006)
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)
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)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. In: IEEE TSE (January 1986)
Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: PLDI (2007)
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)
Yorsh, G., Ball, T., Sagiv, M.: Testing, abstraction, theorem proving: better together? In: ISSTA, pp. 145–156 (2006)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)