EIP-5450: EOF - Stack Validation

Deploy-time validation of stack usage for EOF functions.

作者	Andrei Maiboroda, Paweł Bylica, Alex Beregszaszi
讨论-To	https://ethereum-magicians.org/t/eip-5450-eof-stack-validation/10410
状态	Review
类型	Standards Track
分类	Core
创建日期	2022-08-12
依赖	3540, 3670, 4200, 4750
英文版	https://eips.ethereum.org/EIPS/eip-5450

Abstract

Introduce extended validation of code sections to guarantee that neither stack underflow nor overflow can happen during execution of validated contracts.

Motivation

Currently existing EVM implementations perform a number of validity checks for each executed instruction, such as check for stack overflow/underflow, sufficient gas, etc. This change aims to minimize the number of such checks required at run-time, by verifying at deploy-time that no exceptional conditions can happen, and preventing to deploy the code where it could happen.

In particular, this extended code validation eliminates the need for EVM stack underflow checks done for every executed instruction. It also prevents deploying code that can be statically proven to require more than 1024 stack items and limits stack overflow checks to the CALLF instruction only.

Specification

Code validation

Remark: We rely on the notions of data stack and type section as defined by EIP-4750.

Code section validation rules as defined by EIP-3670 (which has been extended by EIP-4200 and EIP-4750) are extended again to include the instruction flow traversal procedure, where every possible code path is examined, and data stack height at each instruction is recorded.

Data stack height here refers to the number of stack values accessible by this function, i.e. it does not take into account values of caller functions’ frames (but does include this function’s inputs). Note that validation procedure does not require actual data stack implementation, but only to keep track of its height. Current height value starts at type[code_section_index].inputs (number of inputs of this function) at function entry and is updated at each instruction.

At the same time the following properties are being verified:

1. For each reachable instruction in the section, data stack height is the same for all possible code paths going through this instruction.
2. For each instruction, data stack always has enough items, i.e. stack underflow is invalid.
3. For CALLF instruction, data stack has enough items to use as input arguments to a called function according to its type defined in the type section.
4. For RETF instruction, data stack before executing it has exactly n items to use as output values returned from a function, where n is function’s number of outputs according to its type defined in the type section.
5. max_stack_height does not exceed 1023.
6. The maximum data stack height matches the corresponding code section’s max_stack_height within the type section body.
7. No unreachable instructions exist in the code section.

To examine every reachable code path, validation needs to traverse every instruction in order, while also following each non-conditional jump, and following both possible branches for each conditional jump. After completing this, verify each instruction was visited at least once. Fail if any instructions were not visited as this invalidates 7).

The complexity of this traversal is linear in the number of instructions, because each code path is examined only once, and property 1 guarantees no loops in the validation.

Execution

Given new deploy-time guarantees, EVM implementation is not required anymore to have run-time stack underflow nor overflow checks for each executed instruction. The exception is the CALLF performing data stack overflow check for the entire called function.

Rationale

Stack overflow check only in CALLF

In this EIP, we provide a more efficient variant of the EVM where stack overflow check is performed only in CALLF instruction using the called function’s max_stack_height information. This decreases flexibility of an EVM program because max_stack_height corresponds to the worst-case control-flow path in the function.

向后兼容性

This change requires a “network upgrade”, since it modifies consensus rules.

It poses no risk to backwards compatibility, as it is introduced only for EOF1 contracts, for which deploying undefined instructions is not allowed, therefore there are no existing contracts using these instructions. The new instructions are not introduced for legacy bytecode (code which is not EOF formatted).

Security Considerations

Needs discussion.

Copyright

Copyright and related rights waived via CC0.

参考文献

Please cite this document as:

Andrei Maiboroda, Paweł Bylica, Alex Beregszaszi, "EIP-5450: EOF - Stack Validation [DRAFT]," Ethereum Improvement Proposals, no. 5450, August 2022. [Online serial]. Available: https://eips.ethereum.org/EIPS/eip-5450.