ByteSpector: A Verifying Disassembler for EVM Bytecode

Our contribution is a tool, ByteSpector, that can automatically construct proof objects from EVM bytecode. Proof objects are Dafny (a verification-friendly programming language) programs that encode the semantics of the bytecode, can be instrumented with specifications (e.g., absence of stack underflow) and reasoned about. ByteSpector is itself written in Dafny which has several advantages: the code is free of runtime errors (arithmetic, array-out-of-bounds, division-by-zero, etc.), and always terminates. Moreover, the Dafny code can be automatically translated to several target languages (e.g., C#, Python, Java, JavaScript) using the Dafny backends and re-used in other projects.

The EVM is a stack machine with a bounded stack for computations. Memory stores temporary data during execution, while global storage retains permanent contract state on the blockchain. Every computation consumes gas, a measure of computational cost, and results in one of the following outcomes:

• $\mathrm{■}$

  a successful termination, the effect of the computation is stored in the global storage.

• $\mathrm{■}$

  an abort (exception) e.g., caused by stack overflow, jumps to invalid targets, invalid number of arguments to an instruction, etc.

• $\mathrm{■}$

  an out-of-gas exception if the gas budget is exhausted before the end of the execution.

The EVM supports around 150 instructions to perform arithmetic or bitwise operations (e.g., ADD, SUB, AND, OR), stack operations (e.g., PUSH0, PUSH1, POP, SWAP1, DUP1), memory store/load operations e.g., MSTORE, MLOAD, global storage operations e.g., SSTORE, SLOAD, unconditional (resp. conditional) jumps, JUMP (resp. JUMPI), as well as blockchain specific operations (e.g., BALANCE, ADDRESS, GASLIMIT). A few instructions, such as PUSHes, have parameters and are encoded on a variable number of bytes. For example PUSH2 pushes two bytes on the stack and expects two bytes as arguments e.g., PUSH2 0x3056. We consider only well-formed EVM bytecode with valid opcodes and correct argument counts. Such bytecode can be decoded into an instruction sequence, as shown in Listing 1 (lines 5–18).

The EVM semantics, as per the Yellow Paper [13] define the state transition function of the EVM, that maps an EVM state $s$ to a new state $s^{\prime }$. A state includes bytecode, program counter $s.pc$ (instruction in the program to be executed next), the stack content $s.stack$, the memory content $s.memory$, gas left for the rest of the computation $s.gas$, global storage, and several other fields that we omit here. We let $|s.stack|$ be the size of the stack, and $s.stack[i..]$ be the sequence $s.stack$ without the first $i$ elements. Following the Dafny-EVM [5] semantics, we separate instruction semantics from gas consumption (ignored for now). For instance, if $s.pc$ points to a POP instruction, the next state $\text{Next}(s)$ is defined by:⁵⁵5For simplicity, we only define the PC and stack updates.

If the stack is empty, the execution aborts with an error state $s_{\perp }$. Otherwise, the program counter is incremented by one and the top element of the stack is removed.

The jump instructions JUMP and JUMPI (unconditional/conditional jump) are branching instructions that may transfer the control location ($s.pc$) to an address that is not the next instruction in the code. However, a nice feature of the EVM is that the target of a jump instruction must be a legal address, i.e., the target address of the jump must be a JUMPDEST instruction. For instance, TwoCalls, Listing 1, has 3 legal target addresses: 0x05, 0x0b, and 0x0d. As a result, given a program $p$, we can compute the set $\text{ValidJumps}(p)$ of legal target addresses in $p$ by identifying the JUMPDEST instructions. If the instruction at $s.pc$ is JUMP, $\text{Next}(s)$ is defined by:

For given bytecode $p$ and input $i$, the EVM semantics uniquely define $\text{run}(p,i)$, a finite sequence of EVM states (termination is ensured by the gas limit). The error state $s_{\perp }$ has no successors. The set of all possible executions of $p$ is: $\text{Runs}(p)=\{\text{run}(p,i)|i\in ℐ\}$ where $ℐ$ is the finite set of inputs (the calldata has a maximal size in the EVM).

A segment is a sequence of non-branching consecutive instructions ending at:

• $\mathrm{■}$

  branching instructions JUMP, JUMPI, or

• $\mathrm{■}$

  terminal instructions STOP, REVERT, RETURN, or

• $\mathrm{■}$

  any instruction before a JUMPDEST.

This ensures that $i$) jump targets start segments, preventing jumps into the middle of a segment and $ii$) there is a unique (linear) execution flow within each segment. Segments are shown in Listing 1 and the CFG of TwoCalls in Figure 2(a). We extend Next to segments to compute the state $\text{S}:\text{Next}(s)$ after executing all instructions in a segment S, returning an error state if execution fails before completion.

