WeVerca: Web Applications Verication for PHP (Tool Paper)

Abstract. Static analysis of web applications developed in dynamic lan-guages is a challenging yet very important task. In this paper, we present WeVerca, a framework that allows one to dene static analyses of PHP applications. It supports dynamic type system, dynamic method calls, dynamic data structures, etc. These common features of dynamic lan-guages cause implementation of static analyses to be either imprecise or overly complex. Our framework addresses this problem by dening end-user static analyses independently of value and heap analyses necessary just to resolve these features. As our results show, taint analysis dened using the framework found more real problems and reduced the number of false positives comparing to existing state-of-the-art analysis tools for PHP.