{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,3,7]],"date-time":"2024-03-07T17:56:27Z","timestamp":1709834187875},"reference-count":59,"publisher":"Association for Computing Machinery (ACM)","issue":"6","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            Modern web applications often suffer from command injection attacks. Even when equipped with sanitization code, many systems can be penetrated due to software bugs. It is desirable to automatically discover such vulnerabilities, given the bytecode of a web application. One approach would be symbolically executing the target system and constructing constraints for matching path conditions and attack patterns. Solving these constraints yields an attack signature, based on which, the attack process can be replayed. Constraint solving is the key to symbolic execution. For web applications, string constraints receive most of the attention because web applications are essentially text processing programs. We present\n            <jats:italic>simple linear string equation (SISE)<\/jats:italic>\n            , a decidable fragment of the general string constraint system. SISE models a collection of regular replacement operations (such as the greedy, reluctant, declarative, and finite replacement), which are frequently used by text processing programs. Various automata techniques are proposed for simulating procedural semantics such as left-most matching. By composing atomic transducers of a SISE, we show that a recursive algorithm can be used to compute the solution pool, which contains the value range of each variable in concrete solutions. Then a concrete variable solution can be synthesized from a solution pool. To accelerate solver performance, a symbolic representation of finite state transducer is developed. This allows the constraint solver to support a 16-bit Unicode alphabet in practice. The algorithm is implemented in a Java constraint solver called SUSHI. We compare the applicability and performance of SUSHI with Kaluza, a bounded string solver.\n          <\/jats:p>","DOI":"10.1007\/s00165-011-0214-3","type":"journal-article","created":{"date-parts":[[2012,1,16]],"date-time":"2012-01-16T12:52:53Z","timestamp":1326718373000},"page":"847-891","source":"Crossref","is-referenced-by-count":15,"title":["Simple linear string constraints"],"prefix":"10.1145","volume":"25","author":[{"given":"Xiang","family":"Fu","sequence":"first","affiliation":[{"name":"Department of Computer Science, Hofstra University, 11549, Hempstead, NY, USA"}]},{"given":"Michael C.","family":"Powell","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Hofstra University, 11549, Hempstead, NY, USA"}]},{"given":"Michael","family":"Bantegui","sequence":"additional","affiliation":[{"name":"Department of Computer Science, Hofstra University, 11549, Hempstead, NY, USA"}]},{"given":"Chung-Chih","family":"Li","sequence":"additional","affiliation":[{"name":"School of Information and Technology, Illinois State University, 61790, Normal, IL, USA"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Anley C (2002) Advanced SQL injection in SQL server applications. Next generation security software"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Anand S Pasareanu CS Visser W (2007) JPF-SE: a symbolic execution extension to Java pathfinder. In: Proceedings of the 13th international conference on tools and algorithms for construction and analysis of systems (TACAS) pp 134\u2013138","DOI":"10.1007\/978-3-540-71209-1_12"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Alur R \u010cern\u00fd P (2011) Streaming transducers for algorithmic verification of single-pass list-processing programs. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL) pp 599\u2013610","DOI":"10.1145\/1925844.1926454"},{"key":"e_1_2_1_2_4_2","unstructured":"Brat G Havelund K Park S Visser W (2000) Java path finder: second generation of a Java model checker. In: Workshop on advances in verification"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Boyd SW Keromytis AD (2004) SQLrand: preventing SQL injection attacks. In: Proceedings of the 2nd applied cryptography and network security conference (ACNS). Lecture notes in computer science vol 3089. Springer pp 292\u2013302","DOI":"10.1007\/978-3-540-24852-1_21"},{"key":"e_1_2_1_2_6_2","first-page":"337","article-title":"Definability in the existential theory of concatenation and undecidable extensions of this theory","volume":"34","author":"B\u00fcchi JR","year":"1998","journal-title":"Zeitschr f math Logik und Grundlagen d Math"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner N Tillmann N Voronkov A (2009) Path feasibility analysis for string-manipulating programs. In: Proceedings of the 15th international conference on tools and algorithms for the construction and analysis of systems (TACAS). Springer pp 307\u2013321","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"crossref","unstructured":"Chaudhuri A Foster JS (2010) Symbolic security analysis of ruby-on-rails web applications. In: Proceedings of the 17th ACM conference on computer and communications security (CCS) pp 585\u2013594","DOI":"10.1145\/1866307.1866373"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Cadar C Ganesh V Pawlowski PM Dill DL Engler DR (2006) EXE: automatically generating inputs of death. In: Proceedings of the 13th ACM conference on computer and communications security (CCS) pp 322\u2013335","DOI":"10.1145\/1180405.1180445"},{"key":"e_1_2_1_2_10_2","unstructured":"Christey SM (2006) Dynamic evaluation vulnerabilities in PHP applications. http:\/\/seclists.org\/fulldisclosure\/2006\/May\/35"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/945885.945890"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Christensen AS Moller A Schwartzbach MI (2003) Precise analysis of string expressions. In: Proceedings of the 10th international static analysis symposium (SAS) pp 1\u201318","DOI":"10.1007\/3-540-44898-5_1"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"crossref","unstructured":"Caballero J Poosankam P McCamant S Babic D Song D (2010) Input generation via decomposition and re-stitching: finding bugs in Malware. In: Proceedings of the 17th ACM conference on computer and communications security (CCS) pp 413\u2013425","DOI":"10.1145\/1866307.1866354"},{"key":"e_1_2_1_2_14_2","unstructured":"Fu X Li CC (2010) A string constraint solver for detecting web application vulnerability. In: Proceedings of the 22nd international conference on software engineering and knowledge engineering (SEKE) pp 535\u2013542"},{"key":"e_1_2_1_2_15_2","unstructured":"Fu X Li CC (2010) Modeling regular replacement for string constraint solving. In: Proceedings of the 2nd NASA formal methods symposium (NFM) pp 67\u201376"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"Fu X Lu X Peltsverger B Chen S Qian K Tao L (2007) A static analysis framework for detecting SQL injection vulnerabilities. In: Proceedings of 31st annual international computer software and applications conference (COMPSAC) pp 87\u201396","DOI":"10.1109\/COMPSAC.2007.43"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Fu X Qian K (2008) SAFELI: SQL injection scanner using symbolic execution. In: Proceedings of the 2008 workshop on testing analysis and verification of web services and applications pp 34\u201339","DOI":"10.1145\/1390832.1390838"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Fu X Qian K Peltsverger B Tao L Liu J (2008) APOGEE: automated project grading and instant feedback system for web based computing. In: Proceedings of the 39th SIGCSE technical symposium on computer science education (SIGCSE) pp 77\u201381","DOI":"10.1145\/1352322.1352163"},{"key":"e_1_2_1_2_19_2","unstructured":"Fu X (2009) SUSHI: a solver for single linear string equations. http:\/\/people.hofstra.edu\/Xiang_Fu\/XiangFu\/projects.php"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"Gould C Su Z Devanbu PT (2004) JDBC checker: a static analysis tool for SQL\/JDBC applications. In: Proceedings of the 26th international conference on software engineering (ICSE) pp 697\u2013698","DOI":"10.1109\/ICSE.2004.1317494"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Huang YW Huang SK Lin TP Tsai CH (2003) Web application security assessment by fault injection and behavior monitoring. In: Proceedings of the 12th international world wide web conference (WWW) pp 148\u2013159","DOI":"10.1145\/775152.775174"},{"key":"e_1_2_1_2_22_2","unstructured":"Hooimeijer P Livshits B Molnar D Saxena P Veanes M (2011) Fast and precise sanitizer analysis with BEK. In: Proceedings of the 20th USENIX security symposium (to appear)"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Henglein F Nielsen L (2011) Regular expression containment: coinductive axiomatization and computational interpretation. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL) pp 385\u2013398","DOI":"10.1145\/1925844.1926429"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"Halfond W Orso A (2005) AMNESIA: analysis and monitoring for NEutralizing SQL-injection attacks. In: Proceedings of the 20th IEEE\/ACM international conference on automated software engineering (ASE) pp 174\u2013183","DOI":"10.1145\/1101908.1101935"},{"key":"e_1_2_1_2_25_2","unstructured":"HP WebInspect (2011) https:\/\/download.hpsmartupdate.com\/webinspect\/. Accessed July 2011"},{"key":"e_1_2_1_2_26_2","unstructured":"Hopcroft JE Ullman JD (1979) Introduction to automata theory languages and computation. Addison-Wesley"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Hooimeijer P Veanes M (2011) An evaluation of automata algorithms for string analysis. In: Proceedings of the 12th international conference on verification model checking and abstract interpretation (VMCAI) pp 248\u2013262","DOI":"10.1007\/978-3-642-18275-4_18"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"crossref","unstructured":"Hooimeijer P Weimer W (2009) A decision procedure for subset constraints over regular languages. In: Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation (PLDI) pp 188\u2013198","DOI":"10.1145\/1543135.1542498"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Hooimeijer P Weimer W (2010) Solving string constraints lazily. In: Proceedings of the 25th IEEE\/ACM international conference on automated software engineering (ASE) pp 377\u2013386","DOI":"10.1145\/1858996.1859080"},{"key":"e_1_2_1_2_30_2","unstructured":"Jurafsky D Martin JH (2008) Speech and language processing (2e). Prentice Hall"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"publisher","DOI":"10.1017\/S1351324997001563"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Kiezun A Ganesh V Guo PJ Hooimeijer P Ernst MD (2009) HAMPI: a solver for string constraints. In: Proceedings of the 18th international symposium on testing and analysis (ISSTA) pp 105\u2013116","DOI":"10.1145\/1572272.1572286"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Kiezun A Guo PJ Jayaraman K Ernst MD (2009) Automatic creation of SQL injection and cross-site scripting attacks. In: Proceedings of the 31st international conference on software engineering (ICSE) pp 199\u2013209","DOI":"10.1109\/ICSE.2009.5070521"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.5555\/204915.204917"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"crossref","unstructured":"Kirkegaard C M\u00f8ller A (2006) Static analysis for Java servlets and JSP. In: Proceedings of the 13th international static analysis symposium (SAS) pp 336\u2013352","DOI":"10.1007\/11823230_22"},{"key":"e_1_2_1_2_37_2","unstructured":"Labs@gdssecurity.com. (2009) Adobe Flex SDK Input Validation Bug in \u2018index.template.html\u2019 Permits Cross-Site Scripting Attacks. http:\/\/www.securitytracker.com\/alerts\/2009\/Aug\/1022748.html"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"Lothaire M (2002) Algebraic combinatorics on words. Cambridge University Press","DOI":"10.1017\/CBO9781107326019"},{"key":"e_1_2_1_2_39_2","doi-asserted-by":"publisher","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Minamide Y (2005) Static approximation of dynamically generated Web pages. In: Proceedings of the 14th international conference on World Wide Web (WWW) pp 432\u2013441","DOI":"10.1145\/1060745.1060809"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Moser A Kruegel C Kirda K (2007) Exploring multiple execution paths for Malware analysis. In: Proceedings of the 2007 IEEE symposium on security and privacy (S&P) pp 231\u2013245","DOI":"10.1109\/SP.2007.17"},{"key":"e_1_2_1_2_42_2","doi-asserted-by":"crossref","unstructured":"Mohri M Nederhof MJ (2001) Regular approximation of context-free grammars through transformation. Robustness Lang Speech Technol 153\u2013163","DOI":"10.1007\/978-94-015-9719-7_6"},{"key":"e_1_2_1_2_43_2","unstructured":"M\u00f8ller A (2009) The dk.brics.automaton package. http:\/\/www.brics.dk\/automaton\/. Accessed July 2009"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/972695.972698"},{"key":"e_1_2_1_2_45_2","unstructured":"Newsham T (2000) Format string attacks. Bugtraq mailing list. http:\/\/seclists.org\/bugtraq\/2000\/Sep\/0214.html"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"crossref","unstructured":"Nguyen-Tuong A Guarnieri S Greene D Shirley J Evans D (2005) Automatically hardening Web applications using precise tainting. In: Proceedings of the 20th IFIP international information security conference (SEC) pp 295\u2013308","DOI":"10.1007\/0-387-25660-1_20"},{"key":"e_1_2_1_2_47_2","unstructured":"Pugh W (1994) The Omega project. http:\/\/www.cs.umd.edu\/projects\/omega\/"},{"key":"e_1_2_1_2_48_2","unstructured":"Rafail J (2001) Cross-site scripting vulnerabilities. CERT Coordination Center Carnegie Mellon University. http:\/\/www.cert.org\/archive\/pdf\/cross_site_scripting.pdf"},{"key":"e_1_2_1_2_49_2","doi-asserted-by":"crossref","unstructured":"Rozenberg G Salomaa A (ed) (1997) Handbook of formal languages. Word language grammar vol 1. Springer","DOI":"10.1007\/978-3-642-59136-5"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"crossref","unstructured":"Saxena P Akhawe D Hanna S Mao F McCamant S Song D (2010) A symbolic execution framework for JavaScript. In: Proceedings of the 31st IEEE symposium on security and privacy (S&P) pp 513\u2013528","DOI":"10.1109\/SP.2010.38"},{"key":"e_1_2_1_2_51_2","unstructured":"Saxena P Akhawe D McCamant S Song D (2010) Kaluza constraint solver. http:\/\/webblaze.cs.berkeley.edu\/2010\/kaluza\/"},{"key":"e_1_2_1_2_52_2","unstructured":"Shiflett C (2004) Security corner: cross-site request forgeries. http:\/\/shiflett.org\/articles\/cross-site-request-forgeries"},{"key":"e_1_2_1_2_53_2","unstructured":"Sullo C Lodge D (2010) Nikto. http:\/\/www.cirt.net\/nikto2. Accessed July 2010"},{"key":"e_1_2_1_2_54_2","doi-asserted-by":"crossref","unstructured":"Veanes M Bj\u00f8rner N de Moura L (2010) Symbolic automata constraint solving. In: Proceedings of the 17th international conference of logic for programming artificial intelligence and reasoning (LPAR) pp 640\u2013654","DOI":"10.1007\/978-3-642-16242-8_45"},{"key":"e_1_2_1_2_55_2","doi-asserted-by":"crossref","unstructured":"Xie T Marinov D Schulte W Notkin D (2005) Symstra: a framework for generating object-oriented unit tests using symbolic execution. In: Proceedings of the 11th international conference on tools and algorithms for the construction and analysis of systems (TACAS) pp 365\u2013381","DOI":"10.1007\/978-3-540-31980-1_24"},{"key":"e_1_2_1_2_56_2","doi-asserted-by":"crossref","unstructured":"Yu F Alkhalaf M Bultan T (2009) Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In: Proceedings of the 24th IEEE\/ACM international conference on automated software engineering (ASE) pp 605\u2013609","DOI":"10.1109\/ASE.2009.20"},{"key":"e_1_2_1_2_57_2","doi-asserted-by":"crossref","unstructured":"Yu F Alkhalaf M Bultan T (2010) Stranger: an automata-based string analysis tool for PHP. In: Proceedings of the 16th international conference on tools and algorithms for the construction and analysis of systems (TACAS) pp 154\u2013157","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"e_1_2_1_2_58_2","doi-asserted-by":"crossref","unstructured":"Yu F Bultan T Cova M Ibarra OH (2008) Symbolic string verification: an automata-based approach. In: Proceedings of the 15th SPIN workshop on model checking software (SPIN) pp 306\u2013324","DOI":"10.1007\/978-3-540-85114-1_21"},{"key":"e_1_2_1_2_59_2","doi-asserted-by":"crossref","unstructured":"Yu F Bultan T Ibarra OH (2009) Symbolic string verification: combining string analysis and size analysis. In: Proceedings of the 15th international conference on tools and algorithms for the construction and analysis of systems (TACAS) pp 322\u2013336. Springer","DOI":"10.1007\/978-3-642-00768-2_28"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-011-0214-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-011-0214-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-011-0214-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T15:55:25Z","timestamp":1641484525000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-011-0214-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":59,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1007\/s00165-011-0214-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-011-0214-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,11]]}}}