⚠️ This EIP is not recommended for general use or implementation as it is likely to change.

EIP-5450: EOF - Stack Validation Source

Deploy-time validation of stack usage for EOF functions.

AuthorAndrei Maiboroda, Paweł Bylica, Alex Beregszaszi
Discussions-Tohttps://ethereum-magicians.org/t/eip-5450-eof-stack-validation/10410
StatusDraft
TypeStandards Track
CategoryCore
Created2022-08-12
Requires 3540, 3670, 4200, 4750

Abstract

Introduce extended validation of code sections to guarantee that stack underflow cannot 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, however it may still be possible to exceed that limit in some cases, and thus overflow checks cannot be fully eliminated.

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 types[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 every terminating instruction, except RETF, data stack is empty after executing it.
  5. 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.
  6. Maximum data stack height required by a function does not exceed 1024.

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. See below for reference implementation.

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 check for each executed instruction. However implementations can keep it if they choose to do so.

Stack overflow check, on the other hand, is still required at run-time, because function execution can start at arbitrary (i.e. known only at run-time) stack height at CALLF instruction of a caller (i.e. each execution can be in arbitrary inner call frame). Verification algorithm examines only stack height changes relative to starting stack height of the function.

Rationale

Stack overflow check only in CALLF

In the current proposal stack overflow checks are unchanged (i.e. are done for every instruction). However, we can provide more efficient variant where stack overflow check is performed only in CALLF instruction and uses called function’s max_stack_height information for this. This decreases flexibility of an EVM program because max_stack_height corresponds to the worst-case control-flow path in the function. Moreover, the max_stack_height computed during validation must be stored alongside the code. This can be in the EOF itself or in implementation-defined format.

Unreachable code

The current validation algorithm ignores unreachable instructions. The algorithm can be extended to reject any code having any unreachable instructions but additional instructions traversal is needed (or more efficient algorithm must be developed).

Clean stack upon termination

It is currently required that the EVM stack is empty (in the current function context) after any terminating instruction (STOP, RETURN, etc, but also RETF). This requirement can be lifted.

This can be used for implementing more efficient early exits from a function (e.g. assertion failure).

For “exit” instructions which terminates the whole program execution (STOP, RETURN, etc) this is no change comparing to pre-EOF EVM. I.e. some garbage can be left on the stack. Cleaning the stack does not improve EVM implementation performance but makes the EVM programs potentially cost more (compiler is required to insert additional POP instructions).

For RETF semantic would be more complicated. For n function outputs and s the stack height at RETF the EVM must erase s-n non-top stack items and move the n stack items to the place of erased ones. Cost of such operation may be relatively cheap but is not constant.

Backwards Compatibility

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

Reference Implementation

# Returns maximum stack height required by function execution frame
# (not including frames of internal calls)
# Raises ValidateExceptin if code is invalid.
def validate_function(func_id: int, code: bytes, types: list[FunctionType] = [FunctionType(0, 0)]) -> int:
    assert func_id >= 0
    assert types[func_id].inputs >= 0
    assert types[func_id].outputs >= 0

    validate_code_section(code, len(types))

    stack_heights = {}
    start_stack_height = types[func_id].inputs
    max_stack_height = start_stack_height

    # queue of instructions to analyze, list of (pos, stack_height) pairs
    worklist = [(0, start_stack_height)]

    while worklist:
        pos, stack_height = worklist.pop(0)
        while True:
            # Assuming code ends with a terminating instruction due to previous validation in validate_code_section()
            assert pos < len(code), "code is invalid" 
            op = code[pos]
            info = TABLE[op]

            # Check if stack height (type arity) at given position is the same
            # for all control flow paths reaching this position.
            if pos in stack_heights:
                if stack_height != stack_heights[pos]:
                    raise ValidationException("stack height mismatch for different paths")
                else:
                    break
            else:
                stack_heights[pos] = stack_height


            stack_height_required = info.stack_height_required
            stack_height_change = info.stack_height_change

            if op == OP_CALLF:
                called_func_id = int.from_bytes(code[pos + 1:pos + 3], byteorder="big", signed=False)
                # Assuming called_func_id is valid due to previous validation in validate_code_section()
                stack_height_required += types[called_func_id].inputs
                stack_height_change += types[called_func_id].outputs - types[called_func_id].inputs

            # Detect stack underflow
            if stack_height < stack_height_required:
                raise ValidationException("stack underflow")

            stack_height += stack_height_change
            max_stack_height = max(max_stack_height, stack_height)

            # Handle jumps
            if op == OP_RJUMP:
                offset = int.from_bytes(code[pos + 1:pos + 3], byteorder="big", signed=True)
                pos += info.immediate_size + 1 + offset  # pos is valid for validated code.

            elif op == OP_RJUMPI:
                offset = int.from_bytes(code[pos + 1:pos + 3], byteorder="big", signed=True)
                # Save True branch for later and continue to False branch.
                worklist.append((pos + 3 + offset, stack_height))
                pos += info.immediate_size + 1

            elif info.is_terminating:
                expected_height = types[func_id].outputs if op == OP_RETF else 0
                if stack_height != expected_height:
                    raise ValidationException("non-empty stack on terminating instruction")
                break

            else:
                pos += info.immediate_size + 1


    if max_stack_height > 1024:
        raise ValidationException("max stack above limit")

    return max_stack_height

Security Considerations

Needs discussion.

Copyright and related rights waived via CC0.

Citation

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.