A CFG $g$ is a directed graph with nodes and edges and a designated initial node, $\text{Init}(g)$. Finite paths in the graph can be constructed by starting at $\text{Init}(g)$ and following the (directed) edges of the CFG. We let $\text{Paths}(g)$ be the set of finite paths in $g$ from $\text{Init}(g)$.

A graph $g$ is a CFG for program $p$ if the nodes of $g$ are labelled with segments of bytecode of $p$ or an error node to represent the error state $s_{\perp }$. Examples of CFGs for the program TwoCalls are shown in Figure 2, page 2. The nodes of the graph are assigned a unique id (#k, top left of node) and are labelled⁶⁶6Two nodes may be labelled with the same segment, the node/segment mapping is not necessarily 1-1. with segments (0–3).

A path $\pi$ uniquely defines a sequence of control locations, $\text{Execs}(\pi )$, obtained by concatenating the control locations of the segments on $\pi$. The set of (finite) sequences of control locations defined by a CFG $g$ is: $\text{Execs}(g)=\{\text{Execs}(\pi )|\pi \in \text{Paths}(g)\}.$ For instance, the path ${\pi }_2=\mathrm{\#}0\to \mathrm{\#}1\to \mathrm{\#}2\to \mathrm{\#}3$ in the CFG of Figure 2(a) defines the sequence of segments $[0,3,1,3]$ and the sequence of control locations [0x00,0x02, 0x04, 0x0d, 0x0e, 0x05, 0x06, 0x08, 0x0a, 0x00d, 0x0e] which is a feasible execution in TwoCalls. In the CFG Figure 2(b), the path ${\pi }_1=\mathrm{\#}0\to \mathrm{\#}1\to \mathrm{\#}2\to \mathrm{\#}1\to \mathrm{\#}2\to \mathrm{\#}1\to \mathrm{\#}3$ defines the sequence of segments $[0,3,1,3,1,3,2]$ which in turn defines the sequence of control locations obtained by expanding and concatenating the locations in each segment. Note that ${\pi }_1$ is not feasible in the actual program TwoCalls as they can be only two executions of Segment 3.

An important and desirable property of a CFG is that it over-approximates the set of executions of the program. Given an execution $e\in \text{Runs}(p)$, which is a sequence $s_0,s_1,\mathrm{\cdots },s_n$ of EVM states (Section 3.3), we define (the projection) $e.pc=s_0.pc,s_1.pc,\mathrm{\cdots },s_n.pc$ of corresponding sequence of control locations⁷⁷7The error state is mapped to $s_{\perp }.pc=-1$. (program counters), and we define the set of pc-runs of $p$ as $\text{PCRuns}(p)=\{e.pc|e\in \text{Runs}(p)\}.$ Given a program $p$ and a CFG $g$ for $p$:

This definition does not uniquely define a sound CFG for a program.⁸⁸8There may be an infinite number of sound CFGs for some programs. A CFG is a finite automaton and defines a regular language. The set of executions of a program may not be a regular language and sometimes can be over-approximated by an infinite number of more and more precise regular languages. Both CFGs in Figure 2 are sound. The CFG in Figure 2(a) is more precise than the one in Figure 2(b). The CFG in Figure 2(b) is an over-approximation of the CFG in Figure 2(a) and it contains a cycle that is not present in the CFG in Figure 2(a), and not even feasible in program TwoCalls. The previous observation allows us to define a simple algorithm to build a CFG for EVM bytecode: from each segment ending in a JUMP/JUMPI, we create edges to each segment starting with a JUMPDEST in the code. This over-approximates the set of sequences of control locations and produces a sound CFG but this over-approximation may be too coarse to be of any use (like the CFG in Figure 2(b)). Our objective is to compute sound CFGs that are as precise as possible.

To compute precise CFGs, we use abstract semantics (abstract interpretation) that track the program counter $s.pc$ and an abstract stack representation. While restrictive, this approach is sound and effective (see Section 6). This works well for two reasons:

1. 1.

   valid jump targets ($\text{ValidJumps}(\cdot )$) are known at compile-time.

2. 2.

   jump targets for JUMP/JUMPI are usually stored on the stack because: $i$) computing targets with arithmetic is rare due to gas costs and it is error-prone and $ii$) stack storage is cheaper than memory, so compilers optimise for gas by storing jump targets on the stack.

