From 2e1aaf71436a2f7239207a66338c1243d50349d2 Mon Sep 17 00:00:00 2001 From: liav-certora Date: Thu, 6 Jun 2024 17:05:38 +0300 Subject: [PATCH 1/3] . --- certora/confs/SafeWebAuthnSignerFactory.conf | 7 ---- .../confs/SafeWebAuthnSignerSingleton.conf | 3 ++ certora/specs/SafeWebAuthnSignerFactory.spec | 37 ++++++++++++++++++- .../specs/SafeWebAuthnSignerSingleton.spec | 15 ++++++++ 4 files changed, 53 insertions(+), 9 deletions(-) diff --git a/certora/confs/SafeWebAuthnSignerFactory.conf b/certora/confs/SafeWebAuthnSignerFactory.conf index 6dfe5b5f5..00cb576f3 100644 --- a/certora/confs/SafeWebAuthnSignerFactory.conf +++ b/certora/confs/SafeWebAuthnSignerFactory.conf @@ -7,14 +7,9 @@ "certora/harnesses/ERC20Like/DummyWeth.sol", "certora/harnesses/Utilities.sol", ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" - ], "link": [ "SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton" ], - "msg": "sanity_with_all_default_summaries", - "process": "emv", "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" @@ -26,7 +21,5 @@ "optimistic_hashing": true, "hashing_length_bound": "4694", "loop_iter": "144", - "prover_version": "master", - "server": "production", "verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec" } \ No newline at end of file diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf index cb5d77137..6ffa1786d 100644 --- a/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/certora/confs/SafeWebAuthnSignerSingleton.conf @@ -7,6 +7,9 @@ "modules/passkey/contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarness.sol", ], + "java_args": [ + " -ea -Dlevel.setup.helpers=info" + ], "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 731f268c4..2528c52b1 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -104,16 +104,18 @@ rule deterministicSigner() ghost mathint numOfCreation; ghost mapping(address => uint) address_map; +ghost address createdAddress; ghost bool validValue; -hook EXTCODESIZE(address addr) uint v{ +hook EXTCODESIZE(address addr) uint v { require address_map[addr] == v; validValue = addr <= max_uint160; } -hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{ +hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v { numOfCreation = numOfCreation + 1; address_map[v] = length; + createdAddress = v; } rule SignerCreationCantOverride() @@ -209,4 +211,35 @@ rule isValidSignatureForSignerConsistency() bytes4 magic2 = isValidSignatureForSigner(e, message, signature, x, y, verifier); assert (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE()); +} + +rule getSignerRevertingConditions { + env e; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + bool triedTransferringEth = e.msg.value != 0; + + getSigner@withrevert(e, x, y, verifiers); + + assert lastReverted <=> triedTransferringEth; +} + +rule createSignerRevertingConditions { + env e; + uint256 x; + uint256 y; + P256.Verifiers verifiers; + + address signer = getSigner(e, x, y, verifiers); + bool signerHasNoCode = hasNoCode(signer); + + bool triedTransferringEth = e.msg.value != 0; + + createSigner@withrevert(e, x, y, verifiers); + + bool notCreatedSigner = signerHasNoCode && (createdAddress != signer); + + assert lastReverted <=> (triedTransferringEth || notCreatedSigner); } \ No newline at end of file diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec index c6bcfed38..07b61934f 100644 --- a/certora/specs/SafeWebAuthnSignerSingleton.spec +++ b/certora/specs/SafeWebAuthnSignerSingleton.spec @@ -121,3 +121,18 @@ rule verifyIsValidSignatureWillContinueToSucceed(){ assert (!firstReverted && !secondRevert) => (firstVerified == secondVerify); satisfy true; } + +rule isValidSignatureRevertingConditions { + env e; + bytes32 message; + + WebAuthn.Signature sigStruct; + bytes signature = WebAuthnHarness.encodeSignature(e, sigStruct); + + bool triedTransferringEth = e.msg.value != 0; + bool dataLengthInsufficient = sigStruct.authenticatorData.length <= 32; + + isValidSignature@withrevert(e, message, signature); + + assert lastReverted <=> (triedTransferringEth || dataLengthInsufficient); +} \ No newline at end of file From c81f4a6fd1b45014eb90679fedc1288b98335d66 Mon Sep 17 00:00:00 2001 From: liav-certora Date: Sun, 9 Jun 2024 10:53:04 +0300 Subject: [PATCH 2/3] Update SafeWebAuthnSignerSingleton.conf --- certora/confs/SafeWebAuthnSignerSingleton.conf | 3 --- 1 file changed, 3 deletions(-) diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf index 6ffa1786d..cb5d77137 100644 --- a/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/certora/confs/SafeWebAuthnSignerSingleton.conf @@ -7,9 +7,6 @@ "modules/passkey/contracts/libraries/P256.sol", "certora/harnesses/WebAuthnHarness.sol", ], - "java_args": [ - " -ea -Dlevel.setup.helpers=info" - ], "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" From d208c5a331fe43a58392b935b955999e325d6e87 Mon Sep 17 00:00:00 2001 From: liav-certora Date: Sun, 9 Jun 2024 12:04:14 +0300 Subject: [PATCH 3/3] Update SafeWebAuthnSignerFactory.spec --- certora/specs/SafeWebAuthnSignerFactory.spec | 20 -------------------- 1 file changed, 20 deletions(-) diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec index 2528c52b1..e93587d9e 100644 --- a/certora/specs/SafeWebAuthnSignerFactory.spec +++ b/certora/specs/SafeWebAuthnSignerFactory.spec @@ -104,7 +104,6 @@ rule deterministicSigner() ghost mathint numOfCreation; ghost mapping(address => uint) address_map; -ghost address createdAddress; ghost bool validValue; hook EXTCODESIZE(address addr) uint v { @@ -115,7 +114,6 @@ hook EXTCODESIZE(address addr) uint v { hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v { numOfCreation = numOfCreation + 1; address_map[v] = length; - createdAddress = v; } rule SignerCreationCantOverride() @@ -225,21 +223,3 @@ rule getSignerRevertingConditions { assert lastReverted <=> triedTransferringEth; } - -rule createSignerRevertingConditions { - env e; - uint256 x; - uint256 y; - P256.Verifiers verifiers; - - address signer = getSigner(e, x, y, verifiers); - bool signerHasNoCode = hasNoCode(signer); - - bool triedTransferringEth = e.msg.value != 0; - - createSigner@withrevert(e, x, y, verifiers); - - bool notCreatedSigner = signerHasNoCode && (createdAddress != signer); - - assert lastReverted <=> (triedTransferringEth || notCreatedSigner); -} \ No newline at end of file