Path sensitive static program analysis for web applications

Web applications are pervasive these days. They are becoming the platforms for our daily activities such as reading, shopping, banking, social networking, gaming, and even working. While they are replacing the role of traditional PC-based software applications, they also inevitably inherit the complexity and error-proneness of those applications. Given that valuable and sensitive data are processed and stored by web applications, program defects could pose serious threats to user experience, data integrity, and information security. To locate these problems automatically, we develop static program analysis techniques on both client-side and server-side scripts to identify various kinds of flaws including concurrency issues in JavaScript, server-side external resource contention problems and Remote Code Execution vulnerabilities. The analysis focuses on encoding a web application to datalog languages or constraints. The constraints generated from the analysis are resolved to identify defects. In the path-sensitive analysis, web applications are modeled as constraints; solving such constraints identifies the failure inducing path and inputs. Since web applications are string-intensive, the key challenge is to reason about string and non-string constraints cohesively. However, such capabilities are limited in existing constraint solvers. Many support either only non-string operations or only string operations. Some can handle both but they have limitations in expressiveness, applicability and efficiency. Thus, we develop Z3-str, a new general purpose string solver, on top of one of the most popular SMT engines, Z3, to support cohesive solving of string and non-string constraints. We also propose a practical deterministic procedure to decide the satisfiability of string equations. This is the underlying theory of Z3-str. It leverages the practical insights we have gained from real-world application analysis, and is consequently considerably easier to analyze and implement without losing much expressiveness