search

safe-global / safe-smart-account

Safe allows secure management of blockchain assets.
https://safe.global
GNU Lesser General Public License v3.0
1.84k stars 907 forks source link

Make checkSignature rule run. #661

Closed jhoenicke closed 1 year ago

jhoenicke commented 1 year ago

Moved assembly code for the case v=0 from checkNSignature to new function checkExternalSignature. This way we can summarize this function, in this case by NONDET.

Before, the assembly code broke the pointer analysis, which switched the prover in failsafe mode, where it is (a) much slower and (b) computes different hashes than in the normal mode. The latter was a problem because for the harness function getCurrentOwner the analysis always succeeded and thus computed a different hash. By being able to summarize the checkExternalSignature function and the splitSignature function, the pointer analysis doesn't have to consider the assembly code.

I also tweaked timeout settings in particular mediumTimeout was too low. It's a compromise between waiting for timeout for the cases where we need to split, because the problem is too big for the solver, and unnecessarily splitting when waiting a bit longer would have succeeded.

jhoenicke commented 1 year ago

I didn't change or add any comments. If you would port this munging in the original code, you definitely want to change the references to s in the comments so that they refer to offset. And probably add a function comment 😁.

mmv08 commented 1 year ago

@rmeissner would love to get your opinion about adjusting this in the original code for the v1.5.0 release so we don't have significant differences between formally verified and production code