Verifying Wasm Functions: Part 1

by Rikard Hjort and Stephen Skeirik

12 min readJan 7, 2020

This blog post is the second in a series of posts written by Runtime Verification, Inc. and sponsored by dlab on web assembly (Wasm), and more specifically KWasm, a tool for doing formal verification of Wasm programs. If you missed the first post, feel free to take a look!

Today, we will be starting a mini-series on exploring how to verify a fragment of the WRC20 contract, i.e., a simplifed Wasm implementation of the Ethereum smart contract ERC20, which provides an API for token exchange that is usable by other kinds of smart contracts (e.g., digital wallets). This is relevant because the Ethereum virtual machine (EVM) is migrating to a Wasm implementation dubbed EWasm.

The first part of the mini-series will be a deep dive into what formal verification is and how we can use the K Framework to help automate this process. In the second part, we will show how we can formally verify a fragment of a program i.e., the WRC20 smart contract which is written in WebAssembly.

Our desire is that you will not only enjoy this technical adventure but also walk away knowing just a bit more about Wasm and how the formal verification process proceeds in practice.

A Whirlwind Tour of Formal Verification

Formal verification is a process by which a system (typically, a software system) is proved to be consistent with a set of formalized requirements. To understand what we mean by this, it is helpful to zoom out and recall how the system development proceeds in the large.

Fundamentally, system or product development is an iterative process where we are trying to relate a set of system requirements with a system implementation. More formally, we might write:

Implementation => Requirements

Which is to say, our implementation satisfies our requirements (and possibly more things).

Of course, this leads us to an important question: how can we know that our system implementation satisfies our system requirements? In our view, formal verification is merely a systematic method of answering this question. Stated differently, formal verification shifts the question of system correctness from informal human reasoning to formal mathematical reasoning. But really, why should we bother with formal verification? What is the benefit? There are two enormous benefits we obtain when we embrace the practice of formal verification:

Systematic, formal, and mathematical reasoning gives us a precise language for thinking about system design;
Many important formal verification tasks are automatable by a computer; this means we can consider very difficult problems that would be intractable for a human to solve.

Now, without further ado, we present an overview of how formal verification (for software systems) proceeds in the figure below:

Overview of the Formal Verification Process

In the figure, boxes represent different artifacts that are produced during the verification process, while connecting lines represent transformations from one kind of artifact into another. Double connecting lines represent transformations that preserve all essential information; they are supposed to be reminiscent of the equality symbol (=) from mathematics. All lines are annotated by the entity needed to perform the desired transformation. Let us define the various artifacts and entities that appear in our figure:

Requirements: a human language document that describes what our system should do;
Developer: a human expert that produces source code based on requirements;
Compiler: a special program that transforms code from one language into another language;
Verification expert: someone who understands how to formally relate requirements to source code;
Tests: special code that interfaces with and checks that our source code behaves correctly in certain cases;
Source code/assembly: the code that (hopefully) implements all of our requirements;
Formalized requirements: a mathematical restatement of our requirements;
Semantics: a special compiler that maps code into its mathematical meaning;
Formalized system specification: the mathematical meaning of some source code;
Theorem prover: a computerized assistant that helps a user solve mathematical problems.

With these details in hand, let us re-examine the figure. In conventional software development, a developer (and typically also compiler) together turn system requirements into executable code. A (possibly different) developer will then take those same system requirements and write tests that hook into the executable code, ensuring that certain code paths return desired results. These tests are helpful in showing that our code is correct, but we already know testing is not enough. While tests can demonstrate the presence of bugs, they typically can never prove the absence of bugs. The beauty of formal verification is that we can provably demonstrate a correspondence between our requirements and our system specification, i.e., we can prove that our source code has no bugs.

A key tool that we use in this process is a semantics. You can think of a semantics as a compiler that maps code into its mathematical meaning. Another key tool that we use is a theorem prover, which is just a computer program that assists us in solving mathematical problems and avoiding careless errors. Since our formalized requirements and formalized system specification are both mathematical statements, we can use a theorem prover to talk about how they are related. Thus, to answer the question:

How can we know that our system implementation satisfies our system requirements?

We shift our thinking into the formal, mathematical domain and instead ask:

Can our theorem prover show that our formalized system specification satisfies our formalized requirements?

Thus, we have come full circle and can now see how formal verification shifts our investigation from informal human reasoning to formal mathematical reasoning.

The Main Phases of Formal Verification

With that explanation out of the way, let’s examine the phases of formally verifying a program. Obviously, to formally verify anything, we first need to have some requirements and a program in mind. Thus, let’s assume we already have them. Then we will:

Specify Language Semantics — must be done once for each programming language that consider (e.g., C, Javascript…) and can be used for all programs in that language;
Formalize Program Requirements — convert natural language requirements document into an equivalent mathematical description;
Prove Correspondence — use a theorem prover to prove the desired equivalence between the formalized requirements and formalized system specification.

We are going to illustrate this process concretely, using our tool, the K Framework. The K Framework (which we abbreviate as K) can be used to specify language semantics as well as verify programs written in a specified language.

Specifying Language Semantics

