Static Analysis of WebAssembly Programs by Abstract Interpretation and Environment Specification

In this thesis, we aim to design methods for enabling sound static analysis of bytecode-level programs. The target of this work is primarily enabling sound static analysis for WebAssembly (Wasm), with a particular focus on call graph extraction. The call graph of a program plays a crucial role in inter-procedural verification, and greater precision directly improves analysis quality. To this end, we formalize the standard semantics of a core subset of WebAssembly, the corresponding abstract semantics, and prove the abstract semantics sound w.r.t. the standard semantics. This forms the theoretical base of our analysis by Abstract Interpretation. Furthermore, we address the challenges posed by the weak encapsulation methods of WebAssembly modules. This translates into unknown dependencies that may significantly impact the semantics of Wasm programs, and, for certain tasks, it is necessary to provide the analysis with this semantic knowledge. To that end, we design a specification language that aids the analyzer when external dependencies are concerned. Building on top of the abstract semantics of WebAssembly and a specification engine for external dependencies, we validate our approach experimentally using our analyzer, dubbed wassilly, the first WebAssembly analyzer, to our knowledge, that enables sound analyses under unknown host dependencies. We observe that wassilly surpasses the state of the art in both soundness and precision, demonstrating improved results, thanks to its underlying methodology. We also analyze the limitations of our approach, in particular regarding the cost of manual specification for call graph analysis. This observation motivates strategies for mitigating this burden. The novel strategy we devised is an analysis targeting JavaScript hosts, the most widely used host language for WebAssembly-based applications. We proceed by identifying originated allocations and analyzing mutations of such allocations, detecting violations of pre-defined contracts of how hosts can interact with modules. We present an initial formalization of this approach, with intuitions on how such an analysis can reduce the need for manual specification.