From d71c9a851f9b2ad760d51ff419e25b322904a300 Mon Sep 17 00:00:00 2001 From: niv vaknin Date: Wed, 15 May 2024 18:59:34 +0300 Subject: [PATCH] Add property list --- certora/properties.txt | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/certora/properties.txt b/certora/properties.txt index aa4abb442..3a1a7d116 100644 --- a/certora/properties.txt +++ b/certora/properties.txt @@ -8,4 +8,14 @@ 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) \ No newline at end of file +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. Singleton - Implementation of _verifySignature Function (Integrity) +16. Singleton - getConfiguration Function (Integrity) +17. WebAuthn - castSignature Integrity +18. WebAuthn - encodeClientDataJson Integrity +19. WebAuthn - encodeSigningMessage Integrity +20. WebAuthn - verifySignature Integrity \ No newline at end of file