# Formalising a Simple Virtual Machine

Since starting my new role at ConsenSys, I have become interested in formalising virtual machines. For example, there are already some formalisations of the Ethereum Virtual Machine (e.g. in K, Lem, Coq). So, I figured it would be interesting to explore VM formalisation in a tool like Whiley (or similarly Dafny).

## Overview

In this post, I’m going to formalise a Simple Virtual Machine (SVM) which has only a few instructions. The goal is just to illustrate the technique and show that, using the formalisation, we can prove interesting properties.

The machine state includes a stack of `u16` words and a memory store of `u16` words. In addition, we have a program counter (`pc`) and a stack pointer (`sp`), along with a sequence of bytecodes. To illustrate, here are descriptions for a few example bytecodes:

BytecodeDescriptionStackMemoryPC
`NOP`No-operation`PC += 1`
`PUSH w`Push (immediate) word`.. ⟹ w ..``PC += 2`
`POP`Pop word from stack`.. w ⟹ ..``PC += 1`
`STORE k`Store word in memory`.. w ⟹ ..``data[k] = w``PC += 2`
`LOAD k`Load word from memory`.. ⟹ w ..``w = data[k]``PC += 2`
`ADD`Add words`.. v w ⟹ u ..``PC += 1`
where `u = (v+w) % 0x10000`
`SUB`Subtract words`.. v w ⟹ u ..``PC += 1`
where `u = (v-w) % 0x10000`
`MUL`Multiply words`.. v w ⟹ u ..``PC += 1`
where `u = (v*w) % 0x10000`
`DIV`Divide words`.. v w ⟹ u ..` if `w != 0``PC += 1`
where `u = v/w`
`JMP k`Unconditional Branch`pc += 2+k`
`JZ k`Conditional Branch`v ⟹ ..``pc += 2` if `v!=0`
`pc += 2+k` if `v==0`

This provides a fairly typical description for a bytecode machine (e.g. similar in style to that for the JVM). Each bytecode typically has an effect on the stack, and may also update memory. The effect on the stack is described as a rewrite popping zero or more elements on the stack, and pushing zero or more elements on the stack. For example, the effect `.. w ⟹ ..` for `POP` states that, for the bytecode to execute, there must be at least one word `w` on the stack and, afterwards, that word is removed (and everything else remains the same). Likewise, the memory effect for `STORE` is that the word `w` is written to address `k` in `data`. Finally, for completeness, note that (like most programming languages) integer division is non-Euclidean (i.e. rounds towards zero).

Whilst the above description is fairly clear and easy to follow, there are still some questions. For example, what happens if an address `k` is out of bounds for the `data` store? Likewise, can the stack ever be full? We might also be interested in checking whether an optimisation preserves the program’s semantics (e.g. that `PUSH 0; POP` is equivalent to an empty code sequence). With these questions in mind, it is useful to try and formalise our description in a machine-readable (and checkable) manner. To do this, I am of course going to use Whiley. However, it is worth pointing out that other systems could easily be used as well, (e.g. Dafny, the K framework, etc).

## Formalisation

We begin the formalisation process by defining the notion of a machine state as follows:

``````type SVM is {
u16 pc,
u16 sp,
u16[] data,
u16[] stack,
u8[] code
}
where sp <= |stack| && |stack| < 0xFFFF
where |code| <= 0xFF00
``````

This defines the essential components of our virtual machine. For simplicity, the `code` sequence is an array of bytes separate from the `data` section (i.e. we’re not following a Von Neumann Architecture). I’ve also imposed some additional constraints: (1) on `sp` and the maximum stack size; (2) on the maximum code size. In principle, we could limit the data size as well.

Before formalising individual bytecodes, its useful to have a notion of the machine being halted. This is just helpful to signal error states, and we can define it as follows:

``````property isHalted(SVM st) -> (bool r):
return st.pc >= |st.code|

property exitCode(SVM st) -> (u8 r)
requires isHalted(st):
return |st.code| - st.pc
``````

Basically, whenever the `pc` is passed the end of the `code` size, then the machine has “halted”. Once it reaches this state execution is finished. Furthermore, we’ll exploit the final `pc` value to determine an exit code, such that `exitCode(vm) == 0` indicates execution completed normally (more on this later).

### Bytecodes

We now formalise the semantics of each bytecode. That is, specify how each bytecode should execute. A simple example is the following:

``````property evalPOP(SVM st) -> (SVM nst):
if st.sp < 1:
return halt(st, STACK_OVERFLOW)
else:
return pop(st)
``````

This specifies that evaluating a `POP` bytecode requires at least one element on the stack, otherwise the machine halts (with exit code `STACK_OVERFLOW`). If there is one element, then it is popped off. This uses two helpers `halt` and `pop`, defined as follows:

``````property pop(SVM st) -> SVM
requires st.sp > 0:
return st{sp:=st.sp-1}

property halt(SVM st) -> SVM:
return st{pc:=|st.code|}
``````

Whilst these could have been written inline, I find it helpful to have descriptive names for the operations. I typically refer to these low-level building blocks as microcodes and, as for a physical machine, we’ll see these are reused a lot in defining the semantics of our bytecodes. Observe the precondition for `pop()` is that the stack cannot be empty. Also, the expression `st{sp:=st.sp-1}` returns `st` with field `sp` updated to `sp-1` and all others unchanged.

Another example to illustrate is the following:

