Доверя'й, но проверя'й: SFI safety for native-compiled Wasm

interpretation. Abstract interpretation [20] has been verifying program properties and finding bugs for over forty years. The Astrée static analyzer [21] has verified absence of certain errors in space vehicles [8], and many works [58], [78] use abstract interpretation for everything from verification to synthesis. There are even verified static analysis passes and frameworks [11], [30], [12]. Like these works, VeriWasm uses a verified abstract interpretation passes but specifically focuses on showing that binaries are safely sandboxed. Bug finding. Bug finding tools can also identify security flaws. They use techniques like symbolic execution [15], concolic execution [24], [85], [63], fuzzing [82], [1], and binary instrumentation [54]. These tools find several classes of security bugs like use-after-frees [64], race conditions [61], [65], stack overflows [58], and more; some use fast but unsound analysis to quickly find bugs with low false positives [9]. In contrast, VeriWasm cannot check for general classes of security bugs and instead only validates the Wasm security properties; it uses a sound analysis and may produce false positives (§VI).