Upstream Certora Specs #256
Conversation
andrew-certora
requested review from
dglowinski,
kasperpawlowski and
hoytech
as code owners
andrew-certora
requested review from
hoytech and
shoham-certora
and removed request for
hoytech
|
I have an implementation of @nd-certora 's improvements here: https://github.com/Certora/euler-vault/tree/andrew%40HolyGrailImprovements . There are timeouts that I am attempting to address before putting those changes here. |
|
Thanks @nd-certora for suggesting these improvements! I think the spec is better now. Here are a new (mostly*) complete set of passing runs after these improvements: Borrowing (all, splitting not needed anymore apparently): BalanceForwarder: Liquidation (all except liquidate): Liquidation.liquidate: Vault.withdraw: Caveat* the Liquidation.liquidate case "Account of HS check is liquidator and debt socialization always disabled" has a vacuity check timeout. This should be a less intersting case than the one where socialization is enabled and because of all the other cases passing the vacuity check, I doubt there is an issue with vacuity. I will try just rerunning and also rerunning without the vacuity check and add the result. (I am optimistic enough that this will work to merge the changes into the PR). |
|
that one last case does pass without the sanity check: https://vaas-stg.certora.com/output/65266/c15c876ec63e46e28259831b2113e1e4/?anonymousKey=81fa56928213bb75f84885d0dcf83978160f6b95 |
certora/conf/ERC4626Split/VaultERC4626-vaultSolvency-withdraw.conf
Outdated
Show resolved
Hide resolved
We need to change two private functions to internal so we can harness them and verify properties of these functions. See related PR that builds on this change: #256
There was a problem hiding this comment.
@kasperpawlowski Made some fixes according to your suggestions and looked into your points. I'm just waiting on a few runs (some with rather long runtimes) to finish so we can confirm everything.
|
|
||
| bool healthyBefore = checkLiquidityReturning(e, account, collaterals); | ||
| f(e, args); | ||
| // The only way to call a vault funciton is through EVC's call, batch, |
There was a problem hiding this comment.
Hi @kasperpawlowski. Thanks so much for pointing this out and for your thorough review. You are absolutely right, and this helped us identify a mistake in the spec. It should need and include an assumption that checks are deferred here, but there was another issue with the spec. This was subtle and we have been investigating it. Fortunately, we think we have it fixed now, and are rerunning the fixed rules to confirm that our fix is correct.
It turns out that due to a mistake in our summaries, with this setup we could spuriously prove EVC.areChecksDeferred() returns true in all cases: https://vaas-stg.certora.com/output/65266/0f25180bc5304f6c9c1f3a1f3e53a195/?anonymousKey=6b7327f914bb55c04494f19c57f409a2045bc1c2. The reason for this is that with the env variables in our CVLCheckAccountStatusInternal summary as they were written when you reviewed this we actually caused checkAccountStatus@withRevert to always revert:
function CVLCheckAccountStatusInternalBool(env e, address account) returns bool {
address[] collaterals = evc.getCollaterals(e, account);
checkAccountStatus@withrevert(e, account, collaterals); // the problem is with this env variable more details below.
return !lastReverted;
}
// This summary is applied to EthereumVaultConnector.checkAccountStatusInternal
function CVLCheckAccountStatusInternal(env e, address account) returns (bool, bytes) {
return (CVLCheckAccountStatusInternalBool(e, account),
checkAccountMagicValueMemory(e));
}
The issue with this is that here we are passing the env e that was used during the the vault’s call to EVC’s checkAccountStatus.Because env variables have the msg.sender in them, this forces the msg.sender to be the the same for both: 1) the call from the contract under verification (a vault module) to EVC.requireAccountStatusCheck (which is reached as part of Base.init’s call to EVCRequireStatusChecks) and 2) the call back from EVC into the vault (the call from EVC.requireAccountStatusCheckInternal into Riskmanager.checkAccountStatus). As a result, msg.sender will be the contract under verification during RiskManager.checkAccountStatus rather than evc and when we reach this revert check as a part of the checkAccountStatus call it will always revert
function checkAccountStatus(address account, address[] calldata collaterals)
public
virtual
reentrantOK
onlyEVCChecks /// this is the important part
returns (bytes4 magicValue)
{
}
modifier onlyEVCChecks() {
if (msg.sender != address(evc) || !evc.areChecksInProgress()) {
revert E_CheckUnauthorized(); // we were always reverting here during just the EVC checkAccount/Vault summaries
}
_;
}
There is a similar problem with both the summary for checkAccountStatusInternal and checkVaultStatusInternal.
We confirmed this was the issue by declaring fresh environment variables for these summaries and continuing to omit the requirement that evc.areChecksDeferred().In this case there is a counterexample as you would expect: https://vaas-stg.certora.com/output/65266/7663d91b72c04214898586e968adee89/?anonymousKey=a9b11593bd253324353519853241b692b2f82a24 Note also that in this failing case, evc.areChecksDeferred is returning false indicating this is the reason for the counterexample.
Here is the code that declares a fresh environment variable in the summary. Our candidate fix is to make this change and also add the assumption that evc.areChecksDeferred:
function CVLCheckAccountStatusInternal(address account) returns (bool, bytes) {
// We need a new env for the first function.
// Since the vault calls the EVC, otherwise msg.sender
// would become the vault unless we declare a fresh environment.
env eEVC;
return (CVLCheckAccountStatusInternalBool(eEVC, account),
checkAccountMagicValueMemory());
}
We are currently rerunning all the holy grail runs to make sure that it still passes with this fix. I do want to assure you though that despite this problem and investigation, I did not suspect there was a critical issue with the main intent of the rule – during the development of the rule it failed unless we called evc.checkStatusAll to make the EVC’s call to this function (as a part of restoring the execution context) at the end of call/batch. This is a good sign because it means the rule would catch any issues related to not enqueueing the right deferred account checks. The issue was just that we subtly forced the deferred status checks flag to always be true.
That said, we take the quality of our specifications and verification results very seriously and:
We are rerunning all the holy grail runs to confirm it still passes after this fix
We will thoroughly re-review all of our specifications here
We will write the additional rules you requested and potentially a few others related to assumptions made about the EVC.
Thanks again for your own very detailed and thorough review of the specifications.
This is an upstream of all the Certora specs for the Vault aside from the ones generated by contest participants.