Skip to content

Commit

Permalink
Squashed commit of the following:
Browse files Browse the repository at this point in the history 
commit a1eab8a
Author: Hristo Grigorov <[email protected]>
Date:   Thu Sep 12 22:35:09 2024 +0300

    WebAuthnHarness to WebAuthnHarnessWithMunge fix

commit 0862df2
Merge: 7f56a64 4616e1d
Author: hristo-grigorov <[email protected]>
Date:   Wed Sep 11 17:19:02 2024 +0300

    Merge pull request #22 from Certora/Yoav_Safe_For_Delivery

    restore private to public munge of modules/passkey/contracts/librarie…

commit 4616e1d
Author: hristo <[email protected]>
Date:   Wed Sep 11 17:13:00 2024 +0300

    restore private to public munge of modules/passkey/contracts/libraries/WebAuthn.sol

commit 7f56a64
Merge: 6df348c 3c7c57b
Author: yoav-el-certora <[email protected]>
Date:   Wed Aug 28 16:03:54 2024 +0300

    Merge pull request #19 from Certora/Yoav_Safe_For_Delivery

    Yoav safe for delivery

commit 3c7c57b
Merge: 9fa6a17 7de765d
Author: yoav-el-certora <[email protected]>
Date:   Wed Aug 28 16:03:36 2024 +0300

    Merge pull request #21 from Certora/Yoav_Work_On_createAndVerifyEQtoIsValidSignatureForSigner

    Add munge

commit 7de765d
Author: yoavelmalem <[email protected]>
Date:   Wed Aug 28 16:01:54 2024 +0300

    Add munge

commit 9fa6a17
Merge: 161d059 78e74a1
Author: yoav-el-certora <[email protected]>
Date:   Wed Aug 28 09:58:10 2024 +0300

    Merge pull request #20 from Certora/Yoav_Work_On_createAndVerifyEQtoIsValidSignatureForSigner

    Add munge

commit 78e74a1
Author: yoavelmalem <[email protected]>
Date:   Tue Aug 27 18:43:17 2024 +0300

    Add munge

commit 91fce2c
Author: yoavelmalem <[email protected]>
Date:   Tue Aug 27 18:26:00 2024 +0300

    Add munge

commit b8427fc
Author: yoavelmalem <[email protected]>
Date:   Tue Aug 27 16:38:27 2024 +0300

    Add munge

commit 161d059
Author: yoavelmalem <[email protected]>
Date:   Thu Aug 22 14:58:59 2024 +0300

    Last fixes

commit 62742d0
Author: yoavelmalem <[email protected]>
Date:   Thu Aug 22 11:26:37 2024 +0300

    Added conf files and fixed all issues

commit 6df348c
Merge: 95be4cc d4a9be6
Author: yoav-el-certora <[email protected]>
Date:   Wed Aug 21 12:37:19 2024 +0300

    Merge pull request #14 from Certora/niv/Add-ALL-Rules

    Niv/add all rules

commit d4a9be6
Author: niv vaknin <[email protected]>
Date:   Wed Aug 21 12:36:20 2024 +0300

    Add john fixes

commit 2299bce
Merge: 9747600 95be4cc
Author: niv vaknin <[email protected]>
Date:   Wed Aug 21 12:31:52 2024 +0300

    Merge branch 'certora' of github.com:Certora/safe-modules into niv/Add-ALL-Rules

commit 9747600
Merge: 3d670eb d96881d
Author: yoav-el-certora <[email protected]>
Date:   Wed Aug 21 12:02:53 2024 +0300

    Merge pull request #18 from Certora/yoav/Singleton_GetConfiguration

    Yoav/singleton get configuration

commit d96881d
Author: yoavelmalem <[email protected]>
Date:   Wed Aug 21 12:02:07 2024 +0300

    remove john branch

commit 767bfcc
Author: yoavelmalem <[email protected]>
Date:   Wed Aug 21 11:47:12 2024 +0300

    remove munging

commit 95be4cc
Merge: e6f8e21 a05a177
Author: yoav-el-certora <[email protected]>
Date:   Sun Jun 23 16:24:55 2024 +0300

    Merge pull request #16 from Certora/yoav/Singleton

    Yoav/singleton