``````property evalADD(SVM st) -> (SVM nst):
if st.sp < 2:
return halt(st, STACK_UNDERFLOW)
else:
u16 r = peek(st,1)
u16 l = peek(st,2)
u16 v = (l + r) % 0x10000
// done
return push(pop(pop(st)),v)
``````

Here, the right-hand side `r` is taken from the first (i.e. topmost) stack item, whilst the left-hand side `l` is from the second stack item. Furthermore, the addition itself must be modulo `0x10000` (i.e. `65536`) in order that the value assigned to `v` remains within bounds. Indeed if the modulo operation was left out, then the verifier would highlight a potential integer overflow (and this is where tools like Whiley really help). Again, our definition above uses some more microcodes:

``````property push(SVM st, u16 k) -> SVM
requires st.sp < |st.stack|:
SVM nst = st{stack:=st.stack[st.sp:=k]}
return nst{sp:=st.sp+1}

property peek(SVM st, int n) -> u16
requires 0 < n && n <= st.sp:
return st.stack[st.sp - n]
``````

This time, the precondition for `push()` requires that the stack cannot be full. Likewise, for `peek()`, we must have enough items on the stack to cover the one we’re after.

Finally, whilst I’ve only illustrated the semantics for a few example bytecodes above, you can see them all in the repo.

### Execution

The next piece of the jigsaw is bringing the semantics of all bytecodes together into one method responsible for executing the next bytecode. For this, we have `eval()`:

``````// Execute a "single step" of the machine.
property eval(SVM st) -> (SVM res)
requires !isHalted(st):
u8 opcode = st.code[st.pc]
// increment pc
SVM nst = st{pc:=st.pc+1}
// Decode opcode
if opcode == NOP:
return evalNOP(nst)
...
else if opcode == POP:
return evalPOP(nst)
...
else:
// Force machine to halt
return halt(nst)
``````

There are a few things to note about this: Firstly, it is rather ugly having this large sequence of `if` / `else if` statements. It would be better if we could at least use a `switch` statement. Unfortunately, at the moment, Whiley does not support this (though in the future it should). Secondly, the machine is set to `halt()` whenever an unknown instruction is encountered. Finally, a precondition for `eval()` is that the machine has not already halted.

## Something Useful!

Right, having specified our simple virtual machine the question is: what can we do with it? Well, the first and most obvious thing would be to generate code from it to give us a reference implementation. But, there are some other things we can do as well. For example, we can prove safety properties of bytecode sequences (e.g. that they don’t unexpectedly halt), or that certain compiler optimisations are sound, etc.

### Example 1

As a first example to illustrate, consider the following:

``````method test_add_01():
SVM m1 = execute(
[], // data
1024) // stack size
// Check expected output.
assert exitCode(m1) == OK
assert peek(m1,1) == 3
``````

This method is statically verified by Whiley. However its pretty simplistic since (in this case) it does not depend on any unknown (i.e. symbolic values). So, there isn’t any benefit to static verification over just executing the test.

We can make our example more interesting by introducing an unknown value as follows:

``````method test_add_02(u16 x):
SVM m1 = execute(
[x],
1024)
// Check expected output.
assert exitCode(m1) == OK
assert peek(m1,1) > x
``````

Here, `x` is an arbitrary value and we initialise our memory with `x` at address `0`. Thus, the above computes `x + 1`. However, attempting to statically verify this with Whiley produces an error:

``````main.whiley:5:assertion may not hold
assert peek(m1,1) > x
^^^^^^^^^^^^^^
``````

The problem is that the `ADD` may overflow around to `0`. That’s right! Our assertion doesn’t hold for the instruction sequence above. We can test this hypothesis by restricting our unknown value as follows:

``````method test_add_02(u16 x):
requires x < 65535:
...
``````

This essentially prevents the overflow case and, with that, the assertion will now statically verify.

### Example 2

As another example, lets consider the case for division.

``````method test_div_01(u16 x, u16 y):
SVM m1 = execute(
[x,y],
1024)
// Check expected output.
assert y == 0 || exitCode(m1) == OK
``````

This statically verifies because our final assertion is quite weak. Let’s assume we wanted something stronger. That is, a code sequence which would execute division safely for all values of `x` and `y`. Clearly, the above is not there yet. We need a check against `y` to handle when `y == 0`. Here’s one solution:

``````method test_div_02(u16 x, u16 y):
SVM m1 = execute(
[x,y],
1024)
// Check expected output.
assert exitCode(m1) == OK
``````

This introduces a conditional check using the conditional branch instruction, `JZ`. To keep the example short, the above just returns `x` when `y == 0` (but in principle it can do whatever we want). The above now statically verifies with Whiley. Just think about that for a second. It means we’ve proved (for all input values `x` and `y`) that the above code sequence always executes to completion on our simple virtual machine!

## Conclusion

We’ve formalised a very simple virtual machine in Whiley, and then proved some useful properties about (albeit small) bytecode sequences. In fact, there’s a lot more we could do with this tool, such as proving optimisations preserve a program’s meaning, etc. But, we can save those discussions for another day!

• KEVM: A Complete Semantics of the Ethereum Virtual Machine, Everett Hildenbrandt et al.. In Proc CSF, 2018. (PDF)

• Defining the Ethereum Virtual Machine for Interactive Theorem Provers, Y. Hirai. In Proc WTSC, 2017. (PDF)