From 15e7d27104bcb8a515c8d9f109a055b0a894e74a Mon Sep 17 00:00:00 2001 From: Mikhail Date: Mon, 3 Jul 2023 13:58:41 +0200 Subject: [PATCH] Add owner related invariants --- .github/workflows/certora.yml | 4 +-- certora/harnesses/SafeHarness.sol | 4 +++ certora/scripts/verifySafe.sh | 2 +- certora/specs/Safe.spec | 49 +++++++++++++++++++++++-------- 4 files changed, 43 insertions(+), 16 deletions(-) diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml index e11365ee6..db054b7b0 100644 --- a/.github/workflows/certora.yml +++ b/.github/workflows/certora.yml @@ -25,8 +25,8 @@ jobs: uses: actions/setup-java@v3 with: { java-version: "17", java-package: jre, distribution: semeru } - - name: Install certora cli-beta - run: pip install -Iv certora-cli-beta==4.2.0 + - name: Install certora cli + run: pip install -Iv certora-cli - name: Install solc run: | diff --git a/certora/harnesses/SafeHarness.sol b/certora/harnesses/SafeHarness.sol index 822415d4f..251ed0ece 100644 --- a/certora/harnesses/SafeHarness.sol +++ b/certora/harnesses/SafeHarness.sol @@ -24,6 +24,10 @@ contract SafeHarness is Safe { return getGuard(); } + function getOwnersCount() public view returns (uint256) { + return ownerCount; + } + function getNativeTokenBalance() public view returns (uint256) { return address(this).balance; } diff --git a/certora/scripts/verifySafe.sh b/certora/scripts/verifySafe.sh index c909a4188..7315e1bb5 100755 --- a/certora/scripts/verifySafe.sh +++ b/certora/scripts/verifySafe.sh @@ -10,7 +10,7 @@ certoraRun certora/harnesses/SafeHarness.sol \ --verify SafeHarness:certora/specs/Safe.spec \ --solc solc7.6 \ --optimistic_loop \ - --prover_args "-optimisticFallback true" \ + --prover_args '-optimisticFallback true' \ --loop_iter 3 \ --optimistic_hashing \ --hashing_length_bound 352 \ diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec index f09780902..2078eb049 100644 --- a/certora/specs/Safe.spec +++ b/certora/specs/Safe.spec @@ -9,17 +9,18 @@ methods { function getModule(address) external returns (address) envfree; function getSafeGuard() external returns (address) envfree; function getNativeTokenBalance() external returns (uint256) envfree; + function getOwnersCount() external returns (uint256) envfree; // optional - function execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation) external returns (bool, bytes memory); - function execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation) external returns (bool); - function execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool); + function execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation) external returns (bool, bytes memory); + function execTransactionFromModule(address,uint256,bytes,Enum.Operation) external returns (bool); + function execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes) external returns (bool); } definition noHavoc(method f) returns bool = - f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector - && f.selector != sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector - && f.selector != sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector; + f.selector != sig:execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation).selector + && f.selector != sig:execTransactionFromModule(address,uint256,bytes,Enum.Operation).selector + && f.selector != sig:execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes).selector; definition reachableOnly(method f) returns bool = f.selector != sig:setup(address[],uint256,address,bytes,address,address,uint256,address).selector @@ -46,7 +47,7 @@ rule nonceMonotonicity(method f) filtered { uint256 nonceAfter = nonce(); assert nonceAfter != nonceBefore => - to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector; + to_mathint(nonceAfter) == nonceBefore + 1 && f.selector == sig:execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes).selector; } @@ -128,6 +129,28 @@ hook Sstore SafeHarness.(slot 49122629484629529244014240937346711770925847994644 fallbackHandlerAddress = newFallbackHandlerAddress; } +invariant threholdShouldBeLessThanOwners() getOwnersCount() >= getThreshold() + filtered { f -> reachableOnly(f) } + { preserved { + // The prover found a counterexample if the owners count is max uint256, + // but this is not a realistic scenario. + require getOwnersCount() >= 1 && getOwnersCount() < MAX_UINT256(); + } + } + +invariant safeOwnerCannotBeItself(env e) !isOwner(e, currentContract) + filtered { f -> reachableOnly(f) } + +rule safeOwnerCannotBeSentinelAddress(env e, method f) filtered { + f -> reachableOnly(f) +} { + calldataarg args; env e; + f(e, args); + + assert isOwner(e, 1) == false; +} + + rule fallbackHandlerAddressChange(method f) filtered { f -> f.selector != sig:simulateAndRevert(address,bytes).selector && f.selector != sig:getStorageAt(uint256,uint256).selector @@ -174,16 +197,16 @@ rule nativeTokenBalanceSpending(method f) filtered { uint256 balanceAfter = getNativeTokenBalance(); assert balanceAfter < balanceBefore => - f.selector == sig:execTransaction(address,uint256,bytes,SafeHarness.Operation,uint256,uint256,uint256,address,address,bytes).selector - || f.selector == sig:execTransactionFromModule(address,uint256,bytes,SafeHarness.Operation).selector - || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,SafeHarness.Operation).selector; + f.selector == sig:execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes).selector + || f.selector == sig:execTransactionFromModule(address,uint256,bytes,Enum.Operation).selector + || f.selector == sig:execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation).selector; } rule nativeTokenBalanceSpendingExecTransaction( address to, uint256 value, bytes data, - SafeHarness.Operation operation, + Enum.Operation operation, uint256 safeTxGas, uint256 baseGas, uint256 gasPrice, @@ -208,7 +231,7 @@ rule nativeTokenBalanceSpendingExecTransactionFromModule( address to, uint256 value, bytes data, - SafeHarness.Operation operation + Enum.Operation operation ) { uint256 balanceBefore = getNativeTokenBalance(); env e; @@ -226,7 +249,7 @@ rule nativeTokenBalanceSpendingExecTransactionFromModuleReturnData( address to, uint256 value, bytes data, - SafeHarness.Operation operation + Enum.Operation operation ) { uint256 balanceBefore = getNativeTokenBalance(); env e;