From dcd229b7eda7121230e7ae4e9dc6441f94e91240 Mon Sep 17 00:00:00 2001 From: Akshay Date: Thu, 8 Aug 2024 10:39:26 +0200 Subject: [PATCH] FV: Ownership update after recovery finalisation (#38) Fixes #8 Changes in PR: - Add a rule that checks for Ownership update after Recovery finalisation - Also fixes a minor issue not related to this PR - Use latest prover cli version so that verification works --------- Co-authored-by: Shebin John --- .github/workflows/certora_recovery.yml | 3 +- certora/conf/OwnerUpdateAfterRecovery.conf | 31 ++ certora/requirements.txt | 2 +- certora/specs/OwnerUpdateAfterRecovery.spec | 336 ++++++++++++++++++ ...RecoveryConfirmationSignatureValidity.spec | 2 +- 5 files changed, 370 insertions(+), 4 deletions(-) create mode 100644 certora/conf/OwnerUpdateAfterRecovery.conf create mode 100644 certora/specs/OwnerUpdateAfterRecovery.spec diff --git a/.github/workflows/certora_recovery.yml b/.github/workflows/certora_recovery.yml index 01542eb..3629d3d 100644 --- a/.github/workflows/certora_recovery.yml +++ b/.github/workflows/certora_recovery.yml @@ -35,8 +35,7 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - rule: ['SocialRecoveryModule', 'GuardianStorage', 'RecoveryConfirmationSignatureValidity'] - + rule: ['SocialRecoveryModule', "GuardianStorage", "RecoveryConfirmationSignatureValidity", "OwnerUpdateAfterRecovery"] steps: - uses: actions/checkout@v4 diff --git a/certora/conf/OwnerUpdateAfterRecovery.conf b/certora/conf/OwnerUpdateAfterRecovery.conf new file mode 100644 index 0000000..ad0acc8 --- /dev/null +++ b/certora/conf/OwnerUpdateAfterRecovery.conf @@ -0,0 +1,31 @@ +{ + "files": [ + "certora/harnesses/SocialRecoveryModuleHarness.sol", + "certora/harnesses/SafeHarness.sol" + ], + "global_timeout": "6200", + "loop_iter": "2", + "msg": "SocialRecoveryModule: Owner(s) updated after recovery", + "solc": "solc-0.8.20", + "optimistic_hashing": true, + "optimistic_loop": true, + "packages": [ + "@safe-global=node_modules/@safe-global", + "@openzeppelin=node_modules/@openzeppelin" + ], + "parametric_contracts": [ + "SocialRecoveryModuleHarness" + ], + "prover_args": [ + "-smt_groundQuantifiers false", + "-splitParallel true", + "-smt_nonLinearArithmetic false", + "-adaptiveSolverConfig false", + "-solvers [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]" + ], + "rule": [ + "recoveryFinalisation" + ], + "smt_timeout": "7000", + "verify": "SocialRecoveryModuleHarness:certora/specs/OwnerUpdateAfterRecovery.spec" +} diff --git a/certora/requirements.txt b/certora/requirements.txt index 24e8bf9..df37fea 100644 --- a/certora/requirements.txt +++ b/certora/requirements.txt @@ -1 +1 @@ -certora-cli==7.6.3 +certora-cli==7.10.1 diff --git a/certora/specs/OwnerUpdateAfterRecovery.spec b/certora/specs/OwnerUpdateAfterRecovery.spec new file mode 100644 index 0000000..705d7fe --- /dev/null +++ b/certora/specs/OwnerUpdateAfterRecovery.spec @@ -0,0 +1,336 @@ +/* + * Spec for linked list reachability. + * + * This file uses a reach predicate: + * ghost ghostReach(address, address) returns bool + * to represent the transitive relation of the next + * relation given by the "owners" field. + * + * The idea comes from the paper + * + * [1] Itzhaky, S., Banerjee, A., Immerman, N., Nanevski, A., Sagiv, M. (2013). + * Effectively-Propositional Reasoning about Reachability in Linked Data Structures. + * In: CAV 2013. Springer, https://doi.org/10.1007/978-3-642-39799-8_53 + */ +using SafeHarness as safeContract; + +methods { + // Social Recovery Module Functions + function isGuardian(address, address) external returns (bool) envfree; + function guardiansCount(address) external returns (uint256) envfree; + function threshold(address) external returns (uint256) envfree; + function nonce(address) external returns (uint256) envfree; + function getRecoveryHash(address, address[], uint256, uint256) external returns (bytes32) envfree; + function getRecoveryApprovals(address, address[], uint256) external returns (uint256) envfree; + function getRecoveryApprovalsWithNonce(address, address[], uint256, uint256) external returns (uint256) envfree; + function countGuardians(address) external returns (uint256) envfree; + function hasGuardianApproved(address, address, address[], uint256) external returns (bool) envfree; + + // Safe Functions + function safeContract.isModuleEnabled(address module) external returns (bool) envfree; + function safeContract.isOwner(address owner) external returns (bool) envfree; + function safeContract.getOwners() external returns (address[] memory) envfree; + function safeContract.getThreshold() external returns (uint256) envfree; + + // Wildcard Functions + function _.execTransactionFromModule(address to, uint256 value, bytes data, Enum.Operation operation) external => DISPATCHER(true); + function _.isModuleEnabled(address module) external => DISPATCHER(false); + function _.isOwner(address owner) external => DISPATCHER(false); + function _.getOwners() external => DISPATCHER(false); + function _._ external => DISPATCH[safeContract.removeOwner(address,address,uint256), + safeContract.addOwnerWithThreshold(address,uint256), + safeContract.swapOwner(address,address,address)] default NONDET; + + + // additional summarizations as NONDET DELETE + function _.getStorageAt(uint256 offset, uint256 length) external => NONDET DELETE; + function _.checkNSignatures(bytes32,bytes,bytes,uint256) external => NONDET DELETE; + function _.getModulesPaginated(address,uint256) external => NONDET DELETE; + function _.execTransaction(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,bytes) external => NONDET DELETE; + function _.execTransactionFromModuleReturnData(address,uint256,bytes,Enum.Operation) external => NONDET DELETE; + function _.checkSignatures(bytes32,bytes,bytes) external => NONDET DELETE; + function _.executeRecovery(address,address[],uint256) external => NONDET DELETE; + function _.simulateAndRevert(address,bytes) external => NONDET DELETE; + function _.confirmRecovery(address,address[],uint256,bool) external => NONDET DELETE; + function _.getGuardians(address) external => NONDET DELETE; + function _.getTransactionHash(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,uint256) external => NONDET DELETE; + function _.encodeTransactionData(address,uint256,bytes,Enum.Operation,uint256,uint256,uint256,address,address,uint256) external => NONDET DELETE; + function _.multiConfirmRecovery(address,address[],uint256,SocialRecoveryModule.SignatureData[],bool) external => NONDET DELETE; + function _.setup(address[],uint256,address,bytes,address,address,uint256,address) external => NONDET DELETE; +} + +definition reachableOnly(method f) returns bool = + f.selector != sig:safeContract.simulateAndRevert(address,bytes).selector; + +// A ghost function to check the reachability for given two addresses. +persistent ghost ghostReach(address, address) returns bool { + init_state axiom forall address X. forall address Y. ghostReach(X, Y) == (X == Y || to_mathint(Y) == 0); +} + +// A ghost mapping to store the owners of Safe. This is required because CVL does not allow calling +// contract functions in quantifiers. +persistent ghost mapping(address => address) ghostOwners { + init_state axiom forall address X. to_mathint(ghostOwners[X]) == 0; +} + +// A ghost function to store the number of successors for each owner for a given wallet address. +// This is used to verify the count of owners for a given wallet address. +persistent ghost ghostSuccCount(address) returns mathint { + init_state axiom forall address X. ghostSuccCount(X) == 0; +} + +// A ghost variable to store the number of owners in the Safe. +persistent ghost uint256 ghostOwnerCount; + +persistent ghost address SENTINEL { + axiom to_mathint(SENTINEL) == 1; +} + +persistent ghost address NULL { + axiom to_mathint(NULL) == 0; +} + +// This invariant ensures that the threshold is non-zero and less than equal owner count. +invariant thresholdSet() safeContract.getThreshold() > 0 && safeContract.getThreshold() <= ghostOwnerCount + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_null(); + requireInvariant reach_invariant(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + } + } + +// SoicalRecoveryModule should not be an owner. +invariant self_not_owner() currentContract != SENTINEL => ghostOwners[currentContract] == 0 + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_null(); + requireInvariant reach_invariant(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant thresholdSet(); + } + } + +// Every element with 0 in the owners field can only reach the null pointer and itself +invariant nextNull() + ghostOwners[NULL] == 0 && + (forall address X. forall address Y. ghostOwners[X] == 0 && ghostReach(X, Y) => X == Y || Y == 0) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_invariant(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant reach_null(); + requireInvariant thresholdSet(); + } + } + +// Every element reaches the 0 pointer (because we replace in reach the end sentinel with null) +invariant reach_null() + (forall address X. ghostReach(X, NULL)) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_invariant(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant thresholdSet(); + } + } + +// Every element with non-zero owner field is reachable from SENTINEL (head of the list) +invariant inListReachable() + ghostOwners[SENTINEL] != 0 && + (forall address key. ghostOwners[key] != 0 => ghostReach(SENTINEL, key)) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant thresholdSet(); + requireInvariant reach_invariant(); + requireInvariant reach_null(); + requireInvariant reachableInList(); + requireInvariant thresholdSet(); + } + } + +// Every element that is reachable from another element is either the null pointer or part of the list. +invariant reachableInList() + (forall address X. forall address Y. ghostReach(X, Y) => X == Y || Y == 0 || ghostOwners[Y] != 0) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_invariant(); + requireInvariant reach_null(); + requireInvariant inListReachable(); + requireInvariant reach_next(); + requireInvariant nextNull(); + requireInvariant thresholdSet(); + } + } + +// Checks that every element reachable from SENTINEL is part of the owners list. +invariant reachHeadNext() + forall address X. ghostReach(SENTINEL, X) && X != SENTINEL && X != NULL => + ghostOwners[SENTINEL] != SENTINEL && ghostReach(ghostOwners[SENTINEL], X) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant reach_invariant(); + requireInvariant reach_null(); + requireInvariant thresholdSet(); + } + } + +// ghostReach encodes a linear order. This axiom corresponds to Table 2 in [1]. +invariant reach_invariant() + forall address X. forall address Y. forall address Z. ( + ghostReach(X, X) + && (ghostReach(X,Y) && ghostReach (Y, X) => X == Y) + && (ghostReach(X,Y) && ghostReach (Y, Z) => ghostReach(X, Z)) + && (ghostReach(X,Y) && ghostReach (X, Z) => (ghostReach(Y,Z) || ghostReach(Z,Y))) + ) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant reach_null(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant reachHeadNext(); + requireInvariant thresholdSet(); + } + } + +// Every element reaches its direct successor (except for the tail-SENTINEL). +invariant reach_next() + forall address X. reach_succ(X, ghostOwners[X]) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant reach_null(); + requireInvariant reach_invariant(); + requireInvariant thresholdSet(); + } + } + +// The number of elements in the list is equal to the number of elements reachable from the SENTINEL. +invariant ownerCountEqualsSentinelSuccessor() safeContract.getOwners().length + 1 == ghostSuccCount(SENTINEL) + filtered { f -> reachableOnly(f) } + { + preserved { + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant reach_null(); + requireInvariant reach_invariant(); + requireInvariant thresholdSet(); + } + } + +// Express the next relation from the reach relation by stating that it is reachable and there is no other element +// in between. +// This is equivalent to P_next from Table 3. +definition isSucc(address a, address b) returns bool = ghostReach(a, b) && a != b && (forall address Z. ghostReach(a, Z) && ghostReach(Z, b) => (a == Z || b == Z)); +definition next_or_null(address n) returns address = n == SENTINEL ? NULL : n; + +// Invariant stating that the owners storage pointers correspond to the next relation, except for the SENTINEL tail marker. +definition reach_succ(address key, address next) returns bool = + (isSucc(key, next_or_null(next))) || + (next == NULL && key == NULL); + +// Update the reach relation when the next pointer of a is changed to b. +// This corresponds to the first two equations in Table 3 [1] (destructive update to break previous paths through a and +// then additionally allow the path to go through the new edge from a to b). +definition updateSucc(address a, address b) returns bool = forall address X. forall address Y. ghostReach@new(X, Y) == + (X == Y || + (ghostReach@old(X, Y) && !(ghostReach@old(X, a) && a != Y && ghostReach@old(a, Y))) || + (ghostReach@old(X, a) && ghostReach@old(b, Y))); + +definition count_expected(address key) returns mathint = + ghostOwners[key] == NULL ? 0 : ghostOwners[key] == SENTINEL ? 1 : ghostSuccCount(ghostOwners[key]) + 1; + +definition updateGhostSuccCount(address key, mathint diff) returns bool = forall address X. + ghostSuccCount@new(X) == ghostSuccCount@old(X) + (ghostReach(X, key) ? diff : 0); + +// Hook to update the ghostOwners and the reach ghost state whenever the owners field +// in storage is written. +// This also checks that the reach_succ invariant is preserved. +hook Sstore safeContract.owners[KEY address key] address value { + address valueOrNull; + address someKey; + require reach_succ(someKey, ghostOwners[someKey]); + require ghostSuccCount(someKey) == count_expected(someKey); + assert ghostReach(value, key) => value == SENTINEL, "list is cyclic"; + ghostOwners[key] = value; + havoc ghostReach assuming updateSucc(key, next_or_null(value)); + mathint countDiff = count_expected(key) - ghostSuccCount(key); + havoc ghostSuccCount assuming updateGhostSuccCount(key, countDiff); + assert reach_succ(someKey, ghostOwners[someKey]), "reach_succ violated after owners update"; + assert ghostSuccCount(someKey) == count_expected(someKey); +} + +// Hook to update the ghostOwnerCount whenever the ownerCount field in storage is written. +hook Sstore safeContract.ownerCount uint256 value { + ghostOwnerCount = value; +} + +// Hook to match ghost state and storage state when reading owners from storage. +// This also provides the reach_succ invariant. +hook Sload address value safeContract.owners[KEY address key] { + require ghostOwners[key] == value; + require reach_succ(key, value); + require ghostSuccCount(key) == count_expected(key); +} + +// Hook to match ghost state and storage state when reading ownerCount from storage. +// This also ensures that ownerCount does not exceed the maximum value of uint256. +hook Sload uint256 value safeContract.ownerCount { + // The prover found a counterexample if the owners count is max uint256, + // but this is not a realistic scenario. + require ghostOwnerCount < max_uint256; + require ghostOwnerCount == value; +} + +// Helper functions to be used in rules that require the recovery to be initiated. +// Pending recovery means: +// - a non-zero `executeAfter` timestamp in the `recoveryRequests` mapping (the smart contract checks it the same way) +// - a non-zero nonce in `walletsNonces` mapping. +function requireInitiatedRecovery(address wallet) { + require currentContract.recoveryRequests[safeContract].executeAfter > 0; + require currentContract.walletsNonces[safeContract] > 0; +} + + +// The rule verifies that after recovery finalisation, the ownership of the Safe changes. +rule recoveryFinalisation(env e) { + requireInitiatedRecovery(safeContract); + + requireInvariant reach_null(); + requireInvariant reach_invariant(); + requireInvariant inListReachable(); + requireInvariant reachableInList(); + requireInvariant ownerCountEqualsSentinelSuccessor(); + uint256 ownersLengthBefore = safeContract.getOwners().length; + + require safeContract.getThreshold() <= ownersLengthBefore; + require ownersLengthBefore > 0; + + uint256 newOwnersCount = currentContract.recoveryRequests[safeContract].newOwners.length; + + uint256 x3; + require x3 < newOwnersCount; + address newOwner = currentContract.recoveryRequests[safeContract].newOwners[x3]; + + finalizeRecovery(e, safeContract); + + address[] ownersAfter = safeContract.getOwners(); + require ownersAfter.length == newOwnersCount; + assert safeContract.isOwner(newOwner); +} diff --git a/certora/specs/RecoveryConfirmationSignatureValidity.spec b/certora/specs/RecoveryConfirmationSignatureValidity.spec index e431fda..4a4623e 100644 --- a/certora/specs/RecoveryConfirmationSignatureValidity.spec +++ b/certora/specs/RecoveryConfirmationSignatureValidity.spec @@ -46,7 +46,7 @@ rule multiConfirmRecoveryOnlyWithLegitimateSignatures(env e) { checkSignatures@withrevert(e, _wallet, recoveryHash, signatures); bool signatureCheckSuccess = !lastReverted; - multiConfirmRecovery(e, _wallet, _newOwners, _newThreshold, signatures, _execute); + multiConfirmRecovery@withrevert(e, _wallet, _newOwners, _newThreshold, signatures, _execute); bool multiConfirmRecoverySuccess = !lastReverted; assert signatureCheckSuccess <=> multiConfirmRecoverySuccess, "Recovery confirmed with invalid signatures";