EIPs

EIP3779 - Safer Control Flow for the EVM

# 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 that 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 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, JUMPI and the other proposed jumps -- RJUMP, RJUMPI, RJUMPV, RJUMPSUB and RETURNSUB -- must be validated at initialization time, and in time and space linear in the size of the code

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. We use a linear-time, linear-space symbolic execution of the code to treat some of them as static, and treat the rest as invalid.

# Dynamic Jumps, Static Jumps, and Subroutines

Dynamic jumps need not always impede control-flow analysis. In the simplest and most common case

PUSH address
JUMP
1
2

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
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

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 do not need unconstrained dynamic jumps to implement subroutines.

Even where jumps are dynamic it is possible to statically constrain their range by enumerating valid destinations in advance, as per the proposed RJUMPV instruction.

Finally, the static relative jumps of EIP-4200 and the simple subroutines of EIP-2315 provide static jumps directly.

So 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

We validate safety at instialisazion time. We define a safe EVM contract as one that cannot encounter an exceptional halting state.

# Exceptional Halting States

The execution of each instruction is defined in the Yellow Paper (opens new window) 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 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 programs valid iff no execution of the code can lead to an exceptional halting state.

However, 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.

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 do not in fact produce correct results. So in theory, theory and practice are the same. But in practice, they're not.

We can detect only non-recursive stack overflows at validation time, so at runtime we must check for the first two states:

  • out of gas and
  • stack overflow.

At validation time we can detect the remaining three states:

  • stack underflow,
  • invalid jump, and
  • invalid instruction.

That is to say (again):

Valid code cannot halt with an exception unless it either

  • throws out of gas or
  • recursively overflows stack.

# Constraints on Valid Code

  • Every instruction is valid.
  • Every jump is valid:
    • EveryJUMP and JUMPI is static.
    • No JUMP, JUMPI, RJUMP, RJUMPI, RJUMPV, 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 available:
    • The available items on the data stack are always positive, and the same for every execution of an instruction.

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 RJUMPSUBinstructions take a jumpdst as an immediate argument, so they are static. The RJUMPV instructions take an index on the stack at runtime, and proceeds via the jumpdest indexed in the jump vector, or else via its first, default jumpdest. In this way RJUMPV is constrained to be static, as the programmer must provide a default case, and all cases are validated.

The Yellow Paper has the stack pointer (SP) pointing just past the top item on the data stack. We define the available items as the number of stack items between the current SP and the SP on entry to the most recent basic block.

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.

# 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-recursivereturn stack overflows.

Requiring consistently available stack items 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.

And relative rather than absolute jump destinations are consistent with the other RJUMP instructions, so that code remains position-independent.

Note: The definition of static here is the bare minimum needed to implement subroutines. Constants can be propagated to validate a larger and probably more useful set of jumps, at the cost of more expensive (but still linear) validation.

Note: Requiring the valid destinations of dynamic jumps to be enumerated at every jump instruction allows for tractable bytecode validation: a jump vector takes up space proportional to the number of destinations, so attempting to attack the validation algorithm with large numbers of jumps will also reduce the available space for jumps to be validated.

# Reference Implementation

This section specifies an algorithm for validating EVM contracts. An equivalent algorithm must be run at initialization time.

It 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.

This algorithm 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: Because valid code has a control-flow graph that can be traversed in linear time there are other programs that might otherwise require quadratic time that can also be written to run in linear time, including compilers.

# Validation Algorithm

The following is a pseudo-Go implementation of an algorithm for predicating code validity. It uses an auxiliary stacks to track constant stack slots, and from which to pop the JUMP and JUMPI destinations to validate during analysis.

For simplicity's sake we assume that jumpdest analysis has been done and that we have a few helper functions.

  • is_valid_instruction(pc) returns true if pc points at valid instruction
  • is_immediate_data(pc) returns true if pc points at immediate data
  • immediate_data(pc) returns the immediate data for an instruction.
  • advance_pc() advances the pc, skipping any immediate data.
  • removed_items(pc)returns the number of items removed from the data_stack by an instruction.
  • added_items(pc) returns the number of items added to the data_stack by an instruction.
var code        [code_len]byte
var avail_items [code_len]int
var return_stack[1024]int = { -1 }
var data_stack  [1024]uint256 = { INVALID }

