A suite of abstract domains for static analysis of string values

被引:34
作者
Costantini, Giulia [1 ]
Ferrara, Pietro [2 ,3 ]
Cortesi, Agostino [1 ]
机构
[1] Ca Foscari Univ, I-30172 Venice, Italy
[2] ETH, Zurich, Switzerland
[3] IBM Thomas J Watson Res Ctr, Yorktown Hts, NY USA
关键词
static analysis; abstract interpretation; abstract domains; strings;
D O I
10.1002/spe.2218
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Strings are widely used in modern programming languages in various scenarios. For instance, strings are used to build up Structured Query Language (SQL) queries that are then executed. Malformed strings may lead to subtle bugs, as well as non-sanitized strings may raise security issues in an application. For these reasons, the application of static analysis to compute safety properties over string values at compile time is particularly appealing. In this article, we propose a generic approach for the static analysis of string values based on abstract interpretation. In particular, we design a suite of abstract semantics for strings, where each abstract domain tracks a different kind of information. We discuss the trade-off between efficiency and accuracy when using such domains to catch the properties of interest. In this way, the analysis can be tuned at different levels of precision and efficiency, and it can address specific properties.Copyright (c) 2013 John Wiley & Sons, Ltd.
引用
收藏
页码:245 / 287
页数:43
相关论文
共 44 条
[1]  
Halder R., Cortesi A., Obfuscation-based analysis of SQL injection attacks, Proceedings of the IEEE Symposium on Computers and Communications, ISCC '10, pp. 931-938, (2010)
[2]  
Hooimeijer P., Veanes M., An evaluation of automata algorithms for string analysis, Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI '11, pp. 248-262, (2011)
[3]  
Hosoya H., Pierce B., Xduce: A statically typed xml processing language, ACM Transactions on Internet Technology (TOIT), 3, 2, pp. 117-148, (2003)
[4]  
Tabuchi N., Sumii E., Yonezawa A., Regular expression types for strings in a text processing language, Electronic Notes in Theoretical Computer Science, 75, pp. 95-113, (2002)
[5]  
Yu F., Bultan T., Cova M., Ibarra O., Symbolic string verification: An automata-based approach, Proceedings of the 15th International Workshop on Model Checking Software, SPIN '08, pp. 306-324, (2008)
[6]  
Brabrand C., Moller A., Schwartzbach M.I., Static validation of dynamically generated HTML, Proceedings of the ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering, PASTE '01, Snowbird, UT, USA, 2001, pp. 38-45
[7]  
Gould C., Su Z., Devanbu P., Static checking of dynamically generated queries in database applications, Proceedings of the 26th International Conference on Software Engineering, ICSE '04, pp. 645-654, (2004)
[8]  
Gulwani S., Automating string processing in spreadsheets using input-output examples, Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, pp. 317-330, (2011)
[9]  
Minamide Y., Static approximation of dynamically generated web pages, Proceedings of the 14th International Conference on World Wide Web, WWW '05, pp. 432-441, (2005)
[10]  
Moller A., Schwarz M., HTML validation of context-free languages, Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS '11, pp. 426-440, (2011)