Paper Review: From EVM to a Sound Control-Flow Graph

Paper Assumptions

They make the following assumptions that helps makes their task approachable with static analysis:

1. Restrict the stack size of EVM. The EVM uses a stack to manage computation; each operation can push to or pop items from the stack. By stating that the size of the stack can be bounded by a constant, the paper asserts that it is possible to predict the maximum size of the stack regardless of the path taken by the program execution up to the jump point. This constraint means that the possible states of the stack (and therefore the program) can be exhaustively enumerated or modeled up to any jump instruction. This predictability is crucial for creating a comprehensive CFG that accurately represents all possible execution paths in the contract.
2. Assume jump addresses constant. This means that the destination of a jump instruction does not change based on the state of the program or user inputs. In EVM, the address to which a jump will occur is placed onto the stack using a PUSH operation. Since it’s pushed onto the stack, the address must be known at the time the code is written, not calculated or altered during execution (will not depend on input values and are not stored in memory nor contract storage). They even collect these predetermined jump destinations before runtime in J (following image).
3. Recursion is not used in Solidity programs. In non-recursive programs, each function’s stack frame can be more predictable.
   

CFG EVM Blocks

The paper goes on to define what a block in EVM bytecode of a smart contract looks like. I visualized their blocks using the following diagram:

Stack State

The abstract state of the stack is defined as of the number of stack elements and sigma, which is the partial mapping relating some stack positions to a set of jump destinations (partial, because only certain positions in the stack are defined for mapping to jump destinations).

References

1. EVM codes. (n.d.). An Ethereum Virtual Machine Opcodes Interactive Reference. https://www.evm.codes/
2. Albert, E., Correas, J., Gordillo, P., Román-Díez, A. H. G., & Rubio, A. (2020, April 29). Analyzing Smart Contracts: From EVM to a sound Control-Flow Graph. arXiv.org. https://arxiv.org/abs/2004.14437