Audit Draft PR for Code Review #3
Conversation
|
CLA Assistant Lite bot: I have read the CLA Document and I hereby sign the CLA Derek Sorensen seems not to be a GitHub user. You need a GitHub account to be able to sign the CLA. If you have already a GitHub account, please add the email address used for this commit to your account. |
…le guards; this commit ports a rule from Safe.spec so that rules on guards are in the same spec, adds some functionality to the Safe harness, and makes two mocks for the module and transaction guards.
… and all its expected functionality
Pull Request Test Coverage Report for Build 12432928290Details
💛 - Coveralls |
… an enabled module before making the successful call, and adds documentation that refers to an added function to the Safe Harness
|
All the rules are passing now, this codebase also incorporates changes suggested by @nd-certora on the previous draft PR. |
…but for execTransactionFromModuleReturnData
…s both of which are passing
certora/specs/Safe.spec
Outdated
There was a problem hiding this comment.
The rule guardAddressChange was moved from Safe.spec to Guards.spec so that all the rules about guards are in one place.
| ) { | ||
| env e; | ||
| // the txn guard is the mock | ||
| require (getSafeGuard() == txnGuardMock); |
There was a problem hiding this comment.
can we actully assert that the right Guard is called, maybe we will need another Mock2
…anity on the invariant fallbackHanlderNeverSelf, adding the static Dummy to the spec, and strengthening from satisfy to assert
…n and txnGuardCalled are vioalted otherwise
…olve some CVL issues, filter the invariant fallbackHanlderNeverSelf for sanity, etc. overall improvement of rules for fallback
…d) and it's our problem. will update if we can resolve it
|
|
||
| /// @dev a handler, once set via setSafeMethod, is possible to call | ||
| /// @status Done: https://prover.certora.com/output/39601/9fcde04ecd434963b9ce788f7ddea8c1?anonymousKey=a7efde58b28ef7c99264424b66984a8d39b78518 | ||
| rule hanlderCallableIfSet(method f, bytes4 selector) filtered { f -> f.isFallback } { |
| return safeMethods[safe][selector]; | ||
| } | ||
|
|
||
| function getContextAndHandler() external view returns (ISafe safe, address sender, bool isStatic, address handler) { |
There was a problem hiding this comment.
Note that getContext() returns the msg.sender and the last part of the calldata, so it doesn't make sense to call it from CVL. Are you using this only to get the isStatic and handler?
| setGuard(e,guard); | ||
| address gotGuard = getSafeGuard(); | ||
| assert guard == gotGuard; | ||
| } |
There was a problem hiding this comment.
I wonder if we should also check that the guard must implement the guard interface.
ITransactionGuard(guard).supportsInterface(type(ITransactionGuard).interfaceId))
Not sure if it's possible to call an interface method from CVL though. Also that only holds if supportsInterface method is pure (always returns the same value), which theoretically doesn't have to be the case.
… is never self nor the zero address, and now the Prover is misbehaving. Committing here and opening a ticket
Summary
This is a draft PR to make it easy to get code review on the new rules being written.
Files
The new spec and conf files are located in respective
v1.5files, in order to keep the new spec separate (for now) from the old spec.Note
This is a rebased version of a the previous working branch,
derek/audit, onto a more recent commit given by the customer.