diff --git a/certora/confs/SafeWebAuthnSignerSingleton.conf b/certora/confs/SafeWebAuthnSignerSingleton.conf index ccea556a2..e9ce50e04 100644 --- a/certora/confs/SafeWebAuthnSignerSingleton.conf +++ b/certora/confs/SafeWebAuthnSignerSingleton.conf @@ -2,8 +2,13 @@ "assert_autofinder_success": true, "files": [ "modules/passkey/contracts/SafeWebAuthnSignerFactory.sol", + "modules/passkey/contracts/SafeWebAuthnSignerProxy.sol", "modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol", + "modules/passkey/contracts/libraries/WebAuthn.sol", + "modules/passkey/contracts/libraries/P256.sol", + "modules/passkey/contracts/libraries/ERC1271.sol", "certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol", + "certora/harnesses/WebAuthnHarness.sol", ], "java_args": [ " -ea -Dlevel.setup.helpers=info" @@ -12,14 +17,17 @@ "process": "emv", "prover_args": [ " -verifyCache -verifyTACDumps -testMode -checkRuleDigest -callTraceHardFail on" + //" -useBitVectorTheory" ], "packages":[ "@safe-global=node_modules/@safe-global", "@account-abstraction=node_modules/@account-abstraction" ], "solc": "solc8.23", + "rule_sanity": "basic", "solc_via_ir": false, "optimistic_loop": true, + "loop_iter": "6", "optimistic_hashing": true, "prover_version": "master", "server": "production", diff --git a/certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol b/certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol index b47960248..cddb033e0 100644 --- a/certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol +++ b/certora/harnesses/SafeWebAuthnSignerSingletonHarness.sol @@ -19,4 +19,8 @@ contract SafeWebAuthnSignerSingletonHarness is SafeWebAuthnSignerSingleton { (uint256 x, uint256 y, P256.Verifiers verifiers) = getConfiguration(); success = WebAuthn.verifySignature(message, signature, WebAuthn.USER_VERIFICATION, x, y, verifiers); } + + function getConfigurationHarnessed(bytes32 message, bytes calldata signature) public pure returns (uint256 new_x, uint256 new_y, P256.Verifiers new_verifiers) { + (uint256 new_x, uint256 new_y, P256.Verifiers new_verifiers) = getConfiguration(); + } } diff --git a/certora/harnesses/WebAuthnHarness.sol b/certora/harnesses/WebAuthnHarness.sol index e56c8430c..a343eb3bf 100644 --- a/certora/harnesses/WebAuthnHarness.sol +++ b/certora/harnesses/WebAuthnHarness.sol @@ -89,5 +89,22 @@ contract WebAuthnHarness { function getSha256(bytes memory input) public view returns (bytes32 digest) { return WebAuthn._sha256(input); } + + mapping (bytes32 => mapping (bytes32 => mapping (bytes32 => bytes))) symbolicMessageSummary; + + function GETencodeSigningMessageSummary(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) public returns (bytes memory){ + bytes32 hashed_authenticatorData = keccak256(authenticatorData); + bytes32 hashed_clientDataFields = keccak256(abi.encodePacked(clientDataFields)); + + bytes memory bytes_mapping = symbolicMessageSummary[challenge][hashed_authenticatorData][hashed_clientDataFields]; + + require (checkInjective(challenge, hashed_authenticatorData, hashed_clientDataFields, keccak256(bytes_mapping))); + + return bytes_mapping; + } + + function checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal view returns (bool){ + return true; + } } diff --git a/certora/specs/SafeWebAuthnSignerSingleton.spec b/certora/specs/SafeWebAuthnSignerSingleton.spec index 54cb25549..f6192e82e 100644 --- a/certora/specs/SafeWebAuthnSignerSingleton.spec +++ b/certora/specs/SafeWebAuthnSignerSingleton.spec @@ -1,3 +1,33 @@ +using SafeWebAuthnSignerProxy as proxy; +using WebAuthnHarness as WebAuthnHarness; + +methods { + function P256.verifySignatureAllowMalleability(P256.Verifiers a, bytes32 b, uint256 c, uint256 d, uint256 e, uint256 f) internal returns (bool) => + verifySignatureAllowMalleabilityGhost(a, b, c, d, e, f); + + function WebAuthn.encodeSigningMessage(bytes32 challenge, bytes calldata authenticatorData, string calldata clientDataFields) internal returns (bytes memory) => + GETencodeSigningMessageCVL(challenge, authenticatorData, clientDataFields); + + function WebAuthnHarness.checkInjective(bytes32 challenge, bytes32 authenticatorData, bytes32 clientDataFields, bytes32 result) internal returns (bool) => + checkInjectiveSummary(challenge, authenticatorData, clientDataFields, result); +} + +function GETencodeSigningMessageCVL(bytes32 challenge, bytes authenticatorData, string clientDataFields) returns bytes +{ + env e; + return WebAuthnHarness.GETencodeSigningMessageSummary(e, challenge, authenticatorData, clientDataFields); +} + +ghost checkInjectiveSummary(bytes32, bytes32, bytes32, bytes32) returns bool { + axiom forall bytes32 x1. forall bytes32 y1. forall bytes32 z1. forall bytes32 x2. forall bytes32 y2. forall bytes32 z2. forall bytes32 result. + checkInjectiveSummary(x1, y1, z1, result) && checkInjectiveSummary(x2, y2, z2, result) => x1 == x2; +} + +ghost verifySignatureAllowMalleabilityGhost(P256.Verifiers, bytes32, uint256, uint256, uint256, uint256) returns bool { + axiom forall P256.Verifiers a. forall bytes32 message1. forall bytes32 message2. forall uint256 c. forall uint256 d. forall uint256 e. forall uint256 f. + verifySignatureAllowMalleabilityGhost(a, message1, c, d, e, f) && + verifySignatureAllowMalleabilityGhost(a, message2, c, d, e, f) => message1 == message2; +} /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -5,39 +35,52 @@ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule verifySignatureIntegrity(env e){ +rule verifySignatureUniqueness(env e){ bytes32 first_message; + bytes32 second_message; bytes signature; + require (first_message != second_message); + bool first_message_verified = verifySignatureHarnessed(e, first_message, signature); + bool second_message_verified = verifySignatureHarnessed(e, second_message, signature); + + assert !(first_message_verified && second_message_verified); +} +rule verifySignatureIntegrity(env e){ + bytes32 first_message; bytes32 second_message; + bytes signature; + + bool first_message_verified = verifySignatureHarnessed(e, first_message, signature); + require (first_message_verified); + 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; + assert second_message_verified <=> first_message == second_message; } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ getConfiguration Function (Integrity) │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ + // TODO Not Completed Yet // rule verifyGetConfigurationIntegrity(env e){ +// bytes32 data; +// bytes first_signature; // 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); +// x = proxy.getX(); +// y = proxy.getY(); +// verifiers = proxy.getVerifiers(); +// (new_x, new_y, new_verifiers) = proxy.getConfiguration(e); // assert x == new_x; // assert y == new_y; @@ -45,7 +88,6 @@ rule verifySignatureIntegrity(env e){ // satisfy true; // } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Both is valid Signature behave the same way │ @@ -56,17 +98,16 @@ rule verifyIsValidSignatureAreEqual(env e){ bytes data; bytes first_signature; - bool hashed_data_verified = verifySignatureHarnessed(e, keccak256(data), first_signature); + bytes4 magicValue_hashed = isValidSignature(e, data, first_signature); - bytes second_signature; bytes32 message; - bool message_verified = verifySignatureHarnessed(e, message, second_signature); + bytes4 magicValue_message = isValidSignature(e, message, first_signature); - assert (hashed_data_verified == true && message_verified == true) => message == keccak256(data); - assert message == keccak256(data) => hashed_data_verified == message_verified; + assert (magicValue_hashed == to_bytes4(0x20c13b0b) && magicValue_message == to_bytes4(0x1626ba7e)) => message == keccak256(data); + assert message == keccak256(data) => (magicValue_hashed == to_bytes4(0x20c13b0b) && magicValue_message == to_bytes4(0x1626ba7e)) || + (magicValue_hashed != to_bytes4(0x20c13b0b) && magicValue_message != to_bytes4(0x1626ba7e)); } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Once signer passed isValidSignature it will never fail on it after any call │ @@ -74,24 +115,27 @@ rule verifyIsValidSignatureAreEqual(env e){ */ rule verifyIsValidSignatureWillContinueToSucceed(env e){ + method f; + calldataarg args; bytes32 message; bytes signature; bool first_verified = verifySignatureHarnessed(e, message, signature); require first_verified == true; + f(e, args); + bool second_verified = verifySignatureHarnessed(e, message, signature); assert second_verified; } - /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ │ Once isValidSignature failed, it will never pass before createSigner called │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -rule IsValidSignatureMustSucceedAfterCreation(env e){ +rule IsValidSignatureWillSucceedOnlyAfterCreation(env e){ method f; calldataarg args; @@ -103,8 +147,6 @@ rule IsValidSignatureMustSucceedAfterCreation(env e){ f(e, args); - bool second_verified = verifySignatureHarnessed(e, message, signature); assert second_verified => f.selector == sig:SafeWebAuthnSignerFactory.createSigner(uint256, uint256, P256.Verifiers).selector; } -