Formally Verifying WebAssembly with KWasm Towards an Automated Prover for Wasm Smart Contracts
Ladda ner
Typ
Examensarbete för masterexamen
Program
Computer systems and networks (MPCSN), MSc
Publicerad
2020
Författare
Hjort, Rikard
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
K , K framework , WebAssembly , Wasm , Ethereum , Ewasm , formal methods , formal verification , semantics , specification