Valid contracts will not halt with an exception unless they either run out of gas, attempt to dynamically jump to an unvalidated destination, or overflow stack during a recursive subroutine call.
Code must validated at contract creation time – not runtime – by the provided algorithm or its equivalent. Therefore, valid jump destinations for dynamic jumps are specified in an EOF container section. This allows for a one-pass algorithm that is (and must be) linear in the size of the _code_, so as not to be a DoS vulnerability.
Dynamic jumps, where the destination of a JUMP or JUMPI is not known until runtime, can be an obstacle to statically proving this sort of safety, but have also been seen as necessary to implement the return jump from a subroutine. But consider this example of calling a minimal subroutine
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.
Still, providing for the safe use of dynamic jumps makes for concise and efficient implementations of language constructs like switches and virtual functions.
Dynamic jumps can be an obstacle to linear-time validation of EVM bytecode. But even where jumps are dynamic it is possible to tabulate valid destinations in advance, and the Ethereum Object Format gives us a place to store such tables. So again, we can validate their safety with a static analysis of the code, and we should.
We need [EIP-3540: EVM Object Format (EOF)](./eip-3540.md) to support container sections.
### EOF container changes
1. A new EOF section called `jumptable` (`section_kind = 3`) is introduced. It contains a sequence of *n* tuples *(jumpsrc, jumpdest<sub>i</sub>*, sorted in ascending lexicographic order. Each tuple represents a valid jump from one location in the bytecode to another.
2. The `jumpsrc` and `jumpdest` values are encoded as 3-byte, MSB-first, unsigned integers.
_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.
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.
We need to define `matching tuple`. A tuple matches a `jmpsrc` to a `jumpdest` if the first element of the tuple is the offset of a `JUMP` or `JUMPI` opcode in the bytecode, and the second element is the address of a `JUMPDEST` opcode in the bytecode.
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`.
> 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.
The alternative to checking validity at creation time is checking it at runtime. This hurts performance and is a denial of service vulnerability. Thus the above rules and accompanying one-pass validation algorithm.
_Rule 1_ – requiring static or previously tabulated destinations for `JUMP` and `JUMPI`– simplifies static jumps and constrains dynamic jumps.
* Jump destinations are currently checked at runtime, but static jumps can be validated at creation time.
* Requiring the possible destinations of dynamic jumps to be tabulated in advance allows for tractable bytecode traversal for creation-time validation: a jump table takes up space proportional to the number of jump destinations, so attempting to attack the validation algorithm with large numbers of jump destinations will also reduce the available space for _code_ to be validated.
_Rule 2_ – requiring positive, consistent stack depth – ensures sufficient stack. Exceptions can be caused by irreducible paths like jumping into loops and subroutines, and by calling subroutines with insufficient numbers of arguments.
These changes affect the semantics of existing EVM code – the use of JUMP, JUMPI, and the stack are restricted, such that some existing _code_ that run correctly will nonetheless become invalid EOF _code_ sections.
