From 051e1547cfb31dd475a49edbf2034d728ec251dc Mon Sep 17 00:00:00 2001
From: niv vaknin <niv@certora.com>
Date: Thu, 6 Jun 2024 18:21:07 +0300
Subject: [PATCH] Add missing rules

---
 certora/specs/SafeWebAuthnSignerFactory.spec | 101 +++++++++++++++++++
 certora/specs/WebAuthn.spec                  |  21 ++++
 2 files changed, 122 insertions(+)

diff --git a/certora/specs/SafeWebAuthnSignerFactory.spec b/certora/specs/SafeWebAuthnSignerFactory.spec
index 1444edcaf..b9d5dc833 100644
--- a/certora/specs/SafeWebAuthnSignerFactory.spec
+++ b/certora/specs/SafeWebAuthnSignerFactory.spec
@@ -57,6 +57,61 @@ rule createAndGetSignerEquivalence(){
     assert signer1 == signer2 <=> (createX == getX && createY == getY && createVerifier == getVerifier);
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Deterministic address in get signer (Proved)                                                                        │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule deterministicSigner()
+{
+    env e1;
+    env e2;
+
+    uint x;
+    uint y;
+    P256.Verifiers verifier;
+
+    address signer = getSigner(e1, x, y, verifier);
+
+    assert signer == getSigner(e2, x, y, verifier);
+}
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ Correctness of Signer Creation. (Cant called twice and override) (Bug CERT-6252)                                           │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+ghost mathint numOfCreation;
+ghost mapping(address => uint) address_map;
+
+hook EXTCODESIZE(address addr) uint v{
+    require address_map[addr] == v;
+}
+
+hook CREATE2(uint value, uint offset, uint length, bytes32 salt) address v{
+    numOfCreation = numOfCreation + 1;
+    address_map[v] = length;
+}
+
+rule SignerCreationCantOverride()
+{
+    env e;
+    require numOfCreation == 0;
+
+    uint x;
+    uint y;
+    P256.Verifiers verifier;
+
+    address a = getSigner(e, x, y, verifier);
+    require address_map[a] == 0;
+
+    createSigner(e, x, y, verifier);
+    createSigner@withrevert(e, x, y, verifier);
+
+    assert numOfCreation < 2;
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ Has no code integrity  (Proved)                                                                                     │
@@ -68,6 +123,30 @@ rule hasNoCodeIntegrity()
     assert (a == proxy) => !hasNoCode(a);
 }
 
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ isValidSignatureForSigner equiv to first deploying the signer with the factory, and then                            |
+|     verifying the signature with it directly (CERT-6221)                                                            │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule createAndVerifyEQtoIsValidSignatureForSigner()
+{
+    env e;
+    uint x;
+    uint y;
+    P256.Verifiers verifier;
+    bytes signature;
+    bytes32 message;
+
+    storage s = lastStorage;
+
+    bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier);
+
+    bytes4 magic2 = createAndVerify(e, message, signature, x, y, verifier) at s;
+
+    assert magic1 == magic2;
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ isValidSignatureForSigner Consistency (Proved)                                                                        │
@@ -101,4 +180,26 @@ rule isValidSignatureForSignerConsistency()
 
     assert firstRevert == secondRevert;
     assert (!firstRevert && !secondRevert) => (magic1 == MAGIC_VALUE()) <=> (magic2 == MAGIC_VALUE());
+}
+
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ isValidSignatureForSigner Integrity (Violated)                                                                      │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+
+rule isValidSignatureForSignerIntegrity()
+{
+    env e;
+
+    uint x;
+    uint y;
+    P256.Verifiers verifier;
+    bytes signature;
+    bytes32 message;
+
+    bytes4 magic1 = isValidSignatureForSigner(e, message, signature, x, y, verifier);
+    
+    satisfy magic1 == MAGIC_VALUE();
 }
\ No newline at end of file
diff --git a/certora/specs/WebAuthn.spec b/certora/specs/WebAuthn.spec
index f59e6818a..4f394a3aa 100644
--- a/certora/specs/WebAuthn.spec
+++ b/certora/specs/WebAuthn.spec
@@ -44,6 +44,27 @@ rule shaIntegrity(){
     assert (keccak256(input1) != keccak256(input2)) <=> input1_sha != input2_sha;
 }
 
+
+/*
+┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
+│ every 2 challenges results in unique message when using encodeSigningMessage (Timeout cert-6290)                    │
+└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
+*/
+rule uniqueMessagePerChallenge(){
+    env e;
+
+    bytes32 challenge1;
+    bytes32 challenge2;
+    bytes authenticatorData;
+    require authenticatorData.length % 32 == 0;
+    string clientDataField;
+
+    bytes message1 = encodeSigningMessage(e, challenge1, authenticatorData, clientDataField);
+    bytes message2 = encodeSigningMessage(e, challenge2, authenticatorData, clientDataField);
+
+    assert (challenge1 != challenge2) <=> (getSha256(e, message1) != getSha256(e, message2));
+}
+
 /*
 ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
 │ verifySignature functions are equivalent (Proved)                                                                   │