safe-global / safe-modules / 7265551640

85%

push

github

4337 module formal verification (#162)

This PR is related to #142

Changes in PR:
- Setup spec files, and configuration files for Formal Verification
using Certora
- Setup harnesses contracts
- Add GitHub workflow file

Rules Implemented:

- onlyEntryPointCallable
This rule verifies that methods related to 4337 are only callable by the
entrypoint contract: `validateUserOp(..)`, `executeUserOp(...)` and
`executeUserOpWithErrorString(...)`

- checkSignaturesIsCalledIfValidateUserOpSucceeds
This rule verifies that `checkSignatures(...)` is always called
`validateUserOp(...)` function is invoked

- signatureTimestampsPresentInValidationData
This rule verifies that `validAfter` and `validUntil` are present in the
first 12 bytes of the validation data returned by the
`validateUserOp(...)` function

- validationDataLastBitZeroIfCheckSignaturesSucceeds
This rule verifies that validation data returned by the
`validateUserOp(...)` contains the last bit `0` if signature validation
succeeds

2. ExecTransactionFromModule.spec 
This rule should verify that `safe.execTransactionFromModule(...)` is
only called by `validateUserOp(..)`, `executeUserOp(...)` and
`executeUserOpWithErrorString(...)`

3. PayMissingFunds.spec
This rule should verify that the Module sends only `missingAccountFunds`
from Safe to EntryPoint contract

4. ValidationDataLastBitOne.spec
This rule should verify that validation data returned by the
`validateUserOp(...)` contains the last bit `1` if signature validation
fails

---------

Co-authored-by: Mikhail <16622558+mmv08@users.noreply.github.com>

22 of 124 branches covered (0.0%)

Branch coverage included in aggregate %.

33 of 282 relevant lines covered (11.7%)

2.93 hits per line