Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Setup certora workflow #96

Draft
wants to merge 16 commits into
base: main
Choose a base branch
from
Draft

Conversation

akshay-ap
Copy link
Contributor

@akshay-ap akshay-ap commented Sep 1, 2023

Fixes #95
Changes in PR:

  • Create certora.yml
  • Set CERTORA_KEY in github secrets
  • Create spec file
  • Add README

Add Rules and invariants

  • Registry can be only set by owner

Additional properties:

  • Paginated list of enabled modules
  • Only Enabled, whitelisted and non-flagged Plugin can execute transaction through a Safe
  • Only Enabled, whitelisted and non-flagged Plugin can root-execute transaction through a Safe
  • Non-root tx should not update any state of the account i.e. call to self blocked if permission not granted
  • no dangling permissions for disabled Plugins
  • Temporary storage is cleared

@akshay-ap akshay-ap added the enhancement New feature or request label Sep 1, 2023
@akshay-ap akshay-ap self-assigned this Sep 1, 2023
@akshay-ap akshay-ap marked this pull request as draft September 1, 2023 12:28
@github-actions
Copy link

github-actions bot commented Sep 18, 2023

Pull Request Test Coverage Report for Build 6299064684

  • 3 of 28 (10.71%) changed or added relevant lines in 5 files are covered.
  • No unchanged relevant lines lost coverage.
  • Overall coverage decreased (-8.6%) to 91.395%

Changes Missing Coverage Covered Lines Changed/Added Lines %
contracts/test/TestFunctionHandlerCertora.sol 0 2 0.0%
contracts/test/certora/TestHooksCertora.sol 0 5 0.0%
contracts/test/TestExecutorCertora.sol 0 18 0.0%
Totals Coverage Status
Change from base Build 6262748768: -8.6%
Covered Lines: 184
Relevant Lines: 209

💛 - Coveralls

@@ -83,6 +83,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana
if (areHooksEnabled) {
// execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender.
// executionType = 1 for plugin flow
// should check below exist here?
checkPermittedModule(hooksAddress);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should revert or skip if flagged?

@@ -140,6 +142,8 @@ contract SafeProtocolManager is ISafeProtocolManager, RegistryManager, HooksMana
if (areHooksEnabled) {
// execution metadata for transaction execution through plugin is encoded address of the plugin i.e. msg.sender.
// executionType = 1 for plugin flow
// should check below exist here?
checkPermittedModule(hooksAddress);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should revert or skip if flagged?

@@ -69,6 +69,8 @@ abstract contract FunctionHandlerManager is RegistryManager {
revert FunctionHandlerNotSet(account, functionSelector);
}

checkPermittedModule(functionHandler);
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should revert or skip if flagged?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

In my opinion, since this doesn't affect the core execution flow, it's OK to revert here.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Formal verification of protocol
2 participants