commit a05a177
Merge: e81f28b e6f8e21
Author: yoav-el-certora <[email protected]>
Date:   Sun Jun 23 11:46:22 2024 +0300

    Merge branch 'certora' into yoav/Singleton

commit 99c9c6c
Author: yoavelmalem <[email protected]>
Date:   Sun Jun 23 11:39:42 2024 +0300

    Added getConfiguration Rule

commit e81f28b
Author: yoavelmalem <[email protected]>
Date:   Sun Jun 23 11:38:32 2024 +0300

    Some small changes and verifyIsValidSignatureWillContinueToSucceed working

commit 3d670eb
Author: niv vaknin <[email protected]>
Date:   Wed Jun 19 09:52:56 2024 +0300

    Fix isValidSignerVerifyFor signure

commit 3b5bfd2
Author: niv vaknin <[email protected]>
Date:   Tue Jun 18 09:28:13 2024 +0300

    Update on progress

commit 2568691
Author: niv vaknin <[email protected]>
Date:   Sun Jun 16 12:05:20 2024 +0300

    Add conf with john configuration for createAndVerifyEQtoIsValidSignatureForSigner ruel

commit 306ff0d
Author: niv vaknin <[email protected]>
Date:   Sun Jun 16 10:57:42 2024 +0300

    small fix

commit dd5d83c
Author: niv vaknin <[email protected]>
Date:   Sun Jun 16 10:56:01 2024 +0300

    Add john requirements, proving the rule only for the first time proxy is created.

commit e6f8e21
Author: liav-certora <[email protected]>
Date:   Thu Jun 13 19:30:48 2024 +0300

    .

commit 37050dd
Author: liav-certora <[email protected]>
Date:   Thu Jun 13 17:05:16 2024 +0300

    proxy duplicate

commit ed1bf4d
Author: liav-certora <[email protected]>
Date:   Thu Jun 13 16:58:38 2024 +0300

    cleanup

commit 321c050
Author: niv vaknin <[email protected]>
Date:   Thu Jun 13 11:01:56 2024 +0300

    Try to fix unresolved call to isValidSignature via proxy fallback with dispatch list

commit b50be18
Author: niv vaknin <[email protected]>
Date:   Thu Jun 13 10:57:08 2024 +0300

    Fix

commit aebe38c
Author: niv vaknin <[email protected]>
Date:   Thu Jun 13 10:55:09 2024 +0300

    Add summaries to factory

commit ac7fd70
Merge: 7db212d 08594cc
Author: niv vaknin <[email protected]>
Date:   Thu Jun 13 10:49:29 2024 +0300

    Merge branch 'certora' of github.com:Certora/safe-modules into niv/Add-ALL-Rules

commit 08594cc
Merge: 021d60d dba6d97
Author: liav-certora <[email protected]>
Date:   Tue Jun 11 02:02:33 2024 +0300

    Merge pull request #15 from Certora/liav/more-reverting-conditions

    Liav/more reverting conditions

commit dba6d97
Merge: d208c5a 021d60d
Author: liav-certora <[email protected]>
Date:   Tue Jun 11 02:02:24 2024 +0300

    Merge branch 'certora' into liav/more-reverting-conditions

commit 021d60d
Author: niv vaknin <[email protected]>
Date:   Mon Jun 10 17:27:30 2024 +0300

    Fix proxy return rule at least on john branch

commit d208c5a
Author: liav-certora <[email protected]>
Date:   Sun Jun 9 12:04:14 2024 +0300

    Update SafeWebAuthnSignerFactory.spec

commit c81f4a6
Author: liav-certora <[email protected]>
Date:   Sun Jun 9 10:53:04 2024 +0300

    Update SafeWebAuthnSignerSingleton.conf

commit 7db212d
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 18:22:34 2024 +0300

    Small clean

commit 051e154
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 18:21:07 2024 +0300

    Add missing rules

commit ccab47a
Merge: 741bb38 df3b264
Author: Niv vaknin <[email protected]>
Date:   Thu Jun 6 17:51:56 2024 +0300

    Merge pull request #12 from Certora/niv/snapshot-to-certora

    Niv/snapshot to certora

commit df3b264
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 17:23:34 2024 +0300

    .

commit 8a5a2c7
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 17:15:16 2024 +0300

    move signer rules

commit 2e1aaf7
Author: liav-certora <[email protected]>
Date:   Thu Jun 6 17:05:38 2024 +0300

    .

