Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Certora Prover setup and properties for the audit of Passkey module #495

Closed
wants to merge 133 commits into from
Closed

Certora Prover setup and properties for the audit of Passkey module #495

wants to merge 133 commits into from

Conversation

hristo-grigorov
Copy link

This PR includes the setup files (.conf files, harnesses, munged .sol files) and .spec files with properties for the different contracts as part of the Passkey module audit by Certora.

All the rules were verified using the latest certora-cli (7.14.2).

yoav-el-certora and others added 30 commits April 25, 2024 18:17
@yoav-el-certora
Added first batch of setup confs
e2dca84
@yoav-el-certora
Small fixes
512eb51
@yoav-el-certora
Reorganize all folders, Added specific spec file for each contract, A…
ff3c325 
…dded summarizations.
@nivcertora
Merge branch 'main' of github.com:Certora/safe-modules into certora
7070a09
@yoav-el-certora
Merge branch 'safe-global:main' into certora
cedccec
@nivcertora
Merge branch 'certora' of github.com:Certora/safe-modules into certora
5ef533b
@nivcertora
Merge branch 'main' of github.com:Certora/safe-modules into certora
aca3afc
@nivcertora
.
da59212
@nivcertora
Add webAuthn conf
9488e45
@nivcertora
Merge pull request #1 from Certora/niv/Orgenazie-Files
9545b45 
Organize project setup files
@nivcertora
Fix sanity using alex parameters
8ba3831
@nivcertora
Merge pull request #2 from Certora/niv/Handle-signer-methods
26fd77b 
Fix sanity using alex parameters
@nivcertora
Add property list
b8989c3
@nivcertora
Add property list
d71c9a8
@nivcertora
Add property list
d132793
@nivcertora
Add property list
dc842ad
@nivcertora
Add property list
f247607
@nivcertora
Add property list
5aa3bac
@nivcertora
Add property list
39e5159
@nivcertora
Add property list
f50532f
@nivcertora
Add property list
896c24b
@yoav-el-certora
Updated properties and priorities.
64a6083
@nivcertora
.
20f659b
@liav-certora
Update SafeWebAuthnSignerProxy.spec
589a626
@liav-certora
Update SafeWebAuthnSignerProxy.spec
66b5fcb
@nivcertora
.
6242d48
@yoav-el-certora
Added all properties.
4714c04 
getConfiguration Integrity not done yet.
@liav-certora
Merge pull request #3 from Certora/liav/property
e5c5e70 
Proxy Immutability Property
@yoav-el-certora
Added the harness file
c9d1532
@nivcertora
.
958f508
nivcertora and others added 15 commits August 21, 2024 12:31
@nivcertora
Merge branch 'certora' of github.com:Certora/safe-modules into niv/Ad…
2299bce 
…d-ALL-Rules
@nivcertora
Add john fixes
d4a9be6
@yoav-el-certora
Merge pull request #14 from Certora/niv/Add-ALL-Rules
6df348c 
Niv/add all rules
@yoav-el-certora
Added conf files and fixed all issues
62742d0
@yoav-el-certora
Last fixes
161d059
@yoav-el-certora
Add munge
b8427fc
@yoav-el-certora
Add munge
91fce2c
@yoav-el-certora
Add munge
78e74a1
@yoav-el-certora
Merge pull request #20 from Certora/Yoav_Work_On_createAndVerifyEQtoI…
9fa6a17 
…sValidSignatureForSigner

Add munge
@yoav-el-certora
Add munge
7de765d
@yoav-el-certora
Merge pull request #21 from Certora/Yoav_Work_On_createAndVerifyEQtoI…
3c7c57b 
…sValidSignatureForSigner

Add munge
@yoav-el-certora
Merge pull request #19 from Certora/Yoav_Safe_For_Delivery
7f56a64 
Yoav safe for delivery
restore private to public munge of modules/passkey/contracts/librarie…
4616e1d 
…s/WebAuthn.sol
@hristo-grigorov
Merge pull request #22 from Certora/Yoav_Safe_For_Delivery
0862df2 
restore private to public munge of modules/passkey/contracts/librarie…
@hristo-grigorov
WebAuthnHarness to WebAuthnHarnessWithMunge fix
a1eab8a
@hristo-grigorov hristo-grigorov requested a review from a team as a code owner September 12, 2024 19:50
@hristo-grigorov hristo-grigorov requested review from nlordell, akshay-ap, mmv08 and remedcu and removed request for a team September 12, 2024 19:50
@github-actions GitHub Actions
Copy link

CLA Assistant Lite bot:
Thank you for your submission, we really appreciate it. Like many open-source projects, we ask that you all sign our Contributor License Agreement before we can accept your contribution. You can sign the CLA by just posting a Pull Request Comment same as the below format.

I have read the CLA Document and I hereby sign the CLA

0 out of 3 committers have signed the CLA.
❌ @yoav-el-certora
❌ @nivcertora
❌ @liav-certora
You can retrigger this bot by commenting recheck in this Pull Request

@mmv08
Copy link
Member

mmv08 commented Sep 13, 2024 •
edited
Loading

Could you please move the folder from root to modules/passkey? Since this is a monorepo and the rules only concern the passkey module, it's better placed there.

You can also enable the "allow edits from maintainers" option so we can fix small nits ourselves.

@hristo-grigorov
Copy link
Author

I have read the CLA Document and I hereby sign the CLA

@nlordell
Copy link
Collaborator

For the CLA - the individual commit authors need to sign it for the bot. Alternatively, you can squash the commits into one with a single author to make it easier :)

@remedcu remedcu mentioned this pull request Sep 20, 2024
Merged
remedcu added a commit that referenced this pull request Oct 14, 2024
@remedcu
FV based on audit of Passkey module (#496)
0b9ea28 
Based on #495 

This PR was made based on Certora's `safe-modules` repo with the FV
specifications.

The author was manually changed to avoid the CLA requirement.

Steps:
```
git remote add Certora https://github.com/Certora/safe-modules/
git fetch Certora
git checkout -b fv-passkey
git merge --squash certora
// Git commit with GUI to add details of all squashed commits
git commit --amend --author="Shebin John <admin@remedcu.com>" --no-edit
git push -u origin fv-passkey
```

Some other changes includes:
- Moving FV to `modules/passkey`
- Formatting changes
- Path update
- Using `solc8.26` for FV
@remedcu
Copy link
Member

remedcu commented Oct 14, 2024

Closing in favor of #496

@remedcu remedcu closed this Oct 14, 2024
@github-actions github-actions bot locked and limited conversation to collaborators Oct 14, 2024
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@nlordell nlordell Awaiting requested review from nlordell nlordell is a code owner automatically assigned from safe-global/safe-protocol

@akshay-ap akshay-ap Awaiting requested review from akshay-ap akshay-ap is a code owner automatically assigned from safe-global/safe-protocol

@mmv08 mmv08 Awaiting requested review from mmv08 mmv08 is a code owner automatically assigned from safe-global/safe-protocol

@remedcu remedcu Awaiting requested review from remedcu remedcu is a code owner automatically assigned from safe-global/safe-protocol

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
7 participants
@hristo-grigorov @mmv08 @nlordell @remedcu @yoav-el-certora @nivcertora @liav-certora