safe-global / safe-smart-account / 12805189361

94%

push

github

Formal Verification for Safe v1.5 Audit (#901)

This pull request corresponds to the formal verification aspect of the
Safe v1.5 audit done by Certora.

## Summary of Changes

### Added

Configuration and Specification files corresponding to new rules:
* `execute.conf` and `Execute.spec`
* `extensible.conf` and `Extensible.spec`
* `fallback.conf` and `Fallback.spec`
* `guards.conf` and `Guards.spec`
* `hash.conf` and `Hash.spec`
* `setup.conf` and `Setup.spec`

Harness:
* `ExtensibleFallbackHandlerHarness.sol` to reason about the fallback
handler

Mocks:
* `DummyHandler.sol` for reasoning about the fallback handler
* `TxnGuardMock.sol` and `TxnGuardMockDuplicate.sol` for reasoning about
the transaction guard
* `ModuleGuardMock.sol` and `ModuleGuardMockDuplicate.sol` for reasoning
about the module guard

### Modified
* `applyHarness.patch` - added some minor munging as explained in the
audit report
* `run.conf` - remove a deprecated configuration tag that was giving
errors to the Prover
* `Safe.spec` - moved a rule about guards to `Guard.spec` for logical
continuity
* `SafeHarness.sol` - added some view functionality to the Safe harness
for some rules

Co-authored-by: Derek Sorensen <derek-certora@Dereks-MacBook-Pro.local>

325 of 366 branches covered (88.8%)

Branch coverage included in aggregate %.

499 of 511 relevant lines covered (97.65%)

100.87 hits per line