ABSTRACT
We propose a novel technique for statically verifying the strings generated by a program. The verification is conducted by encoding the program in Monadic Second-Order Logic (M2L). We use M2L to describe constraints among program variables and to abstract built-in string operations. Once we encode a program in M2L, a theorem prover for M2L, such as MONA, can automatically check if a string generated by the program satisfies a given specification, and if not, exhibit a counterexample. With this approach, we can naturally encode relationships among strings, accounting also for cases in which a program manipulates strings using indices. In addition, our string analysis is path sensitive in that it accounts for the effects of string and Boolean comparisons, as well as regular-expression matches.
We have implemented our string-analysis algorithm, and used it to augment an industrial security analysis for Web applications by automatically detecting and verifying sanitizers---methods that eliminate malicious patterns from untrusted strings, making those strings safe to use in security-sensitive operations. On the 8 benchmarks we analyzed, our string analyzer discovered 128 previously unknown sanitizers, compared to 71 sanitizers detected by a previously presented string analysis.
- IBM Rational AppScan Source Edition. ibm.com/software/rational/products/appscan/source.Google Scholar
- Open Web Application Security Project (OWASP). owasp.org/index.php/Category:Attack.Google Scholar
- A. Ayari and D. Basin. Bounded model construction for monadic second-order logics. In CAV, 2000. Google ScholarDigital Library
- D. Balzarotti, M. Cova, V. Felmetsger, N. Jovanovic, E. Kirda, C. Kruegel, and G. Vigna. Saner: Composing static and dynamic analysis to validate sanitization in web applications. In Security and Privacy (Oakland), 2008. Google ScholarDigital Library
- N. Bjørner, N. Tillmann, and A. Voronkov. Path feasibility analysis for string-manipulating programs. In TACAS, 2009.Google ScholarDigital Library
- D. Brumley, H. Wang, S. Jha, and D. Song. Creating vulnerability signatures using weakest preconditions. In CSF, 2007. Google ScholarDigital Library
- A. S. Christensen, A. Feldthaus, and A. Møller. JSA -- the Java String Analyzer. brics.dk/JSA, 2009.Google Scholar
- A. S. Christensen, A. Møller, and M. I. Schwartzbach. Precise analysis of string expressions. In SAS, 2003. Google ScholarDigital Library
- P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In FPCA, 1995. Google ScholarDigital Library
- R. Cytron, J. Ferrante, B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Efficiently computing static single assignment form and the control dependence graph. TOPLAS, 1991. Google ScholarDigital Library
- X. Fu and C.-C. Li. A string constraint solver for detecting web application vulnerability. In SEKE, 2010.Google Scholar
- E. Geay, M. Pistoia, T. Tateishi, B. Ryder, and J. Dolby. Modular string-sensitive permission analysis with demand-driven precision. In ICSE, 2009. Google ScholarDigital Library
- D. Grove and C. Chambers. A Framework for Call Graph Construction Algorithms. TOPLSA, 2001. Google ScholarDigital Library
- D. Grove, G. DeFouw, J. Dean, and C. Chambers. Call graph construction in object-oriented languages. In OOPSLA, 1997. Google ScholarDigital Library
- C. Hammer, R. Schaade, and G. Snelting. Static path conditions for java. In PLAS, 2008. Google ScholarDigital Library
- J. G. Henriksen, J. L. Jensen, M. E. Jørgensen, N. Klarlund, R. Paige, T. Rauhe, and A. Sandholm. MONA: Monadic second-order logic in practice. In TACAS, 1995. Google ScholarDigital Library
- P. Hooimeijer and W. Weimer. A decision procedure for subset constraints over regular languages. In PLDI, 2009. Google ScholarDigital Library
- M. Kay and R. M. Kaplan. Regular models of phonological rule systems. Computational Linguistics, 20(3), 1994. Google ScholarDigital Library
- A. Kieżun, V. Ganesh, P. J. Guo, P. Hooimeijer, and M. D. Ernst. HAMPI: A solver for string constraints. In ISSTA, 2009.Google ScholarDigital Library
- N. Klarlund and A. Møller. MONA Version 1.4 User Manual. BRICS, 2001. Notes Series NS-01-1. http://www.brics.dk/mona.Google Scholar
- B. Livshits, A. V. Nori, S. K. Rajamani, and A. Banerjee. Merline: Specification inference for explicit information flow problems. In PLDI, 2009. Google ScholarDigital Library
- V. B. Livshits and M. S. Lam. Finding security vulnerabilities in java applications with static analysis. In USENIX Security, 2005. Google ScholarDigital Library
- Y. Minamide. Static approximation of dynamically generated web pages. In WWW, 2005. Google ScholarDigital Library
- B. K. Rosen, M. N. Wegman, and F. K. Zadeck. Global value numbers and redundant computations. In POPL, 1988. Google ScholarDigital Library
- P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song. A symbolic execution framework for javascript. In Security and Privacy (Oakland), 2010. Google ScholarDigital Library
- D. Shannon, I. Ghosh, S. Rajan, and S. Khurshid. Efficient symbolic execution of strings for validating web applications. In DEFECTS, 2009. Google ScholarDigital Library
- G. Snelting. Combining slicing and constraint solving for validation of measurement software. In SAS, 1996. Google ScholarDigital Library
- T. Tateishi, M. Pistoia, and O. Tripp. Path- and index-sensitive string analysis based on monadic second-order logic. IBM Research Report RT0930, 2011.Google Scholar
- N. Tillmann and J. D. Halleux. Pex: white box test generation for .NET. In TAP, 2008. Google ScholarDigital Library
- O. Tripp, M. Pistoia, S. Fink, M. Sridharan, and O. Weisman. TAJ: Effective taint analysis of web applications. In PLDI, 2009. Google ScholarDigital Library
- M. Veanes, P. de Halleux, and N. Tillmann. Rex: Symbolic regular expression explorer. Microsoft Research Technical Report MSR-TR-2009-137, 2009.Google Scholar
- T. J. Watson Libraries for Analysis, wala.sf.net/.Google Scholar
- G. Wassermann and Z. Su. Sound and precise analysis of web applications for injection vulnerabilities. In PLDI, 2007. Google ScholarDigital Library
- M. N. Wegman and F. K. Zadeck. Constant propagation with conditional branches. TOPLAS, 1991. Google ScholarDigital Library
- F. Yu, M. Alkhalaf, and T. Bultan. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In ASE, 2009. Google ScholarDigital Library
- F. Yu, T. Bultan, M. Cova, and O. Ibarra. Symbolic string verification: An automata-based approach. In SPIN Workshop, 2008. Google ScholarDigital Library
- Z3, research.microsoft.com/projects/z3.Google Scholar
Recommendations
Path- and index-sensitive string analysis based on monadic second-order logic
Testing, debugging, and error handling, formal methods, lifecycle concerns, evolution and maintenanceWe propose a novel technique for statically verifying the strings generated by a program. The verification is conducted by encoding the program in Monadic Second-order Logic (M2L). We use M2L to describe constraints among program variables and to ...
Verifying pointer and string analyses with region type systems
Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and usually contributes to other analyses or code optimizations. In recent ...
String analysis for Java and Android applications
ESEC/FSE 2015: Proceedings of the 2015 10th Joint Meeting on Foundations of Software EngineeringString analysis is critical for many verification techniques. However, accurately modeling string variables is a challeng- ing problem. Current approaches are generally customized for certain problem domains or have critical limitations in handling ...
Comments