From 90a02dcb31dcf49ae7b6b23355ae05e6a369e438 Mon Sep 17 00:00:00 2001 From: Lucas Date: Thu, 3 Oct 2024 17:21:10 -0300 Subject: [PATCH] Stricter Verification --- proposals/0179-stricter-verification.md | 107 ++++++++++++++++++++++++ 1 file changed, 107 insertions(+) create mode 100644 proposals/0179-stricter-verification.md diff --git a/proposals/0179-stricter-verification.md b/proposals/0179-stricter-verification.md new file mode 100644 index 000000000..97152eeed --- /dev/null +++ b/proposals/0179-stricter-verification.md @@ -0,0 +1,107 @@ +--- +simd: '0179' +title: SBPF Stricter verification constraints +authors: + - Alexander Meißner + - Lucas Steuernagel +category: Standard +type: Core +status: Draft +created: 2024-10-03 +--- + +## Summary + +This SIMD proposes improvements in the verification rules of SBPF programs. +The introduction of the syscall instruction in SIMD-0178 allows for the +differentiation of internal and external calls, opening up for stricter +verification constraints and increased security of deployed programs. + +## Motivation + +The `call` instruction (opcode `0x85`) in SBF, especially when it requires a +relocation, is ambiguous. It does not carry information about whether it is +a system call or an internal call. This ambiguity prevents more rigid +verification constraints that would reject programs jumping to inconvenient +locations, like invalid destinations or the middle of an `lddw` instruction. +The new syscall instruction introduced in SIMD-0178 permits the +differentiation of internal and external calls, so we can introduce new +verification rules to prevent any unwarranted behavior. + +## New Terminology + +None. + +## Detailed Design + +The following must go into effect if and only if a program indicates the SBF +version XX or higher in its ELF header e_flags field, according to the +specification of SIMD-0161. + +### Restrict functions’ last instruction + +Functions must only end with the `ja` (opcode `0x05`) or the exit (opcode +`0x9D` since SIMD-0178) instruction. Allowing calls to be the last instruction +of functions was inconvenient, because when the call returns, and there is no +other instruction to redirect the control flow, we will execute the very next +program counter, resulting in a fallthrough into another function’s code. +Offending this new validation condition must throw an +`VerifierError::InvalidFunction` error. + +### Restrict jump instruction destination + +All jump instructions, except for `call` (opcode `0x85`) and `callx` (opcode +`0x8D`), must now jump to a code location inside their own function. Jumping +to arbitrary locations hinders a precise program verification. +`VerifierError::JumpOutOfCode` must be thrown for offending this rule. + +`call imm` (opcode `0x85`) must only be allowed to jump to a program counter +previously registered as the start of a function. Otherwise +`VerifierError::InvalidFunction` must be thrown. Functions must be known if +they are present in the symbol table or are the target program counter of a +`call imm` instruction. The entrypoint to the program must also define a valid +function. + +### Runtime check for callx + +The jump destination of `callx` (opcode `0x8D`) must be checked during +execution time to match the initial address of a registered function. If this +is not the case, a `EbpfError::UnsupportedInstruction` must be thrown. This +measure is supposed to improve security of programs, disallowing the malicious +use of callx. + +A function is registered according to the rules mentioned in the previous +section: be present in the symbol table or be the target program counter of a +call imm instruction. + +### Limit where a function can start + +Presently, functions may start in any part of the ELF text section, however +this is an encumbrance when it comes to `lddw` (opcode `0x18`) instructions. +As they occupy two instruction slots in an ELF, it is possible for functions +to start between these lddw slots, very likely resulting in undesired +behavior. The verifier must throw an `VerifierError::JumpToMiddleOfLddw` error +when that is the case. + +### Removal of ExecutionOverrun error + +As the jump instructions destinations are now limited to the range of the +function they are located in, and the call instructions can only move the +program counter to a known location, the `EbpfError::ExecutionOverrun` must not +be reachable, so it must be removed. + +## Alternatives Considered + +None. + +## Impact + +The changes proposed in this SIMD are transparent to dApp developers. The +compiler toolchain will emit correct code for the specified SBF version. The +enhanced verification restrictions will improve the security of programs +deployed to the blockchain, filtering out unwarranted behavior that could be +used with malicious intents. + +## Security Considerations + +None. \ No newline at end of file