String Constraints for Security Analysis

verification; security; web-applications; SQL-injection; XSS; automata; string constraints; SMT; automated reasoning

We aim at advancing the technology of string constraint solving (SCS) to enable security analysis of web applications. It is a timely objective---vulnerabilities to cross-site scripting, SQL-injection, or security policy malfunctions are among the main sources of security breaches of today's web technologies. They elicit astronomical costs that pose a significant obstacle for the industry. Automatic and precise analysis of web applications has always been the vision of SCS research community. Realizing it is within the potential of our recent SCS method that showcases our long term research of automata technology and, despite its youth, surpasses the state of the art. We propose to perfect our SCS technique so that it reaches the required scalability and expressiveness, and to initiate a development of SC enabled analyses of web applications written in languages such as JavaScript or PHP. It requires tackling fundamental questions about SCS, further develop automata techniques we build on, and to propose scalable analyses for dynamic languages compatible with the SCS technology.