基于约束 Horn 子句的 WebAssembly 程序自动验证
CHC-based Automated Verification of WebAssembly Programs
浏览论文内容
中文总结 AI 辅助
研究基于约束 Horn 子句的 WebAssembly 程序自动验证方法，通过利用类型信息过滤间接函数调用候选者，用控制流分析总结恐慌处理程序，经初步实验证实该方法有效。
中文摘要 AI 辅助
WebAssembly 是一种基于栈的命令式语言，广泛用于开发安全高效的 Web 应用程序。本文提出了一种使用约束 Horn 子句（CHC）可满足性求解器对 WebAssembly 的一个子集进行自动静态验证的方法。主要挑战包括如何有效处理间接函数调用以及如何分析庞大的恐慌处理程序。对于间接函数调用问题，通过利用类型信息并为每个间接函数调用过滤候选者来解决。对于恐慌处理程序问题，通过控制流分析对其进行总结来缓解。通过初步实验证实了该方法的有效性。
英文摘要
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.
