search

ubiquity / ubiquity-dollar

Ubiquity Dollar (uAD) smart contracts and user interface.
https://uad.ubq.fi
Apache License 2.0
31 stars 82 forks source link

Formal verification #926

Open rndquu opened 2 months ago

rndquu commented 2 months ago

We should implement formal verification for LibUbiquityPool.

So collaborator who's going to take this issue should carefully study the LibUbiquityPool and think of the invariants that should be tested.

Invariants could be:

Possible solutions for formal verification:

We already had a try with formal verification, you may find related scripts here.

What should be done:

  1. Impelent formal verification for the LibUbiquityPool contract (you may create tests in a separate test file like UbiquityPoolFacet.formal.t.sol so we could distinguish unit, fuzz, invariant and formal verification tests)
  2. Setup testing CI to run formal verification tests on merge to the development branch (keep in mind that github action runnners can run for 6 hours). We don't need to run formal verification tests on eash PR since they're really time consuming.
0x4007 commented 2 months ago

I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

rndquu commented 2 months ago

I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

I guess you mean this topic: https://github.com/ubiquity/ubiquity-dollar/discussions/197

This issue doesn't include only 2 topics you mentioned at https://github.com/ubiquity/ubiquity-dollar/discussions/197:

Regarding the bug bounty program, we have an implicit rule (which we applied at least 2 times) to reward 10% of the funds at risk. So I think a simple mention of bug bounty program somewhere at https://ubq.fi/ is enough, without going into details of severity, possibility, etc...

Regarding the incident handling, all of the tutorials that I read goes simply to:

  1. Pause contracts
  2. Find the root cause
  3. Fix the root cause

The most important is step 1 which pauses contracts. If it is not on time then all other mitigation steps don't make sense. So a separate incident response tutorial seems to be a low priority issue right now.

rndquu commented 1 month ago

I heard great things about Certora. If you search the ubiquity org for me writing the term "Certora" you can see that I listed a security checklist with a lot of what you filed issues for.

Certora is closed sourced and has a pretty steep learning curve. I've had great experience using https://github.com/a16z/halmos which seems to be the most user friendly out of all of the tools.

0x4007 commented 1 month ago

They asked me to schedule a call with them. I am under the impression that we can bring on one of their engineers to implement things.

If you're interested I can consider your availability before booking

https://calendly.com/d/444-zpr-54m/30-minute-meeting

rndquu commented 1 month ago

They asked me to schedule a call with them. I am under the impression that we can bring on one of their engineers to implement things.

If you're interested I can consider your availability before booking

https://calendly.com/d/444-zpr-54m/30-minute-meeting

Of course they asked for a call since they need to sell the product. Certora is a proprietary paid "formal verification as a service" company. They bring on one of the engineers since the product is really complicated. I'd rather use one of the open-sourced solutions and have one of the core team members to solve this issue in order to keep the context/knowledge in Ubiquity DAO instead of outsourcing solving this issue.