Recall that a semantics is a way of assigning a mathematical meaning to a program. What is the mathematical meaning of a program? We can understand a program as a function over system states, e.g. the state of the memory, the hard disk, network, etc…

A K language semantics consists of three parts:

a syntax for the language (i.e., a parser for programs in the language);
an XML tree that defines the system states;
and a set of transition rules that map systems states to new system states (by executing programs in the language).

The bulk of a semantics is composed of transition rules. For a typical language semantics, an initial system state for a program P is just:

default initialized values (e.g., the object Object in Java);
a parsed program P stored in the <k> cell (a cell is just a fragment of the system state).

When the program terminates, the program P will have been totally consumed by the transition rules, and the rest of the state will have changed in some meaningful way.

Here’s an example of a simple rule in KWasm. The Wasm drop instruction simply drops the top element on the stack.

rule <k> drop => . ... </k>
      <valstack> _ : VALUESTACK => VALUESTACK </valstack>

Here’s how you read it:

An XML pair <name> and </name> introduces a cell, i.e., a fragment of the system state;
Anywhere a double arrow => appears in a cell, it describes how the system state changes when the rule is applied — the current state is described by the pattern on the left-hand side — the successor state is described by the pattern on the right-hand side;
The cell <k> is distinguished; it contains the program code;
In this rule, the first element of the <k> cell (the next instruction to be executed) is drop — the ellipses (…) refers to the (possibly empty) list of the instructions following drop;
The <valstack> cell contains a list of values where : is list concatenation;
In the successor state after the rule is applied, the drop instruction is deleted from the program code to be executed and the top value in the <valstack> cell is also deleted.

Formalizing Program Requirements

In K, the task of formalizing program requirements is also done via rules of the form S=>S' such that:

S is a pattern that describes a (potentially infinite) set of initial system states;
S’ is a pattern that describes a (potentially infinite) set of acceptable final states.

We want to ensure that all initial states S end up in some acceptable final state S’. Let us see a more concrete example rule:

rule <k> foo X Y => Z ... </k>
  requires Z >Int X +Int Y

This rule symbolically specifies a (possibly infinite) set of program states where the <k> cell contains the program fooXY where X, Y, and Z are integer variables (and all other cells are left unspecified). The requirement will be satisfied whenever all executions of program fooXY starting in all possible system states either:
1. do not terminate, or;
2. terminate with integer Z on top of the <k> cell, with everything else that initially followed fooXY (indicated by …) left unchanged, such that Z is larger sum of X and Y.

For example, if our programming language semantics contained the following rules, the requirement would be satisfiable:

rule [a] <k> foo X Y => foo Y X ... </k>
rule [b] <k> foo X Y => X +Int Y +Int 1 ... </k>

Clearly, any path that applies rule [b] would immediately satisfy the program requirement. Of course, if we apply rule [a] forever, the program will never terminate (so we ignore such executions).

Interestingly, writing down requirements precisely is often the most challenging part of the verification process. This is typically because we have not fully considered all possible edge cases (e.g., what happens when x<=0) or because we have assumptions about our system that have often never been written down or even verbalized.

Proving the Correspondence

Here we use the K Framework’s built-in theorem prover to formally prove the correspondence between our program meaning and our program requirements. At this point, our situation is as follows:

Our formalized program requirements has provided us with:

a (possibly infinite) set of initial program states and;
a (possibly infinite) set of acceptable final program states.

2. Our programming language semantics completely determines how initial states can evolve into final states.

Thus, our theorem prover can, in general, test every possible execution path and check that the requirements hold at the end. But, that being the case, how can this formal proof process be challenging? There are two main ways that things can go wrong:

the theorem prover is a computer program and it may take too long or run out of memory;
the theorem prover may get stuck because it could not prove something (either because it is non-trivial or because it doesn’t understand our intended program meaning).

This leads us to primary proof search process that we call here the verification cycle:

What this means is: if the proof is taking too long or if we get stuck, we will:

Examine the proof output term to understand why we are stuck.
Extract any necessary lemmas that will help the stuck proof make progress or add assumptions about our initial state (called strengthening the pre-condition) in order to prune useless paths.
Repeat the proof with the simplified claims.

A Very Simple Proof

As mentioned above, proof obligations in K are specified exactly like regular semantic rules.

Just like in a semantic rules, values referenced by rules mentioned may be symbolic.

A set of these proof obligations is called a specification.

Below is a simple specification which asserts that copying the value of a local variable to the stack with local.get and then writing that value back to the same variable with local.set

terminates, as expressed by the whole program rewriting to ., and
produces no other changes in the state, since there are no other rewrites.

module LOCALS-SPEC
  imports WASM-TEXT
  imports KWASM-LEMMAS
  rule <k> (local.get X:Int) (local.set X:Int) => . ... </k>
       <locals>
         X |-> < ITYPE > VAL
       </locals>
endmodule

The program in the <k> cell is simple to verify, because during the course of its evaluation, only one semantic rule ever applies at a time.

The prover will first need to apply a statement sequencing rule followed by parenthesis unpacking.

rule <k> (S:Stmt SS) => S ~> SS ... </k>
  requires SS =/=K .Stmts
