Skip to content
This repository was archived by the owner on Oct 27, 2025. It is now read-only.

Setup certora workflow - #96

Draft
akshay-ap wants to merge 16 commits into
mainfrom
feature-95-formal-verification
Draft

Setup certora workflow#96
akshay-ap wants to merge 16 commits into
mainfrom
feature-95-formal-verification

Conversation

@akshay-ap

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

Copy link
Copy Markdown
Contributor

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

github-actions Bot commented Sep 18, 2023

Copy link
Copy Markdown

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

// 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
Copy Markdown
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?

// 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
Copy Markdown
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?

revert FunctionHandlerNotSet(account, functionSelector);
}

checkPermittedModule(functionHandler);

Copy link
Copy Markdown
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
Copy Markdown
Contributor

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.

@4player90 4player90 left a comment

Copy link
Copy Markdown

Choose a reason for hiding this comment

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

Looks okay

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Labels

enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Formal verification of protocol

3 participants