Skip to content

[Certora] Ensure that an Augustus can't call approve. #254

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
Open
gd-colin wants to merge 4 commits into
base: main
Choose a base branch
from
Open

[Certora] Ensure that an Augustus can't call approve. #254

gd-colin wants to merge 4 commits into from

Conversation

@gd-colin
Copy link
Contributor

@gd-colin gd-colin commented Apr 13, 2025 •
edited
Loading

This PR:

  • the current specs does not cover the ParaswapAdapter;
  • we lift this restriction on the allowancesAreReset invariant;
  • we simulate an Augustus contract and ensure that it can't call (the prover does not support this with the delegatecall) approve through the low-level call with a mock contract.

@gd-colin gd-colin added the verif Fromal verification with Certora label Apr 13, 2025
@gd-colin gd-colin requested review from MathisGD and QGarchery April 13, 2025 13:53
@gd-colin gd-colin self-assigned this Apr 13, 2025
@gd-colin gd-colin changed the title [Certora] Ensure that a safe Augustus can't call approve. [Certora] Ensure that an Augustus can't call approve. Apr 13, 2025
QGarchery
QGarchery reviewed Apr 14, 2025
View reviewed changes
@gd-colin gd-colin requested a review from QGarchery April 14, 2025 10:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@MathisGD MathisGD Awaiting requested review from MathisGD

@QGarchery QGarchery Awaiting requested review from QGarchery

At least 2 approving reviews are required to merge this pull request.

Assignees

@gd-colin gd-colin

Labels

verif Fromal verification with Certora

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@gd-colin @QGarchery