commit 7cdc8ac
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 16:51:01 2024 +0300

    remove munging

commit dc899e6
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 15:59:00 2024 +0300

    Clean

commit c4ec5eb
Merge: 34450e2 741bb38
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 13:34:54 2024 +0300

    Merge branch 'certora' of github.com:Certora/safe-modules into niv/Fix-Factory-Rules

commit 34450e2
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 13:32:17 2024 +0300

    Add munging remove changes from safe source code

commit 4d3d0f4
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 13:23:21 2024 +0300

    .

commit a9e97ea
Author: niv vaknin <[email protected]>
Date:   Thu Jun 6 12:58:09 2024 +0300

    .

commit 741bb38
Merge: 8e82a69 f56b19c
Author: yoav-el-certora <[email protected]>
Date:   Wed Jun 5 17:26:25 2024 +0300

    Merge pull request #9 from Certora/yoav/Singleton

    Yoav/singleton

commit 7d58f27
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 17:08:51 2024 +0300

    .

commit f56b19c
Author: yoavelmalem <[email protected]>
Date:   Wed Jun 5 16:55:04 2024 +0300

    Removed harness and cleaned both spec and conf file.

commit 80ab0d5
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 16:43:29 2024 +0300

    Organize files

commit d3e5471
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 14:33:42 2024 +0300

    .

commit 10473cf
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 14:31:16 2024 +0300

    .

commit a346a51
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 14:31:02 2024 +0300

    Add verifySignatureConsistent

commit 6e49f86
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 12:44:14 2024 +0300

    Fix castSignatureDeterministicDecoding and castSignatureLengthCheckValidity

commit a43568d
Author: niv vaknin <[email protected]>
Date:   Wed Jun 5 12:02:28 2024 +0300

    Fix verifySignatureEq

commit 3345b5c
Merge: 1523c06 299cd29
Author: yoavelmalem <[email protected]>
Date:   Tue Jun 4 15:51:14 2024 +0300

    Merge remote-tracking branch 'origin/yoav/Singleton' into yoav/Singleton

commit 1523c06
Author: yoavelmalem <[email protected]>
Date:   Tue Jun 4 15:50:50 2024 +0300

    revert verifyIsValidSignatureWillContinueToSucceed changes

commit d668c41
Author: niv vaknin <[email protected]>
Date:   Tue Jun 4 15:35:41 2024 +0300

    Add munging for hasNoCode

commit 299cd29
Merge: bde14d6 8e82a69
Author: yoav-el-certora <[email protected]>
Date:   Tue Jun 4 15:07:42 2024 +0300

    Merge branch 'certora' into yoav/Singleton

commit bde14d6
Author: yoavelmalem <[email protected]>
Date:   Tue Jun 4 15:03:41 2024 +0300

    Addressed Hristo comments

commit 8e82a69
Merge: 6ad4b5e f9251a9
Author: liav-certora <[email protected]>
Date:   Tue Jun 4 11:47:57 2024 +0300

    Merge pull request #10 from Certora/liav/reverting-conditions

    Liav/reverting conditions

commit 80a64da
Author: niv vaknin <[email protected]>
Date:   Tue Jun 4 11:42:56 2024 +0300

    Add summary for getsiner

commit 6ba6742
Author: niv vaknin <[email protected]>
Date:   Tue Jun 4 11:42:18 2024 +0300

    Add summary for getsiner

commit 6a21c3f
Author: niv vaknin <[email protected]>
Date:   Tue Jun 4 11:40:31 2024 +0300

    Fix uniqueSigner and createAndGetSignerEquivalence rules

commit 3983d89
Author: yoavelmalem <[email protected]>
Date:   Mon Jun 3 11:39:10 2024 +0300

    Small updates and improved castSignatureLengthCheckValidity condition

commit f9251a9
Author: liav-certora <[email protected]>
Date:   Thu May 30 19:50:51 2024 +0300

    .

commit 82cecef
Author: yoavelmalem <[email protected]>
Date:   Thu May 30 18:03:21 2024 +0300

    Added Jochen suggestion

commit 6c7348e
Author: yoavelmalem <[email protected]>
Date:   Thu May 30 17:40:57 2024 +0300

    Added summaries and additional fixes

