From b4c29a86da7c376495d618cbb47b289096046712 Mon Sep 17 00:00:00 2001 From: Greg Colvin Date: Sat, 4 Sep 2021 02:56:08 -0400 Subject: [PATCH] Update eip-3779.md (#3797) --- EIPS/eip-3779.md | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/EIPS/eip-3779.md b/EIPS/eip-3779.md index 9a9263c5..be4851f1 100644 --- a/EIPS/eip-3779.md +++ b/EIPS/eip-3779.md @@ -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