Since we do not track memory, CFG construction might fail if target addresses are stored there. However, experiments (Section 6) confirm this rarely occurs in practice.

An (EVM) abstract state $s$ of type EState is a pair $(s.pc,s.stack)$: $s.pc$ is the program counter, and $s.stack$ is an abstract stack, with elements either $v\in \text{ValidJumps}(p)$ or $\perp$ which is the unknown/arbitrary value. The abstract representation of the stack captures the size of the stack, and the target addresses of JUMP/JUMPI instructions.

The abstract semantics of EVM instructions (Figure 3) is given by the function⁹⁹9The complete definition of the Next^α function can be found in the code base here. $\text{Next}\text{<sup class="ltx\_sup"><span class="ltx\_text ltx\_font\_italic">α</span></sup>}:\text{EState}\to 2^{\text{EState}}$. The abstract semantics may contain more than one successor states for some instructions like JUMPI that have two possible successors: one for the case when the condition is true and one for the case when the condition is false. Other instructions are deterministic and have a single successor. What is captured in the semantics in Figure 3 is that the result of an addition operation “add and pop the two values at the top of the stack, and push the result” is abstracted as $\perp$. It is not likely to be a target jump. For some instructions like POP, Next^α is identical to Next. The abstract semantics¹⁰¹⁰10The PC advances by $k+1$ as PUSHk instructions have $k$ bytes as arguments. of PUSHk instructions track the concrete values that are pushed on the stack, but only if they are in $\text{ValidJumps}(p)$. For jump instructions, the abstract semantics check if the target address is a valid jump target and if the stack is not empty. This implies that if $s.stack[0]==\perp$, the target of the jump is not known, we end up in an error (abstract) state $s_{\perp }$.

Given a segment S, and an abstract state $s$ such that the start address of S is $s.pc$, we let $\text{S}:\text{Next}\text{<sup class="ltx\_sup"><span class="ltx\_text ltx\_font\_italic">α</span></sup>}(s)$ be the abstract states obtained after executing the segment S from $s$.

To compute the CFG of program $p$, we perform a standard Depth First Search (DFS) traversal of the graph defined by Next^α starting from the initial abstract state (0x00, []). It is not guaranteed that the DFS will terminate, as the stack may grow indefinitely.

To ensure termination, we limit the DFS to a given maximum depth (e.g., 100). If the maximum depth is reached (indicated by the result of the DFS), we can try a larger bound and iterate until the CFG fits within the bound. We write $\text{CFG}(p)$ for the CFG of program $p$ as computed by our DFS algorithm on abstract states.