commit 6ad4b5e
Merge: 294f1e7 a932fab
Author: liav-certora <[email protected]>
Date:   Thu May 30 00:51:24 2024 +0300

    Merge pull request #8 from Certora/liav/reverting-conditions

    .

commit a932fab
Author: liav-certora <[email protected]>
Date:   Thu May 30 00:49:49 2024 +0300

    .

commit 294f1e7
Merge: a2ef981 76d0729
Author: liav-certora <[email protected]>
Date:   Wed May 29 15:33:46 2024 +0300

    Merge pull request #6 from Certora/liav/property

    Proxy properties

commit a2ef981
Author: niv vaknin <[email protected]>
Date:   Wed May 29 13:47:06 2024 +0300

    Replace cast signature rules

commit 9fa9ac8
Author: niv vaknin <[email protected]>
Date:   Wed May 29 12:39:40 2024 +0300

    Split between BitVector theory conf and regular

commit 8643c6f
Author: niv vaknin <[email protected]>
Date:   Wed May 29 12:28:10 2024 +0300

    Improve consistent rule for cast signature

commit 1a90bed
Author: niv vaknin <[email protected]>
Date:   Wed May 29 12:14:32 2024 +0300

    Remove summary apply bitvector

commit caf2a10
Author: niv vaknin <[email protected]>
Date:   Tue May 28 13:57:30 2024 +0300

    Apply smt suggestion to avoid timeout on Encoding message

commit 34d557b
Author: niv vaknin <[email protected]>
Date:   Tue May 28 13:55:47 2024 +0300

    Fix summary rule is still violated

commit 3a7ecc2
Author: niv vaknin <[email protected]>
Date:   Tue May 28 10:25:49 2024 +0300

    Improve deterministic signer

commit 82aef3a
Author: niv vaknin <[email protected]>
Date:   Mon May 27 19:11:45 2024 +0300

    Cleaning

commit 3e1758f
Author: niv vaknin <[email protected]>
Date:   Mon May 27 18:27:43 2024 +0300

    Fix assert

commit a1aad3b
Merge: dca8c02 bf0ff62
Author: Niv vaknin <[email protected]>
Date:   Mon May 27 17:05:01 2024 +0300

    Merge pull request #7 from Certora/niv/WebAuth

    Add webAuth rules

commit bf0ff62
Author: niv vaknin <[email protected]>
Date:   Mon May 27 17:04:20 2024 +0300

    Add webAuth rules

commit 76d0729
Author: liav-certora <[email protected]>
Date:   Mon May 27 12:58:11 2024 +0300

    Nurit CR

commit dca8c02
Author: niv vaknin <[email protected]>
Date:   Sun May 26 18:22:27 2024 +0300

    Fix rule condition

commit d723451
Merge: 89bd20e fc88173
Author: Niv vaknin <[email protected]>
Date:   Sun May 26 18:17:38 2024 +0300

    Merge pull request #5 from Certora/niv/Factory

    Niv/factory

commit fc88173
Author: niv vaknin <[email protected]>
Date:   Sun May 26 18:17:10 2024 +0300

    Start webauth

commit ba92c5b
Author: liav-certora <[email protected]>
Date:   Sun May 26 18:14:16 2024 +0300

    comments

commit d15faf8
Author: liav-certora <[email protected]>
Date:   Sun May 26 15:50:53 2024 +0300

    more rules

commit 24cf1df
Author: niv vaknin <[email protected]>
Date:   Thu May 23 22:28:06 2024 +0300

    For nurit

commit 761f58b
Author: niv vaknin <[email protected]>
Date:   Thu May 23 14:05:49 2024 +0300

    Add ticket

commit 4ad1bf0
Author: niv vaknin <[email protected]>
Date:   Wed May 22 13:55:18 2024 +0300

    Try to fix

commit 657f413
Author: niv vaknin <[email protected]>
Date:   Wed May 22 11:36:18 2024 +0300

    Try to fix

commit a8f1793
Author: niv vaknin <[email protected]>
Date:   Wed May 22 10:20:07 2024 +0300

    Comment out

commit 9858608
Author: niv vaknin <[email protected]>
Date:   Tue May 21 17:37:59 2024 +0300

    Add sanity basic

commit 6dbea47
Author: niv vaknin <[email protected]>
Date:   Tue May 21 15:57:05 2024 +0300

    Clean munging

