From 4714c04967ed98b712af206ae8d99edfd0b1a38d Mon Sep 17 00:00:00 2001 From: yoavelmalem Date: Mon, 20 May 2024 17:51:14 +0300 Subject: [PATCH] Added all properties. getConfiguration Integrity not done yet. --- .../confs/SafeWebAuthnSignerSingleton.conf | 8 +- .../specs/SafeWebAuthnSignerSingleton.spec | 157 +++++++++++++++--- 2 files changed, 138 insertions(+), 27 deletions(-) diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf index b43b06da5..ccea556a2 100644 --- a/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/certora/confs/SafeWebAuthnSignerSingleton.conf @@ -1,14 +1,14 @@ { "assert_autofinder_success": true, "files": [ + "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", - "certora/harnesses/ERC20Like/DummyWeth.sol", - "certora/harnesses/Utilities.sol", + "certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol", ], "java_args": [ " -ea -Dlevel.setup.helpers=info" ], - "msg": "sanity_with_all_default_summaries", + "msg": "", "process": "emv", "prover_args": [ " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on" @@ -23,5 +23,5 @@ "optimistic_hashing": true, "prover_version": "master", "server": "production", - "verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec" + "verify": "SafeWebAuthnSignerSingletonHarness:certora/specs/SafeWebAuthnSignerSingleton.spec" } \ No newline at end of file diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec index 938aba94a..6f71beea0 100644 --- a/certora/specs/SafeWebAuthnSignerSingleton.spec +++ b/certora/specs/SafeWebAuthnSignerSingleton.spec @@ -1,23 +1,134 @@ -import "ERC20/erc20cvl.spec"; -import "ERC20/WETHcvl.spec"; -import "ERC721/erc721.spec"; -import "ERC1967/erc1967.spec"; -import "PriceAggregators/chainlink.spec"; -import "PriceAggregators/tellor.spec"; - -import "spec_utils/problems.spec"; -import "spec_utils/unresolved.spec"; -import "spec_utils/optimizations.spec"; - -import "spec_utils/generic.spec"; // pick additional rules from here - -use builtin rule sanity filtered { f -> f.contract == currentContract } - -use builtin rule hasDelegateCalls filtered { f -> f.contract == currentContract } -use builtin rule msgValueInLoopRule; -use builtin rule viewReentrancy; -use rule privilegedOperation filtered { f -> f.contract == currentContract } -use rule timeoutChecker filtered { f -> f.contract == currentContract } -use rule simpleFrontRunning filtered { f -> f.contract == currentContract } -use rule noRevert filtered { f -> f.contract == currentContract } -use rule alwaysRevert filtered { f -> f.contract == currentContract } \ No newline at end of file +// import "ERC20/erc20cvl.spec"; +// import "ERC20/WETHcvl.spec"; +// import "ERC721/erc721.spec"; +// import "ERC1967/erc1967.spec"; +// import "PriceAggregators/chainlink.spec"; +// import "PriceAggregators/tellor.spec"; + +// import "spec_utils/problems.spec"; +// import "spec_utils/unresolved.spec"; +// import "spec_utils/optimizations.spec"; + +// import "spec_utils/generic.spec"; // pick additional rules from here + +// use builtin rule sanity filtered { f -> f.contract == currentContract } + +// use builtin rule hasDelegateCalls filtered { f -> f.contract == currentContract } +// use builtin rule msgValueInLoopRule; +// use builtin rule viewReentrancy; +// use rule privilegedOperation filtered { f -> f.contract == currentContract } +// use rule timeoutChecker filtered { f -> f.contract == currentContract } +// use rule simpleFrontRunning filtered { f -> f.contract == currentContract } +// use rule noRevert filtered { f -> f.contract == currentContract } +// use rule alwaysRevert filtered { f -> f.contract == currentContract } + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Implementation of _verifySignature Function (Integrity) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifySignatureIntegrity(env e){ + bytes32 first_message; + bytes signature; + + bool first_message_verified = verifySignatureHarnessed(e, first_message, signature); + + bytes32 second_message; + bool second_message_verified = verifySignatureHarnessed(e, second_message, signature); + + assert (first_message_verified == true && second_message_verified == true) => first_message == second_message; + assert first_message == second_message => first_message_verified == second_message_verified; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ getConfiguration Function (Integrity) │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +// TODO Not Completed Yet +// rule verifyGetConfigurationIntegrity(env e){ + +// uint256 x; +// uint256 y; +// P256.Verifiers verifiers; +// uint256 new_x; uint256 new_y; P256.Verifiers new_verifiers; +// bytes32 message; + +// // bytes data = assignValues(e, x, y, verifiers); +// (new_x, new_y, new_verifiers) = temp(e, x, y, verifiers); + +// // (x, y, verifiers) = getConfiguration(e); +// // (new_x, new_y, new_verifiers) = getConfigurationHarnessed(e, data); + +// assert x == new_x; +// assert y == new_y; +// assert verifiers == new_verifiers; +// satisfy true; +// } + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Both is valid Signature behave the same way │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifyIsValidSignatureAreEqual(env e){ + bytes data; + bytes first_signature; + + bool hashed_data_verified = verifySignatureHarnessed(e, keccak256(data), first_signature); + + bytes second_signature; + bytes32 message; + bool message_verified = verifySignatureHarnessed(e, message, second_signature); + + assert (hashed_data_verified == true && message_verified == true) => message == keccak256(data); + assert message == keccak256(data) => hashed_data_verified == message_verified; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Once signer passed isValidSignature it will never fail on it after any call │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule verifyIsValidSignatureWillContinueToSucceed(env e){ + bytes32 message; + bytes signature; + + bool first_verified = verifySignatureHarnessed(e, message, signature); + require first_verified == true; + + bool second_verified = verifySignatureHarnessed(e, message, signature); + assert second_verified; +} + + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Once isValidSignature failed, it will never pass before createSigner called │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ + +rule IsValidSignatureMustSucceedAfterCreation(env e){ + method f; + calldataarg args; + + bytes32 message; + bytes signature; + + bool first_verified = verifySignatureHarnessed(e, message, signature); + require !first_verified; + + f(e, args); + + + bool second_verified = verifySignatureHarnessed(e, message, signature); + assert second_verified => f.selector == sig:SafeWebAuthnSignerFactory.createSigner(uint256, uint256, P256.Verifiers).selector; +} +