The DFS algorithm completes the exploration of a branch when it encounters a previsoulsy visited node with the same abstract state. However, in some cases, this may lead to non-termination regardless of the maximum depth limit, as the abstract stack may grow arbitrarily large. In the next section we provide a sufficient condition to test whether two abstract states are equivalent and can be safely merged.

The bytecode in Listing 3 is a simple program that contains an unbounded loop. The CFG for this program is depicted in Figure 4. After $n$ execution of the JUMP instruction, the abstract stack content at PC location 0x02 is $[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},\perp ,\perp ,\mathrm{\cdots },\perp ]$ with $n$ unknown values.

The DFS algorithm introduced previously will not terminate for any maximum depth limit. However, we can see that the part of the stack that grows arbitrarily large is made of $\perp$ elements and this has no impact on the target of the JUMP instruction, which remains constant and equal to 0x02. For instance when we run the DFS algorithm we explore the path ${\pi }^{\prime }=(\mathrm{𝟶}𝚡\mathrm{𝟶𝟶},[])\to (\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸}])\to (\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},\perp ])$. If we execute Segment 1 from the state $(\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},\perp ])$, we end up in a state where the top of the stack is still 0x02. The state $(\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},\perp ])$ can be merged with the state $(\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸}])$ because every future execution after $(\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},\perp ])$ is covered by executions starting from $(\mathrm{𝟶}𝚡\mathrm{𝟶𝟸},[\mathrm{𝟶}𝚡\mathrm{𝟶𝟸}])$. To identify such configurations, we need to determine that every execution of Segment 1 results in the JUMP at its end always targeting 0x02.

We can provide a sufficient condition to test whether this is the case:

1. 1.

   Compute the weakest precondition that ensures that at the end of Segment 1 the value of the PC is 0x02;

2. 2.

   check whether this weakest precondition is invariant when executing Segment 1.

Assume we want to prove that after executing the JUMP instruction at 0x06 (line 11, Figure 4), the program counter is 0x02. As a JUMP instruction updates the program counter to the value at the top element of the stack, the least we can require is that, before we execute the JUMP instruction, the top of the stack contains 0x02. Any other choice would fail to result in pc == 0x02 after the JUMP. If execution begins in a state $s$ where the top of the stack holds 0x02, represented by the predicate $s.stack[0]==\mathrm{𝟶}𝚡\mathrm{𝟶𝟸}$, then executing a JUMP instruction guarantees that the next instruction to execute is at location 0x02.

To check the previous condition, we can compute the weakest precondition that ensures that executing a JUMP instruction leads to the postcondition pc==0x02. Weakest preconditions are standard concepts in formal verification and we illustrate the computation of weakest preconditions with a simple example. We let $\text{Wpre}(i,P)$ denote the weakest precondition (a predicate) for instruction $i$ to ensure that $P$ (a post condition) holds after the execution of the instruction. For instance, for the JUMP instruction, we have:

Computing weakest preconditions for sequences of instructions amounts to propagating the weakest preconditions backwards. For a sequence of instructions $\sigma +[a]$, and a predicate $P$, $\text{Wpre}(\sigma +[a],P)=\text{Wpre}(\sigma ,\text{WPre}(a,P))$ with $\text{Wpre}([],P)=P$. If we perform this computation for all the instructions in Segment 1, we obtain condition $C_1$:

To decide whether we can add a loop edge from node #1 to node #1 in the CFG of the program, we are going to check whether $C_1$ is preserved by Segment 1. If this is the case we have an invariant and a proof that any future execution of Segment 1 will end up in a state that satisfies $C_1$. To check whether $C_1$ is preserved by Segment 1, we can compute the postcondition of $C_1$ after executing Segment 1. If it implies $C_1$ then it is an invariant. We have implemented this check in the DFS algorithm, and we can successfully build a CFG for programs with unbounded stacks similar to Listing 3.

