Proof Generation (Immediate Properties)

[DavePearce]

(follows on from #494)

The purpose of this issue is to consider all security properties that arise immediately (in some sense) from the bytecode semantics. Such properties can be checked for without developer interaction (i.e. because they are immediately apparent) though they may require interaction by the proof engineer (e.g. to make the proof go through).

• ADD / MUL / SUB / EXP. Prevent arithmetic overflow / underflow.
• DIV / SDIV / MOD / SMOD. Prevent division by zero.
• SHL / SHR / SAR. Prevent shifts with large rhs ?
• KECCAK256 Prevent out-of-bounds access.
• Caller should this bytecode be allowed?
• CALLDATALOAD / CALLDATACOPY / CODECOPY / EXTCODECOPY Prevent out-of-bounds access.
• RETURNDATACOPY. Prevent out-of-bounds access. Separated from others because this bytecode reverts on out-of-bounds access. Note also that this is not the only way to read RETURNDATA.
• MLoad. Identify loads beyond current memory size?
• LogN. Prevent out-of-bounds access.
• CALL / CALLCODE / DELEGATECALL / STATICCALL. Prevent out-of-bounds access on CALLDATA. Somehow ensure that RETURNDATA is also accessed within bounds (unsure how to though).
• RETURN / REVERT. Prevent out-of-bounds access.
• CREATE / CREATE2. ????
• SELFDESTRUCT ????

Memory Safety

Assembly blocks can be marked as memory-safe. This communicates key information to the optimiser, but is not statically checked. As such adhering properly to these rules could be challenging. The benefits of using memory-safe are that the optimiser is not disabled in surrounding code. Useful quote from this discussion:

The recent compiler versions from 0.8.13 use memory to prevent stack too deep errors by copying some stack variables onto memory and some optimisations.

Thoughts

• What about authentication (e.g. SELFDESTRUCT not by everyone? value transfer not by everyone?)
• What about precompiled contracts?
• What about call depth attacks?
• What about checking return from contract calls?
• What about accidental memory overwriting? E.g. Buffer overflow?
• What about storage / memory corruption?
• What about deadlock? (i.e. zombie contracts)