CHC-based Automated Verification of WebAssembly Programs
Programming Languages
Summary
The authors developed a way to automatically check parts of WebAssembly programs to make sure they work correctly without running them. They focused on two tricky problems: handling indirect function calls without exploring too many possibilities and managing big error-handling functions called panic handlers. To solve these, they filtered function calls using type information and simplified the panic handlers by analyzing how the program flows. Their early tests showed that these techniques worked well.
Authors
Akihisa Yagi, Ken Sakayori, Naoki Kobayashi
Abstract
WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A naïve approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.