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.