commit 8dd8ec3
Author: niv vaknin <[email protected]>
Date:   Tue May 21 15:54:18 2024 +0300

    .

commit 89bd20e
Merge: e5c5e70 db36204
Author: yoav-el-certora <[email protected]>
Date:   Tue May 21 12:08:26 2024 +0300

    Merge pull request #4 from Certora/Singleton_Rules

    Added all properties.

commit db36204
Author: yoavelmalem <[email protected]>
Date:   Tue May 21 12:07:46 2024 +0300

    Removed commented code.

commit 958f508
Author: niv vaknin <[email protected]>
Date:   Tue May 21 11:50:23 2024 +0300

    .

commit c9d1532
Author: yoavelmalem <[email protected]>
Date:   Tue May 21 11:04:45 2024 +0300

    Added the harness file

commit e5c5e70
Merge: 20f659b 66b5fcb
Author: liav-certora <[email protected]>
Date:   Mon May 20 18:56:13 2024 +0300

    Merge pull request #3 from Certora/liav/property

    Proxy Immutability Property

commit 4714c04
Author: yoavelmalem <[email protected]>
Date:   Mon May 20 17:51:14 2024 +0300

    Added all properties.
    getConfiguration Integrity not done yet.

commit 6242d48
Author: niv vaknin <[email protected]>
Date:   Mon May 20 14:33:33 2024 +0300

    .

commit 66b5fcb
Author: liav-certora <[email protected]>
Date:   Mon May 20 11:02:34 2024 +0300

    Update SafeWebAuthnSignerProxy.spec

commit 589a626
Author: liav-certora <[email protected]>
Date:   Sun May 19 16:30:55 2024 +0300

    Update SafeWebAuthnSignerProxy.spec

commit 20f659b
Author: niv vaknin <[email protected]>
Date:   Sun May 19 14:23:20 2024 +0300

    .

commit 64a6083
Author: yoavelmalem <[email protected]>
Date:   Sun May 19 12:48:10 2024 +0300

    Updated properties and priorities.

commit 896c24b
Author: niv vaknin <[email protected]>
Date:   Thu May 16 17:56:02 2024 +0300

    Add property list

commit f50532f
Author: niv vaknin <[email protected]>
Date:   Thu May 16 17:51:56 2024 +0300

    Add property list

commit 39e5159
Author: niv vaknin <[email protected]>
Date:   Thu May 16 17:47:17 2024 +0300

    Add property list

commit 5aa3bac
Author: niv vaknin <[email protected]>
Date:   Thu May 16 17:45:09 2024 +0300

    Add property list

commit f247607
Author: niv vaknin <[email protected]>
Date:   Thu May 16 17:41:25 2024 +0300

    Add property list

commit dc842ad
Author: niv vaknin <[email protected]>
Date:   Thu May 16 16:38:09 2024 +0300

    Add property list

commit d132793
Author: niv vaknin <[email protected]>
Date:   Wed May 15 19:02:09 2024 +0300

    Add property list

commit d71c9a8
Author: niv vaknin <[email protected]>
Date:   Wed May 15 18:59:34 2024 +0300

    Add property list

commit b8989c3
Author: niv vaknin <[email protected]>
Date:   Wed May 15 18:30:25 2024 +0300

    Add property list

commit 26fd77b
Merge: 9545b45 8ba3831
Author: Niv vaknin <[email protected]>
Date:   Wed May 15 14:27:45 2024 +0300

    Merge pull request #2 from Certora/niv/Handle-signer-methods

    Fix sanity using alex parameters

commit 8ba3831
Author: niv vaknin <[email protected]>
Date:   Wed May 15 14:13:54 2024 +0300

    Fix sanity using alex parameters

commit 9545b45
Merge: aca3afc 9488e45
Author: Niv vaknin <[email protected]>
Date:   Wed May 15 13:42:36 2024 +0300

    Merge pull request #1 from Certora/niv/Orgenazie-Files

    Organize project setup files

commit 9488e45
Author: niv vaknin <[email protected]>
Date:   Wed May 15 12:56:09 2024 +0300

    Add webAuthn conf

commit da59212
Author: niv vaknin <[email protected]>
Date:   Wed May 15 11:27:06 2024 +0300

    .

commit aca3afc
Merge: 5ef533b 8a90660
Author: niv vaknin <[email protected]>
Date:   Wed May 15 10:13:15 2024 +0300

    Merge branch 'main' of github.com:Certora/safe-modules into certora

