This EIP specifies validation rules for some important safety properties, including
* valid instructions,
* valid jump destinations,
* no stack underflows, and
* no stack overflows without recursion.
Valid contracts will not halt with an exception unless they either run out of gas or overflow stack during a recursive subroutine call.
Code must validated at contract creation time – not runtime – by the provided algorithm or its equivalent. This is a one-pass algorithm. It is (and must be) linear in the size of the bytecode, so as not to be a DoS vulnerability.
## Motivation
Validating safe control flow at creation time has a few important advantages.
* Jump destination analysis does not need to be performed at runtime, thus improving performance and preventing denial of service attacks.
* Jump destination validity does not need to be checked for at runtime, improving performance.
* Stack underflow does not need to be checked for at runtime, improving performance.
The runtime addressing of `JUMP` has long been seen as an obstacle to statically proving this sort of safety, but that very feature has been considered necessary to implement the return jump from a subroutine. But consider this example of calling a minimal subroutine.
```
ADD:
RTN_ADD
0x02
0x03
ADDITION
jump
RTN_ADD:
jumpdest
swap1
jump
ADDITION:
jumpdest
add
swap1
jump
```
Note that the return address and the destination address are pushed on the stack as constants, so the `JUMP` instructions are in fact static, not dynamic – they jump to the same `PC` on every run. We do not need (nor typically use) dynamic jumps to implement subroutines.
Since the jumps we need in practice are static we can validate their safety with a static analysis of the code. And since can, we should.
## Specification
### Dependencies
We need [EIP-3540: EVM Object Format (EOF)](./eip-3540.md) to forbid invalid instructions.
### Validity
We define safety here as avoiding exceptional halting states:
* Valid contracts will not halt with an exception unless they
* run out of gas or
* overflow stack while making a recursive subroutine call.
Attempts to create contracts that cannot be proven to be valid will fail.
#### Exceptional Halting States
_Execution_ is as defined in the [Yellow Paper](https://ethereum.github.io/yellowpaper/paper.pdf) a sequence of changes to the EVM state. The conditions on valid code are preserved by state changes. At runtime, if execution of an instruction would violate a condition the execution is in an exceptional halting state. The Yellow Paper defines five such states.
1. Insufficient gas
2. More than 1024 stack items
3. Insufficient stack items
4. Invalid jump destination
5. Invalid instruction
We would like to consider EVM code valid iff no execution of the program can lead to an exceptional halting state, but we must be able to validate code in linear time to avoid denial of service attacks. So in practice, we can only partially meet these requirements. Our validation algorithm does not consider the codes data and computations, only its control flow and stack use. This means we will reject programs with any invalid code paths, even if those paths are not reachable at runtime. Further, conditions _1_ and _2_ Insufficient gas and stack overflow must in general be checked at runtime. Conditions _3_, _4_, and _5_ cannot occur if the code conforms to the following rules.
#### The Rules
> This section extends contact creation validation rules (as defined in EIP-3540.)
0. All instructions are valid.
1.`JUMP` and `JUMPI` address only a constant, valid `JUMPDEST`.
2. The `stack depth` at the end of a _basic block_ is always always positive.
3. The `stack pointer` is always positive and at most 1024.
We need to define `stack depth`. The Yellow Paper has the `stack pointer` (`SP`) pointing just past the top item on the `data stack`. We define the `stack base` as the element that the `SP` addressed at the entry to the current _basic block_, or `0` on program entry. So we can define the `stack depth` as the number of stack elements between the current `SP` and the current `stack base`.
#### An Algorithm
> This section specifies an algorithm for checking the above the rules. Equivalent code must be run at creation time (as defined in EIP-3540.)
The following is a pseudo-Go implementation of an algorithm for enforcing program validity. This algorithm is a symbolic execution of the program that recursively traverses the bytecode, following its control flow and stack use and checking for violations of the rules above. It uses a stack to track the slots that hold `PUSHed` constants, from which it pops the destinations to validate during the analysis.
This algorithm runs in time equal to `O(vertices + edges)` in the program's control-flow graph, where vertices represent control-flow instructions and the edges represent basic blocks – thus the algorithm takes time proportional to the size of the bytecode.
For simplicity's sake we assume a few helper functions.
*`advance_pc()` advances the `PC`, skipping any immediate data.
*`imm_data()` returns immediate data for an instruction.
*`valid_jumpdest()` tests whether a destination is a JUMPDEST byte and not in immediate data.
*`add_items()` and `remove_items()` push or pop the `const_stack` items for an instruction,
and return its effect on the `stack pointer`.
`add_items()` will `PUSH` the value of constants – all other stack items are zeroed.
```
var bytecode [code_len]byte
var stack_depth [code_len]unsigned
var const_stack[1024]unsigned
var SP := 0
func validate(PC :=0, stack_depth:=0) boolean {
// valid instructions only
instruction := bytecode[PC]
if !valid_instruction(instruction) {
return false;
}
// if stack depth for `PC` is non-zero we have been here before
// return true to break cycle in control flow graph
if stack_depth[PC] != 0 {
return true
}
stack_depth[PC] = stack_depth
entrySP := SP
if instruction == JUMP {
// check for valid destination
dest = stack[SP]
if valid!_jumpdest(dest) {
return false
}
// reset PC to destination of jump
PC += jumpdest
--SP
continue
}
if instruction == JUMPI {
// check for valid destination
jumpdest = stack[SP]
if bytecode[jumpdest] != JUMPDEST {
return false
}
// reset PC to destination of jump
PC += jumpdest
// check for stack underflow and
// recurse to jump to code to validate
stack_depth := SP - entry_SP
if stack_depth <0{
return false
}
--SP
if !validate(stack[SP]), stack_depth {
return false
}
continue
}
// check effect of instruction on stack
SP -= remove_items(instruction)
SP += add_items(instruction)
if SP <0||1024<SP{
return false
}
// successful validation of path
if PC > code_len
|| instruction == STOP
|| instruction == RETURN
|| instruction == SUICIDE {
return true
}
// advance PC according to instruction
PC = advance_pc(PC, instruction)
}
```
## Rationale
The alternative to checking validity at creation time is checking it at runtime. This hurts performance and is a DoS vulnerability. Thus the above rules and accompanying one-pass validation algorithm.
_Rule 1_ – requiring constant destinations for `JUMP` and `JUMPI`– forbids dynamic jumps. Jump destinations are currently checked at runtime, but static jumps can be validated at creation time.
_Rule 2_ – requiring positive stack depth on block exit – ensures that basic_blocks always have sufficient stack on entry. Exceptions can be caused by irreducible paths like jumping into loops and subroutines, and by calling subroutines with insufficient numbers of arguments.
_Rule 3_ – bounding the `stack pointer`– catches all stack overflows that occur without recursion.
Taken together, these rules allow for code to be validated by traversing the control-flow graph, following each edge only once.
## Backwards Compatibility
These changes affect the semantics of existing EVM code – dynamic use of JUMP and JUMPI is deprecated and stack usage is restricted.
## Security Considerations
This EIP is intended to ensure a minimal level of safety for EVM code deployed on the blockchain.
## Copyright
Copyright and related rights waived via [CC0](https://creativecommons.org/publicdomain/zero/1.0/).
