Update eip-3779.md (#3797)

This commit is contained in:
Greg Colvin 2021-09-04 02:56:08 -04:00 committed by GitHub
parent e154ca74b2
commit b4c29a86da
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23

View File

@ -19,9 +19,9 @@ This EIP specifies validation rules for some important safety properties, includ
* no stack underflows, and
* no stack overflows without recursion.
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.
Valid contracts will not halt with an exception unless they either run out of gas, make an unvalidated dynamic jump, 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.
Code must be validated at contract creation time not runtime by the provided algorithm or its equivalent. Therefore, a table of valid dynamic jumps is 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_ plus the _section_, so as not to be a DoS vulnerability.
## Motivation
@ -51,11 +51,11 @@ ADDITION:
```
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 many of 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.
Since many of the jumps we need in practice are static we can validate their safety with a static analysis of the _code_. And since can, so we should.
Still, providing for the safe use of dynamic jumps makes for concise and efficient implementations of language constructs like switches and virtual functions.
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.
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.
So again, we can validate safety of tabulated dynamic jumps with a static analysis of the code, so we should.
## Specification
@ -72,7 +72,8 @@ We need [EIP-3540: EVM Object Format (EOF)](./eip-3540.md) to support container
We define safety here as avoiding exceptional halting states:
* Valid contracts will not halt with an exception unless they
* run out of gas or
* run out of gas,
* make an unvalidated dynamic jump
* overflow stack while making a recursive subroutine call.
Attempts to create contracts that cannot be proven to be valid will fail.
@ -93,7 +94,7 @@ We would like to consider EVM _code_ valid iff no execution of the program can l
> This section extends the contact creation validation rules (as defined in EIP-3540.)
0. All instructions are valid.
1. Every JUMP and JUMPI address a valid JUMPDEST,
* either static or matching a tuple in the `jumptable`.
* either static or matching a tuple in the jumptable.
2. The stack depth is
* always positive and
* the same on every path through a bytecode.
@ -142,13 +143,8 @@ func validate(PC :=0, stack_depth:=0) boolean {
// if stack depth for `PC` is non-zero we have been here before
// so return to break cycle in control flow graph
if stack_depth[PC] != 0 {
if stack_depth[PC] == stack_depth
return true
else
return false
return true
}
stack_depth[PC] = stack_depth
if instruction == JUMP {
// check for valid destination
@ -165,6 +161,11 @@ func validate(PC :=0, stack_depth:=0) boolean {
}
if instruction == JUMPI {
if stack_depth[PC] != stack_depth
return false
}
stack_depth[PC] = stack_depth
// check for valid destination
jumpdest = stack[SP]
if !valid_jumpdest(dest) {
@ -224,7 +225,7 @@ Taken together, these rules allow for code to be validated by traversing the con
## Backwards Compatibility
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.
These changes affect the semantics of existing EVM code the use of JUMP, JUMPI, and the stack are restricted, such that some _code_ that would run correctly will nonetheless invalid EVM _code_.
## Security Considerations