Updated properties and priorities.

certora/properties.txt

@@ -1,30 +1,33 @@
-1.  Factory - isValidSignaure will return the same as create signer
-2.	Integrity for Proxy <- this is not a standard implementation
-3.	WebAuthn - encodeSigningMessage compute presage which needs to get hashed
-		Given data should be able to to produce only 1 valid message.
-4.  Factory - Immutability of Singleton Contract.
-5.  Factory - getSigner is unique for every x,y and verifier combination (need to make sure it is required)
-6.  Factory - createSigner and getSigner always returns the same address.
-7.  Factory - Deterministic Address Calculation for Signers.
-8.  Factory - Correctness of Signer Creation. (Cant called twice, override)
-9.  Factory - Signature Validation (isValidSignatureForSigner Integrity)
-10. Factory - Code Presence Check (_hasNoCode Integrity)
-11. Proxy   - Immutability of Configuration Parameters (x, y, Singleton, verifier)
-12. Proxy   - Delegate Call Integrity (calls the _verifySignature implementation in the Singleton)
-13. Proxy   - Fallback data corruption (uses data appending that needed to be verified)
-14. Proxy   - verify return data from Delegatecall.
-15. Proxy - No buffer overflow when appending Parameters. //(Maybe for Dravee)
-15. Singleton - Implementation of _verifySignature Function (Integrity)
-16. Singleton - getConfiguration Function (Integrity).
-17. Singleton - Both is valid Signature behave the same way.
-19. Singleton - Once signer passed is isValidSignaure it will never fail on it after any call.
-20. WebAuthn - castSignature Integrity
-21. WebAuthn - encodeClientDataJson Integrity
-22. WebAuthn - encodeSigningMessage Integrity
-23. WebAuthn - verifySignature Integrity
-24. WebAuthn - Both verifySignature behave the same way.
-25. DDOS on verifySignature.
+1.  Factory   - isValidSignatureForSigner() should return the same result as createSigner()						[Duplication]
+2.	Proxy     - Integrity, this is not a standard implementation												[Duplication]
+4.  Factory   - Immutability of Singleton Contract.																[Critical]
+5.  Factory   - getSigner is unique for every x,y and verifier combination (need to make sure it is required)	[High]
+6.  Factory   - createSigner and getSigner always returns the same address.										[Medium]
+7.  Factory   - Deterministic Address Calculation for Signers.													[High]
+8.  Factory   - Correctness of Signer Creation. (Cant called twice, override)									[Cannot understand the risk]
+9.  Factory   - Signature Validation (isValidSignatureForSigner Integrity)										[Critical]
+10. Factory   - Code Presence Check (_hasNoCode Integrity)														[Deprecated - internal code]
+11. Proxy     - Immutability of Configuration Parameters (x, y, Singleton, verifier)							[Critical]
+12. Proxy     - Delegate Call Integrity (calls the _verifySignature implementation in the Singleton)			[Low]
+13. Proxy     - Fallback data corruption (uses data appending that needed to be verified)						[Low]
+14. Proxy     - verify return data from Delegate call.															[Low]
+15. Proxy     - No buffer overflow when appending Parameters. //(Maybe for Dravee)								[Low]
+15. Singleton - Implementation of _verifySignature Function (Integrity)											[High/Medium]
+16. Singleton - getConfiguration Function (Integrity).															[High/Medium]
+17. Singleton - Both is valid Signature behave the same way.													[Low]
+19. Singleton - Once signer passed isValidSignature it will never fail on it after any call.					[Low]
+20. Singleton - Once isValidSignature failed, it will never pass before createSigner called.					[High]
+21. WebAuthn  - castSignature Integrity																			[Low/Medium]
+22. WebAuthn  - encodeClientDataJson Integrity																	[Medium]
+23. WebAuthn  - encodeSigningMessage Integrity																	[Medium]
+24. WebAuthn  - verifySignature Integrity																		[Medium]
+25. WebAuthn  - Both verifySignature behave the same way.														[Low]
+3.	WebAuthn  - given input in encodeSigningMessage(), one should produce only one valid output.				[Medium - Maybe duplication]	
+		i.e., one cannot reuse a signature valid for one challenge to be valid for another challenge			
 
 // Optional
-Checks for Revert condition on critical Functions (isValidSignaure,
- verifySignature, Proxy Fallback, createSigner, getSigner)
+Checks for Revert condition on critical Functions (isValidSignature,
+ verifySignature, Proxy Fallback, createSigner, getSigner)			 											[Low]
+
+ // Open Question for Dravee:
+	What is the user protection against hacks?