String Constraints for Security Analysis

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

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.