Feature: Extract contract signature check into a function to allow summarization during formal verification

safe-global / safe-smart-account

Safe allows secure management of blockchain assets.

https://safe.global

GNU Lesser General Public License v3.0

1.88k stars 927 forks source link

Feature: Extract contract signature check into a function to allow summarization during formal verification #662

Closed mmv08 closed 1 year ago

mmv08 commented 1 year ago

This PR:

Extracts contract signature to a separate function called checkContractSignature to allow summarization during formal verification because lots of assembly in the function broke the pointer analysis in the prover
Add a rule that verifies that calling checkNSignatures for each signature individually is equal to calling checkSignatures
Adds a blueprint for the rule that verifies that signatures are always provided for executed transactions. However, it's commented now because of prover bugs on the summarization + execTransaction function. I reported to the Certora team, waiting for a fix or further guidance.

cc @jhoenicke

coveralls commented 1 year ago

Pull Request Test Coverage Report for Build 6352532543

8 of 8 (100.0%) changed or added relevant lines in 1 file are covered.
No unchanged relevant lines lost coverage.
Overall coverage increased (+0.01%) to 92.784%

Totals
Change from base Build 6352468698:	0.01%
Covered Lines:	338
Relevant Lines:	358

💛 - Coveralls

mmv08 commented 1 year ago

I have no idea why the lint action is failing, and it doesn't display any error. Also, locally, it doesn't exit with the code 1.

mmv08 commented 1 year ago

Do we know if this adds any overhead on the contract size and gas costs?

Before changes:

Safe 23569 bytes (limit is 24576)
SafeL2 24411 bytes (limit is 24576)

After changes:

Safe 23599 bytes (limit is 24576)
SafeL2 24441 bytes (limit is 24576)

So, it increases the code size by 30 bytes. Regarding the gas costs, I'm not sure. We don't have benchmarks set up for contract signers. I can try setting up some, but it also heavily varies on the actual verification logic in the contract

mmv08 commented 1 year ago

Actually, it did increase gas costs for EOA signers as well: Before:

Ether - transfer
           Used 21000n gas for >transfer<
    ✔ with an EOA (224ms)
           Used 58754n gas for >transfer<
    ✔ with a single owner Safe
           Used 64571n gas for >transfer<
    ✔ with a single owner and guard Safe
           Used 65820n gas for >transfer<
    ✔ with a 2 out of 2 Safe
           Used 72875n gas for >transfer<
    ✔ with a 3 out of 3 Safe
           Used 72863n gas for >transfer<
    ✔ with a 3 out of 5 Safe

After:

    Ether - transfer
           Used 21000n gas for >transfer<
    ✔ with an EOA (213ms)
           Used 58777n gas for >transfer<
    ✔ with a single owner Safe
           Used 64606n gas for >transfer<
    ✔ with a single owner and guard Safe
           Used 65855n gas for >transfer<
    ✔ with a 2 out of 2 Safe
           Used 72910n gas for >transfer<
    ✔ with a 3 out of 3 Safe
           Used 72922n gas for >transfer<
    ✔ with a 3 out of 5 Safe

So, for EOA signers gas costs are increased by 20-40 gas

mmv08 commented 1 year ago

Interesting, so after reverting the removal of the unused "data" param in checkSignatures (link), the gas costs are back to normal and even less in the single owner case in some benchmarks:

 Ether - transfer
           Used 21000n gas for >transfer<
    ✔ with an EOA (216ms)
           Used 58742n gas for >transfer<
    ✔ with a single owner Safe
           Used 64571n gas for >transfer<
    ✔ with a single owner and guard Safe
           Used 65820n gas for >transfer<
    ✔ with a 2 out of 2 Safe
           Used 72875n gas for >transfer<
    ✔ with a 3 out of 3 Safe
           Used 72887n gas for >transfer<
    ✔ with a 3 out of 5 Safe

mmv08 commented 1 year ago

@rmeissner I reverted the change