forked from DecentralizedClimateFoundation/DCIPs
414 lines
16 KiB
Markdown
414 lines
16 KiB
Markdown
---
|
||
eip: 3779
|
||
title: Safer Control Flow for the EVM
|
||
description: Ensure an essential level of safety for EVM code.
|
||
author: Greg Colvin (@gcolvin), Greg Colvin <greg@colvin.org>, Brooklyn Zelenka (@expede)
|
||
discussions-to: https://ethereum-magicians.org/t/eip-3779-safe-control-flow-for-the-evm/6975
|
||
status: Withdrawn
|
||
type: Standards Track
|
||
category: Core
|
||
created: 2021-08-30
|
||
withdrawal-reason: material moved to EIP-2315
|
||
---
|
||
|
||
## Abstract
|
||
|
||
We define a safe EVM contract as one that cannot encounter an exceptional halting state. In general, we cannot prove safety for Turing-complete programs. But we can prove a useful subset.
|
||
|
||
This EIP specifies validity rules to ensure that:
|
||
> Valid contracts will not halt with an exception unless they either
|
||
> * throw `out of gas` or
|
||
> * recursively overflow stack.
|
||
|
||
This EIP does not introduce any new opcodes. Rather, it restricts the use of existing and proposed control-flow instructions. The restrictions must be validated at contract initialization time – not at runtime – by the provided algorithm or its equivalent. This algorithm must take time and space near-linear in the size of the contract, so as not to be a denial of service vulnerability.
|
||
|
||
This specification is entirely semantic. It imposes no further syntax on bytecode, as none is required to ensure the specified level of safety. Ethereum Virtual Machine bytecode is just that -- a sequence of bytes that when executed causes a sequence of changes to the machine state. The safety we seek here is simply to not, as it were, jam up the gears.
|
||
|
||
## Motivation
|
||
|
||
### Safety
|
||
|
||
For our purposes we define a safe EVM contract as one that cannot encounter an exceptional halting state. From the standpoint of security it would be best if unsafe contracts were never placed on the blockchain. Unsafe code can attempt to overflow stack, underflow stack, execute invalid instructions, and jump to invalid locations.
|
||
|
||
Unsafe contracts are exploits waiting to happen.
|
||
|
||
Validating contract safety requires traversing the contract code. So in order to prevent denial of service attacks all jumps, including the existing `JUMP` and `JUMPI`, and also the other proposed jumps -- `RJUMP`, `RJUMPI`, `RJUMPSUB` and `RETURNSUB` -- must be validated at initialization time, and in time and space linear in the size of the code.
|
||
|
||
#### Static Jumps and Subroutines
|
||
|
||
The relative jumps of [EIP-4200](./eip-4200) and the simple subroutines of [EIP-2315](./eip-2315) provide a complete set of static control flow instructions:
|
||
> `RJUMP` _offset_
|
||
* Jumps to _IP+offset_.
|
||
> `RJUMPI` _offset_
|
||
* Jumps if the top of stack is non-zero.
|
||
> `RJUMPSUB` offset
|
||
* Pushes _IP+1_ on the return stack and jumps to _IP+offest_.
|
||
> `RETURNSUB`
|
||
* Jumps to the address popped off the return stack.
|
||
|
||
Note that each jump creates at most two paths of control through the code, such that the complexity of traversing the entire control-flow graph is linear in the size of the code.
|
||
|
||
#### *Dynamic Jumps*
|
||
|
||
Dynamic jumps, where the destination of a `JUMP` or `JUMPI` is not known until runtime, are an obstacle to proving validity in linear time -- any jump can be to any destination in the code, potentially requiring time quadratic in the size of code. For this reason we have two real choices.
|
||
|
||
1. Deprecate dynamic jumps. This is easily done:
|
||
|
||
> Define `JUMP` and `JUMPI` as `INVALID` for the purposes of EOF Code Validation
|
||
|
||
2. Constrain dynamic jumps. This requires static analysis.
|
||
|
||
Consider the simplest and most common case.
|
||
```
|
||
PUSH address
|
||
JUMP
|
||
```
|
||
This is effectively a static jump.
|
||
|
||
Another important use of `JUMP` is to implement the return jump from a subroutine. So consider this example of calling and returning from a minimal subroutine:
|
||
```
|
||
TEST_SQUARE:
|
||
jumpdest
|
||
push RTN_SQUARE
|
||
0x02
|
||
push SQUARE
|
||
jump
|
||
RTN_SQUARE
|
||
jumpdest
|
||
swap1
|
||
jump
|
||
|
||
SQUARE:
|
||
jumpdest
|
||
dup1
|
||
mul
|
||
swap1
|
||
jump
|
||
```
|
||
The return address -`RTN_SQUARE` - and the destination address - `SQUARE` - are pushed on the stack as constants and remain unchanged as they move on the stack, such that only those constants are passed to each `JUMP`. They are effectively static. We can track the motion of constants on the `data stack` at validation time, so *we do not need unconstrained dynamic jumps to implement subroutines.*
|
||
|
||
*The above is the simplest analysis that suffices. A more powerful analysis that takes in more use cases is possible -- slower, but still linear-time.*
|
||
|
||
#### Validation
|
||
|
||
We can validate the safety of contracts with a static analysis that takes time and space linear in the size of the *code*, as shown below. And since we can, we should.
|
||
|
||
### Performance
|
||
|
||
Validating safe control flow at initialization time has potential performance advantages.
|
||
* Static jumps do not need to be checked at runtime.
|
||
* Stack underflow does not need to be checked for at runtime.
|
||
|
||
## Specification
|
||
|
||
### Validity
|
||
|
||
> In theory, theory and practice are the same. In practice, they're not. -- Albert Einstein
|
||
|
||
We define a _safe_ EVM contract as one that cannot encounter an exceptional halting state. We validate _safety_ at initialization time to the extent practical.
|
||
|
||
#### *Exceptional Halting States*
|
||
|
||
The *execution* of each instruction is defined in the Yellow Paper as a change to the EVM state that preserves the invariants of EVM state. At runtime, if the execution of an instruction would violate an invariant the EVM is in an exceptional halting state. The Yellow Paper defined five such states.
|
||
1. Insufficient gas
|
||
2. More than 1024 stack items
|
||
3. Insufficient stack items
|
||
4. Invalid jump destination
|
||
5. Invalid instruction
|
||
|
||
*A program is safe iff no execution can lead to an exceptional halting state.*
|
||
|
||
*We would like to consider EVM programs valid iff they are safe.*
|
||
|
||
*In practice*, we must be able to validate *code* in linear time to avoid denial of service attacks. And we must support dynamically-priced instructions, loops, and recursion, which can use arbitrary amounts of gas and stack.
|
||
|
||
Thus our validation cannot consider concrete computations -- it only performs a limited symbolic execution of the _code_. This means we will reject programs if we detect any invalid execution paths, even if those paths are not reachable at runtime. And we will count as valid programs that may not always produce correct results.
|
||
|
||
We can detect only _non-recursive_ stack overflows at *validation time*, so we must check for the first two states at _runtime_:
|
||
* `out of gas` and
|
||
* stack overflow.
|
||
|
||
The remaining three states we can check at *validation time*:
|
||
* stack underflow,
|
||
* invalid jump, and
|
||
* invalid instruction.
|
||
|
||
That is to say:
|
||
> Valid contracts will not halt with an exception unless they either
|
||
> * throw `out of gas` or
|
||
> * recursively overflow stack.
|
||
|
||
#### *Constraints on Valid Code*
|
||
|
||
* Every instruction is valid.
|
||
* Every jump is valid:
|
||
* Every`JUMP` and `JUMPI` is *static*.
|
||
* No `JUMP`, `JUMPI`, `RJUMP`, `RJUMPI`, or `RJUMPSUB` addresses immediate data.
|
||
* The stacks are always valid:
|
||
* The _number_ of items on the `data stack` is always positive, and at most 1024.
|
||
* The _number_ of items on the `return stack` is always positive, and at most 1024.
|
||
* The data stack is consistently aligned:
|
||
* The _number_ of items on the `data stack` between the current `stack pointer` and the `stack pointer` on entry to the most recent basic block is the same for each _execution_ of a _byte_code_.
|
||
|
||
We define a `JUMP` or `JUMPI` instruction to be *static* if its `jumpsrc` argument was first placed on the stack via a `PUSH…` and that value has not changed since, though it may have been copied via a `DUP…` or `SWAP…`.
|
||
|
||
The `RJUMP`, `RJUMPI` and `RJUMPSUB`instructions take their destination as an immediate argument, so they are *static*.
|
||
|
||
Taken together, these rules allow for code to be validated by traversing the control-flow graph, in time and space linear in the size of the code, following each edge only once.
|
||
|
||
_Note: The definition of 'static' for `JUMP` and `JUMPI` is the bare minimum needed to implement subroutines. Deeper analyses could be proposed that would validate a larger and probably more useful set of jumps, at the cost of more expensive (but still linear) validation._
|
||
|
||
|
||
## Rationale
|
||
|
||
Demanding *static* destinations for all jumps means that all jump destinations can be validated at initialization time, not runtime.
|
||
|
||
Bounding the stack pointers catches all `data stack` and non-recursive`return stack` overflows.
|
||
|
||
Requiring a consistently aligned`data stack` prevents stack underflow. It can also catch such errors as misaligned stacks due to irreducible control flows and calls to subroutines with the wrong number of arguments.
|
||
|
||
## Backwards Compatibility
|
||
|
||
These changes affect the semantics of EVM code – the use of `JUMP`, `JUMPI`, and the stack are restricted, such that some *code* that would otherwise run correctly will nonetheless be invalid EVM *code*.
|
||
|
||
## Reference Implementation
|
||
|
||
The following is a pseudo-Go implementation of an algorithm for predicating code validity. An equivalent algorithm must be run at initialization time.
|
||
|
||
This algorithm performs a symbolic execution of the program that recursively traverses the _code_, emulating its control flow and stack use and checking for violations of the rules above.
|
||
|
||
It runs in time equal to `O(vertices + edges)` in the program's control-flow graph, where edges represent control flow and the vertices represent _basic blocks_ -- thus the algorithm takes time proportional to the size of the _code_.
|
||
|
||
_Note: All valid code has a control-flow graph that can be traversed in time and space linear in the length of the code. That means that some other static analyses and code transformations that might otherwise require quadratic time can also be written to run in near-linear time, including one-pass and streaming compilers._
|
||
|
||
### Validation Function
|
||
|
||
***Note:** This function is a work in progress, and the version below is known to be incorrect.*
|
||
|
||
For simplicity's sake we assume that _jumpdest analysis_ has been done and that we have some helper functions.
|
||
* `isValidInstruction(pc)` returns true if `pc` points at a valid instruction
|
||
* `isValidJumpdest(dest)` returns true if `dest` is a valid jumpdest
|
||
* `immediateData(pc)` returns the immediate data for the instruction at `pc`.
|
||
* `advancePC(pc)` returns next `pc`, skipping any immediate data.
|
||
* `removed_items(pc)` returns the number of items removed from the `dataStack` by the instruction at `pc`.
|
||
* `added_items(pc)` returns the number of items added to the `dataStack` by the instruction at `pc`.
|
||
|
||
```
|
||
var bytecode [codeLen]byte
|
||
var subMin [codeLen]int
|
||
var subMax [codeLen]int
|
||
var subDelta [codeLen]int
|
||
var visited [codeLen]bool
|
||
var dataStack [1024]int
|
||
|
||
// validate a path through the control flow of the bytecode at pc
|
||
// and return the maximum number of stack items used down that path
|
||
// or else the PC and an error
|
||
//
|
||
// by starting at pc:=0 the entire program is recursively evaluated
|
||
//
|
||
func validate(pc := 0, sp := 0, rp := 0) int, error {
|
||
minStack := 0
|
||
maxStack := 0
|
||
deltaStack := 0
|
||
for pc < codeLen {
|
||
if !isValidInstruction(pc) {
|
||
return 0,0,0,invalid_instruction
|
||
}
|
||
|
||
// if we have jumped here before return to break cycle
|
||
if visited[pc] {
|
||
|
||
// stack is not aligned if deltas not the same
|
||
if ??? {
|
||
return 0,0,0,invalid_stack
|
||
}
|
||
return minStack, maxStack, sp
|
||
}
|
||
visited[pc] = true
|
||
switch bytecode[pc] {
|
||
|
||
// successful termination
|
||
case STOP:
|
||
return minStack, maxStack, sp
|
||
case RETURN:
|
||
return minStack, maxStack, sp
|
||
|
||
case SELFDESTRUCT:
|
||
return minStack, maxStack, sp
|
||
case REVERT:
|
||
return minStack, maxStack, sp
|
||
case INVALID:
|
||
return 0,0,0,invalid_instruction
|
||
|
||
case RJUMP:
|
||
|
||
// check for valid jump destination
|
||
if !isValidJumpdest(jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
|
||
// reset pc to destination of jump
|
||
pc += immediateData(pc)
|
||
|
||
case RJUMPI:
|
||
|
||
// recurse to validate true side of conditional
|
||
jumpdest = pc + immediateData(pc)
|
||
if !isValidJumpdest(pc + jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
minRight, maxLeft, deltaRight, err =
|
||
validate(jumpdest, sp, rp)
|
||
|
||
err {
|
||
return 0,0,0,err
|
||
}
|
||
|
||
// recurse to validate false side of conditional
|
||
pc = advancePC(pc)
|
||
minRight, maxRight, deltaRight, err =
|
||
validate(pc, sp, rp)
|
||
if err {
|
||
return 0,0,0,err
|
||
}
|
||
|
||
// both paths valid, so return max
|
||
minStack = min(minStack, min(minLeft, minRight))
|
||
maxStack += max(maxLeft, maxRight)
|
||
deltaStack += max(deltaLeft, deltaRight)
|
||
return minStack, maxStack, deltaStack
|
||
|
||
case RJUMPSUB:
|
||
|
||
// check for valid jump destination
|
||
jumpdest = immediateData(pc)
|
||
if !isValidJumpdest(pc + jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
|
||
pc += jumpdest
|
||
|
||
// recurse to validate subroutine call
|
||
minSub, maxSub, deltaSub, err = validate(jumpdest, sp, rp)
|
||
if err {
|
||
return 0,0,0,err
|
||
}
|
||
subMin[pc] = minSub
|
||
subMax[pc] = maxSub
|
||
subDelta[pc] = deltaSub
|
||
minStack = min(minStack, sp)
|
||
maxStack = max(maxStack, sp)
|
||
pc = advancePC(pc)
|
||
|
||
case RETURNSUB:
|
||
|
||
maxStack = max(maxStack, sp)
|
||
return minStack, maxStack, sp, nil
|
||
|
||
/////////////////////////////////////////////////////
|
||
//
|
||
// The following are to be included only if we take
|
||
//
|
||
// Option 2
|
||
//
|
||
// and do not deprecate JUMP and JUMPI
|
||
//
|
||
case JUMP:
|
||
// pop jump destination
|
||
jumpdest = dataStack[--sp]
|
||
if !valid_jumpdest(jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
pc = jumpdest
|
||
case JUMPI:
|
||
// pop jump destination and conditional
|
||
jumpdest = dataStack[--sp]
|
||
jumpif = dataStack[--sp]
|
||
if sp < 0 {}
|
||
return 0,0,0,stack_underflow
|
||
}
|
||
if !valid_jumpdest(jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
|
||
// recurse to validate true side of conditional
|
||
if !isValidJumpdest(jumpdest) {
|
||
return 0,0,0,invalid_destination
|
||
}
|
||
maxLeft, err = validate(jumpdest, sp, rp)
|
||
if err {
|
||
return 0,0,0,err
|
||
}
|
||
|
||
// recurse to validate false side of conditional
|
||
pc = advance_pc(pc)
|
||
maxRight, err = validate(pc, sp, rp)
|
||
if err {
|
||
return 0,0,0,err
|
||
}
|
||
|
||
// both sides valid, return max
|
||
maxStack += max(maxLeft, maxRight)
|
||
return minStack, maxStack, sp
|
||
case PUSH1 <= bytecode[pc] && bytecode[pc] <= PUSH32 {
|
||
sp++
|
||
if (sp > 1023) {
|
||
return 0,0,0,stack_overflow
|
||
}
|
||
maxStack = max(maxStack, sp)
|
||
dataStack[sp] = immediateData(pc)
|
||
pc = advancePC(pc)
|
||
case DUP1 <= bytecode[pc] && bytecode[pc] <= DUP32 {
|
||
dup = sp - (bytecode[pc] - DUP1)
|
||
if dup < 0 {
|
||
return 0,0,0,stack_underflow
|
||
}
|
||
sp++
|
||
if (sp > 1023) {
|
||
return 0,0,0,stack_overflow
|
||
}
|
||
maxStack = max(maxStack, sp)
|
||
dataStack[sp] = dataStack[dup]
|
||
pc = advancePC(pc)
|
||
case SWAP1 <= bytecode[pc] && bytecode[pc] <= SWAP32 {
|
||
swap = sp - (bytecode[pc] - SWAP1)
|
||
if swap < 0 {
|
||
return 0,0,0,stack_underflow
|
||
}
|
||
temp := dataStack[swap]
|
||
dataStack[swap] = dataStack[0]
|
||
dataStack[0] = temp
|
||
pc = advancePC(pc)
|
||
//
|
||
/////////////////////////////////////////////////////
|
||
|
||
default:
|
||
|
||
// apply other instructions to stack pointer
|
||
sp -= removed_items(pc)
|
||
if (sp < 0) {
|
||
return 0,0,0,stack_underflow
|
||
}
|
||
minStack = min(minStack, sp)
|
||
sp += added_items(pc)
|
||
if (sp > 1023) {
|
||
return 0,0,0,stack_overflow
|
||
}
|
||
maxStack = max(maxStack, sp)
|
||
pc = advancePC(pc)
|
||
}
|
||
}
|
||
|
||
// successful termination
|
||
return minStack, maxStack, sp
|
||
}
|
||
```
|
||
## Security Considerations
|
||
|
||
This EIP is intended to ensure an essential level of safety for EVM code deployed on the blockchain.
|
||
|
||
## Copyright
|
||
Copyright and related rights waived via [CC0](../LICENSE.md).
|
||
|