Social Recovery Module Update #23
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Basic FV Setup
This PR sets up the Safe Harness along with a dummy rule to test the functionality of the same. Instead of using `link` as we had for the `safe-locking` setup, we are using a function called `requireSocialRecoveryModuleEnabled(...)` which requires that the `SocialRecoveryModule` is enabled for the Safe. Fixes #2
This PR syncs from Candide's repo to get 100% code coverage (implemented by the Candide Team). --------- Co-authored-by: Andrew Wahid <andrew.wahid1@gmail.com>
…ntracts into candidelabs-main
This PR adds a few rules which mainly check two things regarding guardians in a Social Recovery Module: - Adding a guardian - Removing a guardian for a Safe Smart Account using the Social Recovery Module. In addition to the above, there are some slights changes in: - The `conf` file is updated with more flags for iteration. - Using Harness for both the Social Recovery Module and Guardian Storage (Optimistically, because we only have created a new function for Guardian Storage, and not yet anything for the Social Recovery Module). Note: As a workaround for the linked list-based invariant, a `require` (with comments) is added to avoid problems until #15 is implemented. Fixes #4
Fixes #18 This PR adds a single rule which checks that under ideal conditions, the `confirmRecovery(...)` can always be called by a guardian to either initiate/execute the recovery process.
Closes #5 This PR adds a rule which checks that the finalization of the recovery process is not possible for a safe account that has disabled the recovery module. The prover found a counter-example which allows calling the finalize function with zero new owners and threshold from a safe having exactly one owner. Recovery initiation with zero new owners is not possible, thus this counter-example is not considered (but still we check the owner structure is not changed for the safe account after the finalize function call).
This PR prepares the repo for audit. Once this PR is merged, a new branch called `audit` will be created. Changes: - Formatting changes were made using `prettier`. - Import updated to use named import. - Using `getRecoveryHash` instead of `keccak256(encodeRecoveryData(...))`
Fixes #13 Changes in PR: - Add rule: `cancelRecovery` - Add rule: `cancelRecoveryDoesNotAffectOtherWallet` --------- Co-authored-by: Shebin John <admin@remedcu.com>
Fixes #15 Changes in PR: - Create conf and spec file to formally verify Guardian storage --------- Co-authored-by: Shebin John <admin@remedcu.com> Co-authored-by: Nicholas Rodrigues Lordello <n@lordello.net>
Changes in PR: - Minor fixes in comments
Fixes #10 This PR adds a rule that verifies that the guardian can only initiate recovery for the ones where it is marked as guardian. This rule only checks for the initiation and not the recovery, thus `execute` is passed as `false`. Suggested from the Certora team, we made the `smt_groundQuantifiers` to be `false` as the `newOwners` array even with the `require` was not creating address within the range (`2^160`).
This PR changes the design of how the guardians are stored. Prior to this change, the guardians were stored in a separate contract `GuardianStorage`. The `GuardianStorage` address was then passed as a constructor parameter to `SocialRecoveryModule` which could then make changes to the list on request by the user. So, the recovery functionality was achieved by having two contracts and thus, two storages. As a side effect, it was initially brought to light that any other module can also modify the list of Guardians in `GuardianStorage` and was not write-restricted only to `SocialRecoveryModule`. Any other enabled module on a Safe could change this list. See: https://github.com/5afe/CandideWalletContracts/blob/870f82d3c4d286b3fd9241c6479c9472d7d73fc6/contracts/modules/social_recovery/storage/GuardianStorage.sol#L35 The initial argument for accepting this behavior was that any malicious module can: 1- Change ownership of the account 2- Steal all account's funds 3- Execute any arbitrary function of the `SocialRecoveryModule` impersonating the owner Thus, it did not violate any security assumptions. Also, allowing the guardian list to be edited by any module allows upgradability of `SocialRecoveryModule` without having to migrate the list of guardians. But, later auditing partner also reported the same behavior as an issue with the argument: - There should be a distinction between malicious modules (or any modules that can perform arbitrary operations) and modules that are limited to do these things by their implementation. These "well behaving" modules will effectively gain more privileges than they actually need. - It opens a new attack vector and violates least privilege principle. After internal discussion, we concluded that allowing any module to modify the guardians list should not be permitted and this PR reflects the same. In this PR, `SocialRecoveryModule` inherits `GuardianStorage` so that there is only 1 contract involved in recovery functionality. By making this change and removing `onlyModule` modifier, and other changes in the code (removing `_wallet` as a parameter in some functions) now allows only wallet i.e. `msg.sender` to change the guardians. This also simplifies the design of the recovery functionality and enforces to use storage space of a single contract i.e. `SocialRecoveryModule`. Other changes in PR include: - Fixes to files related to formal verification - Removing duplicated code which is now not needed - Remove redundant parameter `_wallet` in some functions --------- Co-authored-by: Shebin John <admin@remedcu.com> Co-authored-by: Nicholas Rodrigues Lordello <n@lordello.net>
Fixes #6 This PR adds a single rule which checks if the `confirmRecovery(...)` call is successful, then the caller must be a guardian. --------- Co-authored-by: Mikhail <16622558+mmv08@users.noreply.github.com>
This pull request adds a formal verification rule that verifies that the delay period has to be always passed before finalizing the recovery. I also extracted a requirement for a pending recovery process to a helper function. I tested the rule by commenting out [this](https://github.com/5afe/CandideWalletContracts/blob/870f82d3c4d286b3fd9241c6479c9472d7d73fc6/contracts/modules/social_recovery/SocialRecoveryModule.sol#L238) line and it was caught: https://prover.certora.com/output/6575/3e23871afade4f1aaaadddf2a7dcd0c9/?anonymousKey=6a0ba85ca6c02acb503d1620918ab642bd00d55e
Fixes #7 This PR merges the `canFinalizeRecoveryOnlyAfterDelayPeriod` rule which checks that a call to the `finalizeRecovery` can only succeed after the delay period with an additional check to ensure that if reverted, what are the conditions possible.
This PR adds an extra function called `invalidateNonce(...)` based on the recommendation from the audit team to invalidate a particular recovery process. It could be used in two ways: - Assuming the owner lost access to the Safe, the owner requests a guardian for recovery initiation. Once the recovery initiation started, the owner realized that the access was not actually lost, thus to invalidate the current initiation (not execution, for that owner can use `cancelRecovery(...)`), the owner can actually call the `invalidateNonce(...)`. - As a best practice to invalidate any `confirmedHashes[...][...]` from a guardian which is soon to be removed. Also added: - a test to check if execution fails in the case of an invalidated nonce. - run test in CI. - FV to check if invalidating a nonce cancels an execution of recovery. --------- Co-authored-by: Nicholas Rodrigues Lordello <n@lordello.net>
Related to #26 This PR adds the audit report by Ackee Blockchain for the `0.0.1` version of the Social Recovery Module. P.S. The `docs` folder was `.gitignore`-ed, so kept the audit folder separate.
Fixes #9 This PR adds one rule to check that actions done by one safe should not affect another safe smart account. Here we also require that the `otherSafeContract` be different from `safeContract` instead of implications as the rule specifically looks for that case.
Fixes #11 Changes in PR: - Adds a rule that verifies that recovery is always possible given certain conditions are met. These conditions are mentioned in the spec comments. These additional conditions on top of the 2 conditions given in the issue are required because proves reports counter example without them. - This rule is different from `finalizeRecovery`. The new rule here verifies that recovery should always work when certain conditions are met. --------- Co-authored-by: Nicholas Rodrigues Lordello <n@lordello.net> Co-authored-by: Mikhail <16622558+mmv08@users.noreply.github.com>
…ry (#41) This PR implements #17 by adding the following rules: - the rule that verifies that the amount of approvals counted by the `multiConfirmRecovery` function equals to the length of supplied signature array - duplicate signatures should always revert - if the signature check reverts, then the function should revert - the function doesn't add any shadow approvals not included in the signatures array I created a separate specs file and configuration to summarize a couple of functions. Otherwise, the run would timeout Failed runs where I introduced bugs: - removed the call to `validateGuardianSignature` - https://prover.certora.com/output/6575/73ebaf5c425447129adda18cc8a33d7c?anonymousKey=56669628037dafe0f4d909daea90212c828559cc - added a shadow approval https://prover.certora.com/output/6575/75b1e75c0fcc4c7fa7d9758762a42873/?anonymousKey=d2180d11c689ac54b75f076119ac18d1c7eb5205 and https://prover.certora.com/output/6575/b9cb509223b94526976698728d715b01/?anonymousKey=1bf9bb9f412488d3d4785c1a81affc7169635d18 - removed the duplicated signer check https://prover.certora.com/output/6575/41cd0e1911864c8e94629963d46f35f6/?anonymousKey=48962fbfca64772215f0f57f72f3f38f93302431 --------- Co-authored-by: Nicholas Rodrigues Lordello <n@lordello.net>
This PR updates the summary with `DISPATCHER(false)` in `RecoveryConfirmationSignatureValidity.spec` as for most cases, it works as intended (i.e. find the correct implementation from the available contracts) and a summary is not required (to include possible reverting paths as well). Also, we found one case which should be checked (`isModuleEnabled(...)`) but was ignored because we used a summary before.
This PR updates the summary to use `DISPATCHER(true)` for the `execTransactionFromModule`. From Certora Team: > DISPATCHER(false) and DISPATCHER(true) both first try any known Contract. The difference should be only if a different contract is called which is not explicitly linked into the scene. With DISPATCHER(true) the prover just assumes that this will never happens. It only tries those input values for which you only call known contracts. With DISPATCHER(false), the prover will also consider the case you call an unknown contract and in that case assumes the worst, i.e. all ghost variables are havoced and the return value is arbitrary. So you get a lot of spurious counterexamples with DISPATCHER(false), but with DISPATCHER(true) you are technically unsound, as you don’t verify anything if unknown contracts could be called. So, In our case, as we already summarized call to `execTransactionFromModule(...)` if `callee` is `safeContract` before. And as the summary goes for the non-reverting path, I think it is safe to use `DISPATCHER(true)` here. P.S. For the `RecoveryConfirmationSignatureValidity.spec`, as we didn't require some method specified, that was removed, along with an extra harness function.
Fixes #36 This PR introduces a few rules which check the state change and the resulting function call for the same. A new harness function is introduced for easier guardians list check with FV.
This PR updates a few things for #47 - Formatting `README` and adding details to run FV. - Ordering `GuardianStorage.spec` contents. - Updating the `conf` file of FV. - Upgrading certora version to 7.6.3 No new FV rule/invariant is introduced.
This PR updates the README based on the suggestions mentioned in #49 (comment)
|
One small improvement we can make before "un-drafting" the PR would be to not make the FV GitHub action fail when the key is missing, but instead not skip it. |
This PR adds a check to see if the `CERTORA_KEY` is set or not to run the CI. If the key is not set, the Certora check will show as "Skipped" instead of Success in the GitHub Actions. This ensures that the repo can be upstreamed to Candide without any immediate failure to the CI. It also ensures that it doesn't show the impression of FV passing without verification. P.S. I have disabled the ruleset which required all the FV tasks to be successful so this could be included.
andrewwahid
approved these changes
Jul 1, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This PR introduces some breaking changes to the Social Recovery Module. This PR does the following:
GuardianStorage. (Non-backward compatible)nonce5afe/CandideWalletContracts#40)mainbranch for added security.)