Configurable and Sound Static Analysis of JavaScript: Techniques and Applications

JavaScript is widespread. Web developers use JavaScript to enrich user experience via dynamic content ranging from scripts to enhance a web page's appearance, to full-blown web applications, to extending the functionality of web browsers in the form of browser addons. Desktop developers use JavaScript, e.g., for OS applications in Windows 8. JavaScript's growing prominence means that secure, correct, and fast JavaScript code is becoming ever more critical. Static analysis traditionally plays a large role in providing these characteristics: it can be used for security auditing, error-checking, debugging, optimization, and program refactoring, among other uses. Thus, a sound, precise static analysis platform for JavaScript can be of enormous advantage.In this thesis, we present our work on creating a sound, precise, configurable and fast static analysis for JavaScript called JSAI that we have made openly available to the research community. JSAI is both a practical tool for JavaScript static analysis and also a research platform for experimenting with static analysis techniques. JSAI showcases a number of novel techniques to soundly compute a combination of type inference, pointer analysis, control-flow analysis, string analysis, and integer and boolean constant propagation for JavaScript programs. It also provides a unique method for modularly configuring analysis precision that is based on fundamental new insights into the theory of static analysis. We describe precision-increasing techniques for the analysis using type refinement; and performance-increasing techniques for the analysis based on parallelization of JSAI. As an example use-case for JSAI, we discuss a novel security analysis for JavaScript-based browser addon vetting