Project Proposal

dLab Fellowship Program: Tuning KWasm for Symbolic Execution

Introduction

Runtime Verification developed the KWasm semantics in anticipation of the next generation blockchains, many of which use Wasm (WebAssembly). KEVM is used extensively by Runtime Verification and the broader Ethereum community to verify smart contracts, but the impending switch to eWasm as the target VM (and development of other blockchains targeting Wasm) means that the tooling around KEVM needs to be retargeted to Wasm. The modular nature of the K Framework means the retargeting effort is minimal, but there is still work needed in tuning the semantics for symbolic execution.

Note that this tuning will come in three forms: (i) tuning the Haskell backend of K to be able to handle KWasm proofs, (ii) tuning KWasm to be better suited for symbolic execution, and (iii) adding standard lemmas to the global bag that all KWasm proofs can use. All three categories will benefit all users of KWasm trying to verify smart contracts written in Wasm.

Deliverables:

• Selection of 6 Wasm programs to verify using KWasm, each incrementally using more features of Wasm and more complicated program logic.
• K specification of each algorithm, 1 per month, along with updates to KWasm needed to make verifying that algorithm feasible.
• Integration of developed K specs into KWasm CI so that updates to KWasm do not break them.
• JelloPaper-like online documentation updated on pushes to KWasm repository.

From the start date, we will (i) select the program to verify for that month, (ii) implement it in Wasm, and (iii) verify it. One week will be allocated to select and write the program, and three weeks will be allocated to verify said program using KWasm. Each program will be allocated roughly a month.

The first algorithm to verify will be a WRC20, which is a Wasm adaption of an ERC20. ERC20 is the most basic token standard used in Ethereum, and is the building block of many other tokens. This program has no loops and no heap manipulation, so serves as a nice first step towards ironing out issues in KWasm regarding symbolic execution, while also being highly applicable to the smart contract domain.

Community Value:

Already KEVM is used extensively outside of Runtime Verification for verification of smart contracts (most notably by the Ethereum Foundation and MakerDAO). Runtime Verification already had to tune KEVM for symbolic execution “on-the-fly”, often extending the time that our verification engagements took with work not directly related to engagement. Each external actor also benefited from this work, as they did not need to tune the semantics themselves. This proposal seeks to front-load as much of that tuning effort as possible, so that as verification engagements for Wasm roll in both Runtime Verification and the broader community can benefit from a ready-to-go KWasm semantics. By the end of this engagement, “KWasm will be ready to use for commercial verification by RV and other companies”.

Start by reviewing the KWasm semantics and the proposal's deliverables, especially the planned WRC20 verification and KWasm CI integration. Done would require selecting and verifying the proposed Wasm programs, updating KWasm as needed, integrating their K specifications into CI, and updating online documentation.