Finally, we apply a minimisation algorithm after the DFS to collapse nodes that are language-equivalent. Minimising the CFG amounts to minimising an automaton and can be done with standard techniques to partition the set of of nodes in equivalence classes. We have implemented a minimisation algorithm (a mixture of Moore and Hopcroft algorithms) that can generate a minimised version of the CFG. In the experiments the minimisation stage provides marginal benefits. It minimises very short subgraphs of the CFG, mostly nodes that contain segments STOP or REVERT instructions.

Given a program $p$, a node $n$ in $\text{CFG}(p)$ corresponds to an abstract state $n=(n.pc,n.stack)$. The component $n.stack$ is a list of either concrete values (target of jumps) or $\perp$. As a result we can view $n.stack$ as a finite set of contraints $n.\varphi$, of the form $n.stack[i]=v$, with $v\in \text{ValidJumps}(p)$ and write a node/abstract state in the form $(n.pc,n.\varphi )$. The constraints $n.\varphi$ enforces that some elements of the stack have some specific values.

To prove that $\text{CFG}(p)$ is sound, we need to show that it simulates the executions of the program $p$. To do so we prove the following:

Condition 1

The initial EVMState state $s_0$ of the execution of $p$ in the EVM satisfies the constraints of the initial node $\text{Init}(g)$, i.e., $s_0.pc=\text{Init}(g).pc$ and $s_0.stack$ satisfies the constraints $\text{Init}(g).\varphi$.

Condition 2

For any node $n=(n.pc,n.\varphi )$ in $\text{CFG}(p)$, and any concrete EVMState state $s=(s.pc,s.stack,\mathrm{\dots })$ that satisfies the constraints of $n$ i.e., $s.pc=n.pc$ and $s.stack$ satisfies the constraints $n.\varphi$, if $s^{\prime }=\text{Next}(s)$ then there exists a (direct) successor node $n^{\prime }=(p{c}^{\prime },{\varphi }^{\prime })$ of $n$ in $\text{CFG}(p)$ such that $s^{\prime }.pc=n^{\prime }.pc$ and $s^{\prime }.stack$ satisfies ${\varphi }^{\prime }$.

Proving these two properties for all nodes of the CFG ensures (by induction) that the CFG is sound. Condition 1 relating the initial state of the EVM and the initial node of the CFG is straightforward to prove: the initial state of the EVM starts at $pc=0$ and an empty stack, and the initial node of the CFG is associated with the segment of code starting at $pc=0$ and an empty stack. In the Section 5.3 we explain how to prove the second condition.

To prove the soundness of a CFG, we generate a Dafny proof object that encodes the bytecode semantics and node transitions.

The Dafny-EVM library provides functions like PUSH0, DUP, and POP to represent EVM instructions as state transformations, and EVMState that models the EVM state. Listing 4 shows the proof object for SimpleLoop, and Figure 5 shows the CFG for SimpleLoop. The semantics of Segment $0$ is implemented in ExecuteFromCFGNode_s0 lines 2-11. This function maps an EVM state,¹¹¹¹11The gas parameter is explained later. s0: EVMState to a state s’: EVMState obtained after executing the segment.

Each function has a precondition (requires) ensuring the $pc$ in the initial state s0 matches the segment start address. The CFG of SimpleLoop indicates that the successor of node $0$ is node $1$, so the line 10 is a call to the execution of the next node/segment, ExecuteFromCFGNode_s1. When we verify the proof object, Dafny checks that for all input states s0 that satisfy the precondition of ExecuteFromCFGNode_s0, the precondition of ExecuteFromCFGNode_s1 is satisfied at the callsite in line 10. If Dafny successfully verifies ExecuteFromCFGNode_s0 the condition 2 is verified for node $0$. The encoding of the other nodes and edges follow the same pattern.

