diff --git a/certora/confs/SafeWebAuthnSignerFactory.conf b/certora/confs/SafeWebAuthnSignerFactory.conf index 697e519e2..a239eaeca 100644 --- a/certora/confs/SafeWebAuthnSignerFactory.conf +++ b/certora/confs/SafeWebAuthnSignerFactory.conf @@ -15,6 +15,7 @@ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" ], + "exclude_rule": ["createAndVerifyEQtoIsValidSignatureForSigner"], "rule_sanity": "basic", "solc": "solc8.23", "solc_via_ir": false, diff --git a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol index 872879470..b14b24f23 100644 --- a/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol @@ -30,10 +30,10 @@ contract SafeWebAuthnSignerFactoryHarness is SafeWebAuthnSignerFactory { magicValue = abi.decode(result, (bytes4)); } - // /** - // munge to pass the SignerCreationCantOverride rule. - // */ - // function _hasNoCode(address account) internal view override returns (bool result) { - // return account.code.length > 0; - // } + /** + munge to pass the SignerCreationCantOverride rule. + */ + function _hasNoCode(address account) internal view override returns (bool result) { + return account.code.length > 0; + } } diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 9295f982b..22f78b958 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -98,12 +98,14 @@ rule createAndGetSignerEquivalence(){ ghost mathint numOfCreation; ghost mapping(address => uint) address_map; +ghost address signerAddress; hook EXTCODESIZE(address addr) uint v{ require address_map[addr] == v; } hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ + require(v == signerAddress); numOfCreation = numOfCreation + 1; address_map[v] = length; } @@ -152,7 +154,7 @@ rule createAndVerifyEQtoIsValidSignatureForSigner() bytes signature; bytes32 message; - address signerAddress = getSigner(e, x, y, verifier); + signerAddress = getSigner(e, x, y, verifier); require(numOfCreation == 0); require(hasNoCode(e, signerAddress)); require(WebAuthnHarness.castSignatureSuccess(e, message, signature));