rule <k> ( PI:PlainInstr ):FoldedInstr => PI ... </k>

Now the <k> cell of the spec contains

local.get X ~> (local.set X)

Next, the rule for local.get applies

rule <k> local.get I:Int => . … </k>
     <valstack> VALSTACK => VALUE : VALSTACK </valstack>
     <locals> … I |-> VALUE … </locals>

giving the new configuration (after . is removed and parenthesis unpacking)

<k> local.set X:Int … </k>
<valstack> < ITYPE > VAL : VALSTACK </valstack>
<locals>
 X |-> < ITYPE > VAL
</locals>

where VALSTAK is whatever the stack contained before.

Lastly, the rule for local.set applies

rule <k> local.set I:Int => . … </k>
     <valstack> VALUE : VALSTACK => VALSTACK </valstack>
     <locals> … I |-> (_ => VALUE) … </locals>

giving

<k> . … </k>
<valstack> VALSTACK </valstack>
<locals>
 X |-> < ITYPE > VAL
</locals>

which matches the right-hand side of the configuration.

In this simple case we were able to simply state how a program would terminate and leave the state unchanged, and the prover could infer it for us. Indeed, in making this example, the specification above was written and proved on the first try. The proving process is often not so straight-forward, however, and may require some tweaking and ingenuity.

A trickier example

Some proofs require that we further specify our intended semantics and encode the invariants of the transition system.

As an example, we take the exact analogue of our previous proof. Only this time, instead of modifying local variables we are modifying heap storage.

#inUnsignedRange captures the invariants that all integer values will be represented by their corresponding unsigned value, regardless of signed representation.

An invariant the semantics have been designed to maintain (but that we have yet to prove it maintains) is that of #isByteMap

module MEMORY-SPEC
  imports WASM-TEXT
  imports KWASM-LEMMAS
  rule <k> ( i32:IValType.store (i32.const ADDR)
            (i32.load           (i32.const ADDR)):Instr):Instr => . ... </k>
       <curModIdx> CUR </curModIdx>
       <moduleInst>
         <modIdx> CUR </modIdx>
         <memAddrs> 0 |-> MEMADDR </memAddrs>
         ...
       </moduleInst>
       <memInst>
         <mAddr> MEMADDR </mAddr>
         <msize> SIZE </msize>
         <mdata> BM   </mdata>
         ...
       </memInst>
     requires #chop(<i32> ADDR) ==K <i32> EA
      andBool EA +Int #numBytes(i32) <=Int SIZE *Int #pageSize()
      andBool #isByteMap(BM)
endmodule

However, the verification for this specification will fail.

The reason is that storing to and reading from memory is more complicated than storing local values.

When a value is stored to memory it is spliced into bytes. When a value is read from memory, the bytes are assembled into an integer value.

Conceptually, the load instruction will put on the stack the following:

val=bm[addr]+(bm[addr+1]+(bm[addr+2]+bm[addr+3]*256)*256)*256

The store operation takes the value off the stack, and conceptually stores the following sequence of bytes:

           bm[addr] := val mod 256
           bm[addr + 1] := (val / 256)      mod 256
           bm[addr + 2] := (val / 256^2)     mod 256
           bm[addr + 3] := (val / 256^3)     mod 256

If we plug val into the above equation it becomes clear that the modulus and division operators will cancel out exactly so all we are doing is writing the values in each address back.

This type of reasoning presents a challenge for the K prover using the current semantics. The semantics uses pure helper functions, #setRange and #getRange for writing to and reading from the byte map. These functions expand to a series of #set and #get, that get and set individual bytes of the memory.

We added the following lemmas, which should obviously hold in integer and modular arithmetic.

rule (X *Int N +Int Y) modInt N => Y modInt N
rule (Y +Int X *Int N) modInt N => Y modInt Nrule 0 +Int X => X
rule X +Int 0 => Xrule (Y +Int X *Int N) /Int N => (Y /Int N) +Int X

Together, they help eliminate the expressions for assignment to

    bm[addr]:= bm[addr]         mod 256bm[addr + 1]:= bm[addr] /256    mod 256 + bm[addr + 1]       mod 256bm[addr + 2]:= bm[addr] /256^2  mod 256 + bm[addr + 1]/256   mod 256
             + bm[addr + 2]     mod 256bm[addr + 3]:= bm[addr] /256^3  mod 256 + bm[addr + 1]/256^2 mod 256
             + bm[addr + 2]     mod 256 + bm[addr + 3]       mod 256

We also add the following two lemmas:

rule #get(BMAP, IDX) modInt 256 => #get(BMAP, IDX)
 requires #isByteMap(BMAP)
rule #get(BMAP, IDX) /Int 256 => 0
 requires #isByteMap(BMAP)

They state that as long as a byte map maintains its intended invariant — that all values are integers from 0 to 255, inclusive — we may discard the modulus on the values, and the divisions amount to zeroing them.

With all these lemmas added to the theory, the proof goes through.

What’s Next

We covered a lot of highly technical ground today. Thanks for sticking with us this far. In the next post in this mini-series, we will show how to apply the concepts defined today using the K Framework to verify a fragment of the WRC20 program!