From 5f7f660c6e247cf0e91d87c6d64635908997f738 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 8 Mar 2023 22:17:35 +0100 Subject: [PATCH] Add FV specs for Initializable (#4095) Co-authored-by: Francisco --- certora/harnesses/InitializableHarness.sol | 23 +++ certora/specs.json | 5 + certora/specs/Initializable.spec | 165 +++++++++++++++++++++ 3 files changed, 193 insertions(+) create mode 100644 certora/harnesses/InitializableHarness.sol create mode 100644 certora/specs/Initializable.spec diff --git a/certora/harnesses/InitializableHarness.sol b/certora/harnesses/InitializableHarness.sol new file mode 100644 index 000000000..19437e0fc --- /dev/null +++ b/certora/harnesses/InitializableHarness.sol @@ -0,0 +1,23 @@ +// SPDX-License-Identifier: MIT +pragma solidity ^0.8.2; + +import "../patched/proxy/utils/Initializable.sol"; + +contract InitializableHarness is Initializable { + function initialize() public initializer {} + function reinitialize(uint8 n) public reinitializer(n) {} + function disable() public { _disableInitializers(); } + + function nested_init_init() public initializer { initialize(); } + function nested_init_reinit(uint8 m) public initializer { reinitialize(m); } + function nested_reinit_init(uint8 n) public reinitializer(n) { initialize(); } + function nested_reinit_reinit(uint8 n, uint8 m) public reinitializer(n) { reinitialize(m); } + + function version() public view returns (uint8) { + return _getInitializedVersion(); + } + + function initializing() public view returns (bool) { + return _isInitializing(); + } +} diff --git a/certora/specs.json b/certora/specs.json index c22b1ebba..8e4fe21f4 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -28,5 +28,10 @@ "certora/harnesses/ERC3156FlashBorrowerHarness.sol" ], "options": ["--optimistic_loop"] + }, + { + "spec": "Initializable", + "contract": "InitializableHarness", + "files": ["certora/harnesses/InitializableHarness.sol"] } ] diff --git a/certora/specs/Initializable.spec b/certora/specs/Initializable.spec new file mode 100644 index 000000000..1ba8d54e8 --- /dev/null +++ b/certora/specs/Initializable.spec @@ -0,0 +1,165 @@ +import "helpers.spec" + +methods { + // initialize, reinitialize, disable + initialize() envfree + reinitialize(uint8) envfree + disable() envfree + + nested_init_init() envfree + nested_init_reinit(uint8) envfree + nested_reinit_init(uint8) envfree + nested_reinit_reinit(uint8,uint8) envfree + + // view + version() returns uint8 envfree + initializing() returns bool envfree +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Definitions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +definition isUninitialized() returns bool = version() == 0; +definition isInitialized() returns bool = version() > 0; +definition isDisabled() returns bool = version() == 255; + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: A contract must only ever be in an initializing state while in the middle of a transaction execution. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant notInitializing() + !initializing() + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: The version cannot decrease & disable state is irrevocable. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule increasingVersion(env e) { + uint8 versionBefore = version(); + bool disabledBefore = isDisabled(); + + method f; calldataarg args; + f(e, args); + + assert versionBefore <= version(), "_initialized must only increase"; + assert disabledBefore => isDisabled(), "a disabled initializer must stay disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot initialize a contract that is already initialized. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotInitializeTwice() { + require isInitialized(); + + initialize@withrevert(); + + assert lastReverted, "contract must only be initialized once"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot initialize once disabled. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotInitializeOnceDisabled() { + require isDisabled(); + + initialize@withrevert(); + + assert lastReverted, "contract is disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot reinitialize once disabled. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotReinitializeOnceDisabled() { + require isDisabled(); + + uint8 n; + reinitialize@withrevert(n); + + assert lastReverted, "contract is disabled"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Cannot nest initializers (after construction). │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule cannotNestInitializers_init_init() { + nested_init_init@withrevert(); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_init_reinit(uint8 m) { + nested_init_reinit@withrevert(m); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_reinit_init(uint8 n) { + nested_reinit_init@withrevert(n); + assert lastReverted, "nested initializers"; +} + +rule cannotNestInitializers_reinit_reinit(uint8 n, uint8 m) { + nested_reinit_reinit@withrevert(n, m); + assert lastReverted, "nested initializers"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Initialize correctly sets the version. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule initializeEffects() { + requireInvariant notInitializing(); + + bool isUninitializedBefore = isUninitialized(); + + initialize@withrevert(); + bool success = !lastReverted; + + assert success <=> isUninitializedBefore, "can only initialize uninitialized contracts"; + assert success => version() == 1, "initialize must set version() to 1"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Reinitialize correctly sets the version. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule reinitializeEffects() { + requireInvariant notInitializing(); + + uint8 versionBefore = version(); + + uint8 n; + reinitialize@withrevert(n); + bool success = !lastReverted; + + assert success <=> versionBefore < n, "can only reinitialize to a latter versions"; + assert success => version() == n, "reinitialize must set version() to n"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: Can disable. │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule disableEffect() { + requireInvariant notInitializing(); + + disable@withrevert(); + bool success = !lastReverted; + + assert success, "call to _disableInitializers failed"; + assert isDisabled(), "disable state not set"; +}