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.

Description in Czech
Cílem projektu je rozvinout technologii řešení řetězcových omezení (string constraint solving -- SCS) aby byla použitelná v analýze webových aplikací. Jde o aktuální cíl -- zranitelnosti typu cross-site scripting, SQL-injection nebo selhání bezpečnostních politik patří mezi hlavní zdroje bezpečnostních děr webových technologií. Způsobují astronomické náklady, které jsou pro vývoj webových aplikací významnou překážkou. Automatická a přesná analýza webových aplikací byla vždy vizí výzkumné komunity SCS. Její realizace je nyní v možnostech naší nejnovější metody SCS, která je výsledkem našeho dlouhodobého výzkumu automatové technologie a navzdory svému mládí překonává současný stav poznání. V rámci projektu posuneme škálovatelnosti a expresivitu této metody na potřebnou úroveň a začneme na ní stavět analýzu webových aplikací psaných v jazycích jako JavaScript nebo PHP. To vyžaduje řešit fundamentální problémy SCS, zdokonalit automatové techniky, na kterých náš přístup k SCS staví, a navrhnout škálovatelné analýzy pro dynamické jazyky kompatibilní s technologií SCS.

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

Key words in Czech
verifikace; analýza programů; bezpečnost; webové aplikace; SQL-injection; XSS; konečné automaty; řetězcová omezení; SMT;