// return the maximum stack used or else the PC and an error
func validate(pc := 0, sp := 0, bp := 0, rp := 0) int, error {
   used_items := 0 
   for pc < code_len {
      if !is_valid_instruction(pc) {
         return pc, invalid_instruction
      }
      
      // if available items on stack for `pc` are non-zero
      //    we have been here before
      //    so return to break cycle
      if avail_items[pc] != 0 {

          // invalid if available items not the same
          if avail_items[pc] != sp - bp {
            return pc, invalid_stack
          }
          return used_items, nil

      }
      avail_items[pc] = sp - bp
      if avail_items[pc] < 0 {
         return pc, stack_underflow
      }
      
      switch code[pc] {

      // successful termination
      case STOP:
         return true
      case RETURN:
         return true
      case SUICIDE:
         return true

      // track constants on stack
      case PUSH1 <= code[pc] && code[pc] <= PUSH32 {
         sp++
         if (sp > 1023) {
            return pc, stack_overflow
         }
         data_stack[sp] = immediate_data(pc)
         advance_pc()
         continue
      
      case JUMP:

         // will enter basic block at destination
         bp = sp

         // pop jump destination
         jumpdest = data_stack[--sp]
         if !valid_jumpdest(jumpdest) {
            return false
         }
         continue;
         
      case JUMPI:

         // will enter basic block at destination
         bp = sp

         // pop jump destination and conditional
         jumpdest = data_stack[--sp]
         jumpif = data_stack[--sp]
         if sp < 0 {}
            return pc, stack_underflow
         }
         if !valid_jumpdest(jumpdest) {
            return pc, invalid_destination
         }

         // recurse to validate true side of conditional
         if is_immediate_data(jumpdest) {
            return pc, invalid_destination
         }
         left_used, err = validate(jumpdest, sp, bp, rp)
         if err {
            return pc, err
         }
         
         // recurse to validate false side of conditional
         pc = advance_pc(pc)
         right_used, err = validate(pc, sp, bp, rp)
         if err {
            return pc, err
         }
         
         // both sides valid, check stack and return used_items
         used_items += max(left_used, right_used)
         sp += used_items
         if (sp > 1023) {
            return pc, stack_overflow
         }
         return used_items, nil
    
      case RJUMP:
      
         // will enter basic block at destination
         bp = sp

         // check for valid jump destination
         if is_immediate_data(jumpdest) {
            return pc, invalid_destination
         }
         
         // reset pc to destination of jump
         pc += immediate_data(pc)

      case RJUMPI:
      
         // will enter basic block at destination
         bp = sp

         // recurse to validate true side of conditional
         jumpdest := pc + immediate_data(pc)
         if is_immediate_data(jumpdest) {
            return pc, invalid_destination
         }
         left_used, err = validate(jumpdest, sp, bp, rp)
         if err {
            return pc, err
         }
         
         // recurse to validate false side of conditional
         pc = advance_pc(pc)
         right_used, err = validate(pc, sp, bp, rp)
         if err {
            return pc, err
         }
         
         // both sides valid, check stack and return used_items
         used_items += max(left_used, right_used)
         if (sp += used_items > 1023) {
            return pc, stack_overflow
         }
         return used_items, nil

      case RJUMPSUB:

         // check for valid jump destination
         jumpdest = imm_data(pc)
         if is_immediate_data(pc + jumpdest) {
            return pc, invalid_destination
         }

         // will enter basic block at destination
         bp = sp

         // push return address and reset pc to destination
         return_stack[rp++] = pc + 1
         pc += jumpdest

      case RETURNSUB:
      
         // will enter basic block at destination
         bp = sp

         // check for valid return destination
         pc = return_stack[--rp]
         if !code[pc - 1] == JUMPSUB {
            return pc, invalid_destination

          sp++
          data_stack[sp++] = immediate_data(pc)
          pc = advance_pc(pc)

      default:
         pc = advance_pc(pc)

         // apply other instructions to stack pointer
         // removed and added items are filled with INVALID
         used_items -= removed_items(pc)
         used_items += added_items(pc)
         sp += used_items
         if (sp > 1023) {
            return pc, stack_overflow
         }
      }
   }

   // successful termination
   return used_items, nil
}
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189

# 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.

# Security Considerations

This EIP is intended to ensure an essential level of safety for EVM code deployed on the blockchain.

# References

Greg Colvin, Martin Holst Swende, Brooklyn Zelenka, "EIP-2315: Simple Subroutines for the EVM [DRAFT]," Ethereum Improvement Proposals, no. 2315, October 2019. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-2315.

Alex Beregszaszi, Paweł Bylica, Andrei Maiboroda, "EIP-3540: EVM Object Format (EOF) v1," Ethereum Improvement Proposals, no. 3540, March 2021. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-3540..

Alex Beregszaszi, Andrei Maiboroda, Paweł Bylica, "EIP-3670: EOF - Code Validation," Ethereum Improvement Proposals, no. 3670, June 2021. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-3670.

Alex Beregszaszi, Andrei Maiboroda, Paweł Bylica, "EIP-4200: Static relative jumps [DRAFT]," Ethereum Improvement Proposals, no. 4200, July 2021. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-4200.

Copyright and related rights waived via CC0 (opens new window).

▲ Powered by Vercel