Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts

Abstract

A smart contract is immutable, public bytecode which handles valuable assets. This makes it a prime target for formal methods. WebAssembly (Wasm) is emerging as bytecode format for smart contracts. KWasm is a prototype mechanization of Wasm in the K framework which can be used for formal verification. The current project aims to verify a single Wasm smart contract, a simple token contract. First, we complete the KWasm semantics to be able to deal with modules and test the semantics against the official conformance tests. This reveals several shortcomings of the conformance tests. Second, we create an Ethereum embedding by creating a separate Ethereum client semantics and combining it with the KWasm semantics through a thin, synchronizing interface. This embedding is then unit tested, including conformance tests for two variants of the WRC20 contracts. Thirdly, we use the KWasm semantics to prove properties of incrementally more complex Wasm programs, with an emphasis on heap reasoning, culminating in the verification of a helper function that reverses the bytes of a 64-bit integer. In the process we add 25 axioms that get upstreamed into K, and several more that are useful for general Wasm verification.