commit 5ef533b
Merge: 7070a09 cedccec
Author: niv vaknin <[email protected]>
Date:   Sun May 12 17:13:06 2024 +0300

    Merge branch 'certora' of github.com:Certora/safe-modules into certora

commit cedccec
Merge: ff3c325 b143b6f
Author: yoav-el-certora <[email protected]>
Date:   Sun May 12 16:55:45 2024 +0300

    Merge branch 'safe-global:main' into certora

commit 7070a09
Merge: ff3c325 b143b6f
Author: niv vaknin <[email protected]>
Date:   Sun May 12 16:15:17 2024 +0300

    Merge branch 'main' of github.com:Certora/safe-modules into certora

commit ff3c325
Author: yoavelmalem <[email protected]>
Date:   Thu May 2 17:28:57 2024 +0300

    Reorganize all folders, Added specific spec file for each contract, Added summarizations.

commit 512eb51
Author: yoavelmalem <[email protected]>
Date:   Thu Apr 25 18:53:49 2024 +0300

    Small fixes

commit e2dca84
Author: yoavelmalem <[email protected]>
Date:   Thu Apr 25 18:17:26 2024 +0300

    Added first batch of setup confs
  • Loading branch information
@remedcu
remedcu committed Sep 20, 2024
1 parent a5aaf8e commit 1be8e52
Show file tree
Hide file tree
Showing 33 changed files with 2,741 additions and 0 deletions.
25 changes: 25 additions & 0 deletions certora/confs/GetConfigurationConf.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,25 @@
{
"assert_autofinder_success": true,
"files": [
"certora/munged/SafeWebAuthnSignerSingleton.sol",
"certora/harnesses/GetConfigurationProxyHarness.sol",
"modules/passkey/contracts/SafeWebAuthnSignerFactory.sol"
],
"link": [
"GetConfigurationProxyHarness:_SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"prover_args": [
" -split false"
],
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "GetConfigurationProxyHarness:certora/specs/GetConfigurationSpec.spec"
}
23 changes: 23 additions & 0 deletions certora/confs/GetSigner.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{
"assert_autofinder_success": true,
"files": [
"certora/harnesses/GetSignerHarness.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
],
"hashing_length_bound": "4694",
"link": [
"GetSignerHarness:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "144",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "GetSignerHarness:certora/specs/GetSigner.spec"
}
27 changes: 27 additions & 0 deletions certora/confs/ProxySimulator.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,27 @@
{
"assert_autofinder_success": true,
"files": [
"certora/harnesses/ProxySimulator.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/libraries/P256.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"hashing_length_bound": "2048",
"link": [
"ProxySimulator:_proxy=SafeWebAuthnSignerProxy",
"SafeWebAuthnSignerProxy:_VERIFIERS=P256",
"SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "ProxySimulator:certora/specs/ProxySimulator.spec"
}
30 changes: 30 additions & 0 deletions certora/confs/SafeWebAuthnSignerFactory.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
{
"assert_autofinder_success": true,
"files": [
"certora/harnesses/FactoryHarnessForSignerConsistency.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
],
"link": [
"FactoryHarnessForSignerConsistency:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"rule": [
"createAndGetSignerEquivalence",
"getSignerRevertingConditions",
"hasNoCodeIntegrity",
"isValidSignatureForSignerConsistency",
"singletonNeverChanges"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "FactoryHarnessForSignerConsistency:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec"
}
23 changes: 23 additions & 0 deletions certora/confs/SafeWebAuthnSignerProxy.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{
"assert_autofinder_success": true,
"files": [
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/libraries/P256.sol"
],
"link": [
"SafeWebAuthnSignerProxy:_VERIFIERS=P256",
"SafeWebAuthnSignerProxy:_SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerProxy:certora/specs/SafeWebAuthnSignerProxy.spec"
}
23 changes: 23 additions & 0 deletions certora/confs/SafeWebAuthnSignerSingleton.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{
"assert_autofinder_success": true,
"files": [
"modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/libraries/P256.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"link": [
"SafeWebAuthnSignerFactory:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec"
}
31 changes: 31 additions & 0 deletions certora/confs/SignerCreationCantOverride.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
{
"assert_autofinder_success": true,
"exclude_rule": [
"createAndVerifyEQtoIsValidSignatureForSigner"
],
"files": [
"certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol",
"modules/passkey/contracts/libraries/P256.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"hashing_length_bound": "912",
"link": [
"SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule": [
"SignerCreationCantOverride"
],
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec"
}
23 changes: 23 additions & 0 deletions certora/confs/SingletonIsValidSignatureRevertingConditions.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{
"assert_autofinder_success": true,
"files": [
"modules/passkey/contracts/SafeWebAuthnSignerFactory.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/libraries/P256.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule": [
"isValidSignatureRevertingConditions"
],
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerSingleton:certora/specs/SafeWebAuthnSignerSingleton.spec"
}
26 changes: 26 additions & 0 deletions certora/confs/ValidSignatureForSignerIntegrity.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
{
"assert_autofinder_success": true,
"files": [
"certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"modules/passkey/contracts/SafeWebAuthnSignerProxy.sol"
],
"link": [
"SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule": [
"isValidSignatureForSignerIntegrity"
],
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactory.spec"
}
33 changes: 33 additions & 0 deletions certora/confs/VerifyEQtoIsValidSignatureForSigner.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,33 @@
{
"assert_autofinder_success": true,
"dynamic_bound": "1",
"files": [
"certora/harnesses/SafeWebAuthnSignerFactoryHarness.sol",
"modules/passkey/contracts/SafeWebAuthnSignerSingleton.sol",
"certora/munged/SafeWebAuthnSignerProxy.sol",
"certora/munged/WebAuthn.sol",
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"hashing_length_bound": "906",
"link": [
"SafeWebAuthnSignerFactoryHarness:SINGLETON=SafeWebAuthnSignerSingleton"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"prover_args": [
"-depth 12"
],
"rule": [
"createAndVerifyEQtoIsValidSignatureForSigner"
],
"rule_sanity": "basic",
"smt_timeout": "600",
"solc": "solc8.23",
"verify": "SafeWebAuthnSignerFactoryHarness:certora/specs/SafeWebAuthnSignerFactoryWithMunge.spec"
}
17 changes: 17 additions & 0 deletions certora/confs/WebAuthn.conf
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,17 @@
{
"assert_autofinder_success": true,
"files": [
"certora/harnesses/WebAuthnHarnessWithMunge.sol"
],
"loop_iter": "6",
"optimistic_hashing": true,
"optimistic_loop": true,
"packages": [
"@safe-global=node_modules/@safe-global",
"@account-abstraction=node_modules/@account-abstraction"
],
"process": "emv",
"rule_sanity": "basic",
"solc": "solc8.23",
"verify": "WebAuthnHarnessWithMunge:certora/specs/WebAuthn.spec"
}
39 changes: 39 additions & 0 deletions certora/harnesses/FactoryHarnessForSignerConsistency.sol
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,39 @@
// SPDX-License-Identifier: LGPL-3.0-only
pragma solidity >=0.8.0;

import {SafeWebAuthnSignerFactory} from "../munged/FactoryForSignerConsistency.sol";
import {P256} from "../../modules/passkey/contracts/libraries/P256.sol";
import {SafeWebAuthnSignerProxy} from "../../modules/passkey/contracts/SafeWebAuthnSignerProxy.sol";

contract FactoryHarnessForSignerConsistency is SafeWebAuthnSignerFactory {

//Harness
function hasNoCode(address account) external view returns (bool result) {
// solhint-disable-next-line no-inline-assembly
return SafeWebAuthnSignerFactory._hasNoCode(account);
}

function createAndVerify(
bytes32 message,
bytes calldata signature,
uint256 x,
uint256 y,
P256.Verifiers verifiers
) external returns (bytes4 magicValue) {
address signer = this.createSigner(x, y, verifiers);

bytes memory data = abi.encodeWithSignature("isValidSignature(bytes32,bytes)", message, signature);

// Use low-level call to invoke isValidSignature on the signer address
(bool success, bytes memory result) = signer.staticcall(data);
require(success);
magicValue = abi.decode(result, (bytes4));
}

/**
munge to pass the SignerCreationCantOverride rule.
*/
function _hasNoCode(address account) internal view override returns (bool result) {
return account.code.length == 0;
}
}
Loading

0 comments on commit 1be8e52

Please sign in to comment.