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 these 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.
- Ayari, A. and Basin, D. 2000. Bounded model construction for monadic second-order logics. In Proceedings of the International Conference on Computer-Aided Verification (CAV'00). Google ScholarDigital Library
- Balzarotti, D., Cova, M., Felmetsger, V., Jovanovic, N., Kirda, E., Kruegel, C., and Vigna, G. 2008. Saner: Composing static and dynamic analysis to validate sanitization in web applications. In Proceedings of the IEEE Symposium on Security and Privacy. Google ScholarDigital Library
- Bjørner, N., Tillmann, N., and Voronkov, A. 2009. Path feasibility analysis for string-manipulating programs. In Proceedings of the 1st International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'09). Google ScholarDigital Library
- Brumley, D., Wang, H., Jha, S., and Song, D. 2007. Creating vulnerability signatures using weakest preconditions. In Proceedings of the IEEE Computer Security Foundations Symposium. Google ScholarDigital Library
- Christensen, A. S., Feldthaus, A., and Møller, A. 2009. JSA -- The java string analyzer. http://www.brics.dk/JSA.Google Scholar
- Christensen, A. S., Møller, A., and Schwartzbach, M. I. 2003. Precise analysis of string expressions. In Proceedings of the International Static Analysis Symposium (SAS'03). Google ScholarDigital Library
- Cousot, P. and Cousot, R. 1995. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture (FPCA'95). Google ScholarDigital Library
- Cytron, R., Ferrante, J., Rosen, B. K., Wegman, M. N., and Zadeck, F. K. 1991. Efficiently computing static single assignment form and the control dependence graph. ACM Trans. Program. Lang. Syst. 13, 4. Google ScholarDigital Library
- Engelfriet, J. and Hoogeboom, H. J. 2001. MSO definable string transductions and two-way finite-state transducers. ACM Trans. Comput. Logic 2, 2. Google ScholarDigital Library
- Fu, X. and Li, C.-C. 2010. A string constraint solver for detecting web application vulnerability. In Proceedings of the 22nd International Conference on Software Engineering and Knowledge Engineering (SEKE'10).Google Scholar
- Ganesh, V., Kiezun, A., Artzi, S., Guo, P. J., Hooimeijer, P., and Ernst, M. 2011. HAMPI: A string solver for testing, analysis and vulnerability detection. In Proceedings of the 23rd International Conference of Computer Aided Verification (CAV'11). Google ScholarDigital Library
- Geay, E., Pistoia, M., Tateishi, T., Ryder, B., and Dolby, J. 2009. Modular string-sensitive permission analysis with demand-driven precision. In Proceedings of the 31th International Conference on Software Engineering (ICSE'09). Google ScholarDigital Library
- Grove, D. and Chambers, C. 2001. A framework for call graph construction algorithms. ACM Trans. Program. Lang. Syst. 23, 6. Google ScholarDigital Library
- Grove, D., Defouw, G., Dean, J., and Chambers, C. 1997. Call graph construction in object-oriented languages. In Proceedings of the 12th ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'97). Google ScholarDigital Library
- Hammer, C., Schaade, R., and Snelting, G. 2008. Static path conditions for java. In Proceedings of the 3rd ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS'08). Google ScholarDigital Library
- Henriksen, J. G., Jensen, J. L., Jørgensen, M. E., Klarlund, N., Paige, R., Rauhe, T., and Sandholm, A. 1995. MONA: Monadic second-order logic in practice. In Proceedings of the 1st International Workshop on Tools and Algorithms for Construction and Analysis of Systems (TACAS'95). Google ScholarDigital Library
- Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., and Veanes, M. 2011. Fast and precise sanitizer analysis with bek. In Proceedings of the 20th USENIX Conference on Security (SEC'11). USENIX Association, Berkeley, CA, 1--1. Google ScholarDigital Library
- Hooimeijer, P. and Weimer, W. 2009. A decision procedure for subset constraints over regular languages. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'09). Google ScholarDigital Library
- IBM. 2013. Rational appscan source edition. http://www.ibm.com/software/rational/products/appscan/source.Google Scholar
- Kay, M. and Kaplan, R. M. 1994. Regular models of phonological rule systems. Comput. Linguist. 20, 3. Google ScholarDigital Library
- Kiezun, A., Ganesh, V., Guo, P. J., Hooimeijer, P., and Ernst, M. D. 2009a. HAMPI: A solver for string constraints. In Proceedings of the ACM International Symposium on Testing and Analysis (ISSTA'09). Google ScholarDigital Library
- Kiezun, A., Guo, P. J., Jayaraman, K., and Ernst, M. D. 2009b. Automatic creation of sql injection and cross-site scripting attacks. http://dspace.mit.edu/bitstream/handle/1721.1/42836/MIT-CSAIL-TR-2008-054.pdf?sequence=1.Google Scholar
- Klarlund, N. and Møller, A. 2001. MONA version 1.4 user manual. BRICS. Notes series NS-01-1. http://www.brics.dk/mona.Google Scholar
- Livshits, B., Nori, A. V., Rajamani, S. K., and Banerjee, A. 2009. Merline: Specification inference for explicit information flow problems. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'09). Google ScholarDigital Library
- Livshits, V. B. and Lam, M. S. 2005. Finding security vulnerabilities in java applications with static analysis. In Proceedings of the 14th USENIX Security Symposium. Google ScholarDigital Library
- Maier, P. 2009. Deciding extensions of the theories of vectors and bags. In Proceedings of the 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'09). Google ScholarDigital Library
- Minamide, Y. 2005. Static approximation of dynamically generated web pages. In Proceedings of the 14th International Conference on World Wide Web (WWW'05). Google ScholarDigital Library
- Open Web Application Security Project (OWASP). 2013. http://www.owasp.org/index.php/Category:AttackGoogle Scholar
- Reps, T. 1997. Program analysis via graph reachability. Inf. Softw. Technol. 40, 11--12, 701--726.Google Scholar
- Rosen, B. K., Wegman, M. N., and Zadeck, F. K. 1988. Global value numbers and redundant computations. In Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'88). Google ScholarDigital Library
- Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., and Song, D. 2010. A symbolic execution framework for javascript. In Proceedings of the IEEE Symposium on Security and Privacy. Google ScholarDigital Library
- Shannon, D., Ghosh, I., Rajan, S., and Khurshid, S. 2009. Efficient symbolic execution of strings for validating web applications. In Proceedings of the 2nd International Workshop on Defects in Large Software Systems (DEFECTS'09). Google ScholarDigital Library
- Snelting, G. 1996. Combining slicing and constraint solving for validation of measurement software. In Proceedings of the 3rd International Symposium on Static Analysis. Google ScholarDigital Library
- Tillmann, N. and Halleux, J. D. 2008. Pex: White box test generation for .net. In Proceedings of the 2nd International Conference on Tests and Proofs (TAP'08). Google ScholarDigital Library
- Tripp, O., Pistoia, M., Fink, S., Sridharan, M., and Weisman, O. 2009. TAJ: Effective taint analysis of web applications. In Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'09). Google ScholarDigital Library
- Veanes, M., de Halleux, P., and Tillmann, N. 2010. Rex: Symbolic regular expression explorer. In Proceedings of the 3rd International Conference on Software Testing, Verification, and Validation (ICST'10). IEEE Computer Society, Los Alamitos, CA, 498--507. Google ScholarDigital Library
- Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., and Bjorner, N. 2012. Symbolic finite state transducers: Algorithms and applications. In Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL'12). ACM Press, New York, 137--150. Google ScholarDigital Library
- Wala. T. J. 2013. Watson libraries for analysis. http://wala.sf.net/.Google Scholar
- Wang, X., Zhang, L., Xie, T., Mei, H., and Sun, J. 2009. Locating need-to-translate constant strings for software internationalization. In Proceedings of the 31st International Conference on Software Engineering (ICSE'09). Google ScholarDigital Library
- Wassermann, G. and Su, Z. 2007. Sound and precise analysis of web applications for injection vulnerabilities. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'07). Google ScholarDigital Library
- Wassermann, G., Yu, D., Chander, A., Dhurjati, D., Inamura, H., and Su, Z. 2008. Dynamic test input generation for web applications. In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA'08). Google ScholarDigital Library
- Wegman, M. N. and Zadeck, F. K. 1991. Constant propagation with conditional branches. ACM Trans. Program. Lang. Syst. 13, 2. Google ScholarDigital Library
- Whaley, J. and Lam, M. S. 2004. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI'04). Vol. 39. Google ScholarDigital Library
- Yu, F., Alkhalaf, M., and Bultan, T. 2009. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering (ASE'09). Google ScholarDigital Library
- Yu, F., Bultan, T., Cova, M., and Ibarra, O. 2008. Symbolic string verification: An automata-based approach. In Proceedings of the 15th International SPIN Workshop on Model Checking of Software. Google ScholarDigital Library
- Z3. 2013. Z3. http://research.microsoft.com/projects/z3.Google Scholar
Index Terms
- Path- and index-sensitive string analysis based on monadic second-order logic
Recommendations
Z3-str: a z3-based string solver for web application analysis
ESEC/FSE 2013: Proceedings of the 2013 9th Joint Meeting on Foundations of Software EngineeringAnalyzing web applications requires reasoning about strings and non-strings cohesively. Existing string solvers either ignore non-string program behavior or support limited set of string operations. In this paper, we develop a general purpose string ...
Path- and index-sensitive string analysis based on monadic second-order logic
ISSTA '11: Proceedings of the 2011 International Symposium on Software Testing and AnalysisWe 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 ...
Comments