Dafny requires proof of termination. For CFGs with loops, we use a gas parameter that strictly decreases with each transition in the CFG, proving that all paths terminate. This effectively verifies soundness for every path of arbitrary length, not actual gas usage.

Note that with our encoding and Dafny-EVM semantics, we prove more than soundness. In the Dafny-EVM, each operation e.g., Pop(s0) at line 38, may have some preconditions: e.g., the stack must not be empty, otherwise the POP operation results in a error state (stack underflow). In our encoding, we ensure that the stack preconditions of each Dafny-EVM function (Pop, PushN, Swap,…) in the code are satisfied. To do so, we add some constraints, for example, for ExecuteFromCFGNode_s1 to execute without error, we require that the stack on entry has more than two elements requires s0.Operands() >= 2.

To summarise, given a CFG, we can build a Dafny program, a proof object, that encodes the semantics of the bytecode in each node, and the transitions between nodes. If the proof object verifies, we have a proof that the CFG is sound (and no stack underflow exceptions¹²¹²12The absence of stack overflows can be guaranteed by adding a requirement on the capacity of the stack in the initial state. occurs.) This provides a soundness test for CFGs generated by ByteSpector.

The technique we have described previously has some limitations:

• $\mathrm{■}$

  for large segments of code, Dafny may be unable to verify some functions of the proof object due to the complexity of the code. Indeed, the Dafny-EVM semantics is quite complex for some opcodes (and the state has several components) and the verification of the proof object may require a lot of resources, and time out.

• $\mathrm{■}$

  some opcodes correspond to calls to other contracts e.g., CALL, DELEGATECALL, STATICCALL. In the CFG generation algorithm, the effects of these calls are abstracted, only taking into account the effect on the stack. The Dafny-EVM semantics of these instructions is more complex, involving the memory, storage, and the return value of the call.

The solution to these problems is to use an abstract version of the Dafny-EVM semantics. The abstract version is restricted to tracking the (abstract) stack and the program counter, and does include the memory, storage, etc.

For calls to other contracts, we encode the visible effect of the call on the stack: from the caller point of view, a CALL instruction pops $7$ arguments from the stack and pushes one return value (that could be an error code) if it does not abort. As a result the semantics of call instructions can be abstracted as a simple stack operation as shown in Listing 5.

To preserve soundness, we can prove that the abstract semantics simulate the Dafny-EVM semantics, and the proof can be written in Dafny. The proof for the POP instruction is specified in Listing 6.

ByteSpector consists of 6 modules, 36 files,  6000 lines of code, and 2200 lines of comments. The implementation is formally verified, ensuring no division-by-zero, out-of-bounds errors, or non-terminating functions. We use pre/postconditions and datatype constraints to enforce functional correctness. For example, the segment types in Dafny (JUMPSeg, STOPSeg) are constrained to end with the corresponding EVM instructions (JUMP, STOP) and this property is statically verified on the Dafny code. In our experimental evaluation, we have used the Java backend to generate a Java version of ByteSpector.

For experimental evaluation we use a dataset from the project EVMLiSA [2], available at https://github.com/lisa-analyzer/evm-lisa.

The initial dataset less_than_3000_opcode.txt has 1704 EVM bytecode contracts’ addresses. The contracts are published on Ethereum, live, and their bytecodes can be retrieved using the etherscan.io API. Each contracts has less than $3000$ opcodes. In our experiments we excluded the contracts containing the recently introduced instructions RJUMP, RJUMPI, RJUMPV and set the maximum depth to 100 for the CFG generation algorithm. These instructions do not present major difficulties and are already partially supported in our code base, but we have not yet fully integrated them in the CFG generation algorithm. Overall there are 1048/1704 contracts that 1) do not contain RJUMPs instructions and 2) the maximum depth is not reached during the generation of the CFG. With our technique we can generate and verify the CFG for almost all the contracts. A few of them contain jump targets that are stored in memory (probably using an old version of the Vyper compiler).