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

Andrew #20

Draft
wants to merge 9 commits into
base: roy/withdrawRequestNFT
Choose a base branch
from
Draft

Andrew #20

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
61f2fa4
Comment out import as workaround for build failure
andrew-certora Oct 1, 2024
4944168
proof of remaining rules for EtherFiNode outflows
andrew-certora Oct 3, 2024
bf27ecf
Add that only NodeManager calls Node outflow fxns
andrew-certora Oct 7, 2024
490eff8
LiquidityPoolMoneyFlow passing
andrew-certora Oct 9, 2024
77ae603
Remove WIP Recipients dont changed
andrew-certora Oct 9, 2024
8e0a503
Delete callhook helper
andrew-certora Oct 10, 2024
23d389e
Recipients dont change with some filtering
andrew-certora Oct 11, 2024
d11c650
Add passing link to recipientsDoNotChange
andrew-certora Oct 11, 2024
af43a99
Comment out frontrunning rules
andrew-certora Oct 14, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion certora/config/LiquidityPoolMoneyFlow.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
"src/AuctionManager.sol",
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If we add it to the scene, perhaps it's worth checking that it doesn't involve transfer of funds?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We already eliminated this possibility: 1) we proved that there are only 2 functions of EitherFiNode that can move money out of the node, and 2) we proved that the only contract that can call them is the manager. So I think we don't need this to meet the goal of the customer.

I just added this to access AuctionManager.getBidOwner which is one of the addresses allowed in the outflow. I could consider just summarising this to return a ghost, but one of your other suggestions was to prove that a few IDs do not change, and summarizing here might contradict that.

"certora/harnesses/EtherFiNodeA.sol",
"certora/harnesses/EtherFiNodeB.sol",
"certora/helpers/CallHookHelper.sol",
"src/RoleRegistry.sol",
],
"verify": "EtherFiNodesManager:certora/specs/LiquidityPoolMoneyFlow.spec",
Expand Down
11 changes: 9 additions & 2 deletions certora/specs/Basic.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,12 @@ definition methodsSendETH_EtherFiNode(method f) returns bool =
f.selector == sig:EtherFiNodeA.withdrawFunds(address,uint256,address,uint256,address,uint256,address,uint256).selector;

rule whichFunctionSendsETH_EtherFiNode(method f)
filtered{f -> !f.isView && f.contract == NodeA}
filtered{
f -> !f.isView && f.contract == NodeA &&
// will fail the satisfy rule even though no money
// is sent and the assertion passes.
f.selector != sig:EtherFiNodeA.initialize(address).selector
}
{
env e;
require e.msg.sender != NodeA; /// Node doesn't call itself;
Expand All @@ -47,10 +52,12 @@ filtered{f -> !f.isView && f.contract == NodeA}

definition methodsCallEtherNode_NodesManager(method f) returns bool =
f.selector == sig:EtherFiNodesManager.partialWithdraw(uint256).selector ||
f.selector == sig:EtherFiNodesManager.batchPartialWithdraw(uint256[]).selector ||
andrew-certora marked this conversation as resolved.
Show resolved Hide resolved
f.selector == sig:EtherFiNodesManager.fullWithdraw(uint256).selector;

rule whichFunctionSendsETHFromNode_NodesManager(method f)
filtered{f -> !f.isView && ignoreMethods_NodesManager(f) && f.contract == NodesManager}
filtered{f -> !f.isView && !f.isFallback &&
ignoreMethods_NodesManager(f) && f.contract == NodesManager}
{
env e;
require e.msg.sender != NodesManager; /// Nodes manager doesn't call itself;
Expand Down
237 changes: 161 additions & 76 deletions certora/specs/LiquidityPoolMoneyFlow.spec
View file
Open in desktop
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The verification is not yet complete.
A few considerations we should pay attention to:

  • We haven't confirmed that the identity of the recipients (treasury, node operator, NFT holders) remain intact.
  • The amount of ETH per each validator should be limited. What if the contract did send the correct recipients but the wrong amounts?
  • Is it possible to block the ETH transfer in some way by external parties? In the rules present we simply assume they succeed but potentially money could be stuck.

Copy link

@andrew-certora andrew-certora Oct 7, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We haven't confirmed that the identity of the recipients (treasury, node operator, NFT holders) remain intact.

What do you mean by this? Do you mean an invariant that says these don't change or something like that?

(This also seems to be beyond what they requested. So I can attempt to do this, but it seems different from what they requested and I think it may still be worthwhile to show them what we did).

The amount of ETH per each validator should be limited. What if the contract did send the correct recipients but the wrong amounts?

This seems to go beyond the scope of what they requested which was just about the direction of funding. Is it still worthwhile to present what we have given that what they asked for shows the direction of funding and we did prove that? They might be happy with what we have already.

What do you have in mind to check here -- what are the "right amounts" for each of the recipient then?

Is it possible to block the ETH transfer in some way by external parties? In the rules present we simply assume they succeed but potentially money could be stuck.

Is there a way to specify this other than to assert that the transfer never reverts? I am also doubtful that asserting there are no reverts would be verifiable as there are usually always cases that a revert can happen.

Copy link
Author

@Roy-Certora Roy-Certora Oct 7, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We can't necessarily prove all the missing points I mentioned above in a decent amount of time. It's important nevertheless to pay attention to what we did manage to prove.

Even if the client didn't specify verbatim all these rules, he really cares about the funds being safe (and not just that any non-zero amount gets to the correct destination).

About the notes in particular:

  • When a validatorID is created, or when its 32ETH is sent to the Beacon chain, the relevant recipients are defined and shouldn't be changed (unless it's an T-NFT holder). The mapping validatorID -> recipient should stay constant once it is set.

  • If we could somehow track the total amount that is attributed to each validator and show that the sum of the 4 recipients rewards matches it, it would complete the proof.

  • The easiest approach I could think of is to show no one could front-run the call that transfers the ETH to its rightful owners. That is, if the call should succeed in some circumstance, it should not fail if someone were to call some function beforehand.
    This is something I would save for last.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

  • When a validatorID is created, or when its 32ETH is sent to the Beacon chain, the relevant recipients are defined and shouldn't be changed (unless it's an T-NFT holder). The mapping validatorID -> recipient should stay constant once it is set.

OK this sounds useful. I started a parametric rule that shows these don't change, but I'm not sure I'll finish specifying around all the edge cases before we need to close the project.

  • If we could somehow track the total amount that is attributed to each validator and show that the sum of the 4 recipients rewards matches it, it would complete the proof.

I looked into how these values are sent and I don't see a way to specify this other than essentially to rewrite getFullWithdrawalPayouts into CVL. I think doing this would both be too complicated and take forever, and not be too useful.

  • The easiest approach I could think of is to show no one could front-run the call that transfers the ETH to its rightful owners. That is, if the call should succeed in some circumstance, it should not fail if someone were to call some function beforehand. This is something I would save for last.

This is a good approach! I wrote this and it hits a hard stop. I did not attempt to improve performance because you mentioned this is lower priority and I think that makes sense.

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I added that rule that shows the recipients dont change (aside from when they do) in a separate file -- it's a separate file both for performance reasons and becasue I didn't want any summarization I might have introduced for RecipientsDontChange to interfere with the other rule. It is passing and AFAICT the cases I filter out or summarize are sensible.

Original file line number Diff line number Diff line change
@@ -1,34 +1,44 @@
// import "./ERC721Receiver.spec";
// import "./EtherFiNodeInterface.spec";
// import "./EtherFiNodesManagerSetup.spec";
// import "./EigenLayerMethods.spec";
// Status: All Rules PASSING: https://prover.certora.com/output/65266/ff3119ec04544fdbb502959ea809567e/?anonymousKey=36c40fc440497ae114c993ed9818d44ad0577708
import "./Basic.spec";

// using LiquidityPool as Pool;
using AuctionManager as auctionManager;

// Status: All rules here pass
// Run link: https://prover.certora.com/output/65266/e1ae0ebb78c346259a9bd46cf286b3bc/?anonymousKey=d2adcf131917ccf3f7512519f17a985f597b8ce3

methods {
// dispatcher list for unresolved calls in
// EtherFiNode.withdrawFunds
unresolved external in EtherFiNode._ => DISPATCH [
CallHookHelper.HarnessCallHook()
] default NONDET;

function CallHookHelper.HarnessCallHook() external with (env e) => CVLCallHook(e);

}

// This function is used to catch all cases where there is
// a call outside the contract under verification and save
// the target address whenever the value transferred is nonzero
persistent ghost address money_recipient;
function CVLCallHook(env e) {
if (e.msg.value > 0) {
money_recipient = e.msg.sender;
// Tracks if there was ever a transfer to an address
// other than the expected ones.
persistent ghost bool illegal_transfer;

// These are used to pass the relevant addresses to the hook. Calling
// methods on variables does not seem supported within hooks, so
// using these ghosts and calling the relevant functions in the rule
// is a workaround for that
persistent ghost address treasury;
persistent ghost address nodeOperator;
persistent ghost address bnftHolder;
persistent ghost address tnftHolder;

// These are used to express the liveness condition
// that each of these are sent value
persistent ghost bool sent_treasury;
persistent ghost bool sent_nodeOperator;
persistent ghost bool sent_bnftHolder;
persistent ghost bool sent_tnftHolder;

hook CALL(uint g, address addr, uint value, uint argsOffs, uint argLength, uint retOffset, uint retLength) uint rc {
if (value > 0) {
if (!(addr == treasury ||
addr == nodeOperator ||
addr == bnftHolder ||
addr == tnftHolder)) {
illegal_transfer = true;
}
// The OR is used so that we don't unset this.
// These are true if they are ever sent to
sent_treasury = sent_treasury || addr == treasury;
sent_nodeOperator = sent_nodeOperator || addr == nodeOperator;
sent_bnftHolder = sent_bnftHolder || addr == bnftHolder;
sent_tnftHolder = sent_tnftHolder || addr == tnftHolder;
}

}

// the only possible flow of validator funds is eigenpod -> etherfiNode ->
Expand All @@ -41,111 +51,186 @@ function CVLCallHook(env e) {
// some validator funds could be temporarily stuck until we upgrade with a fix,
// but user funds would never be lost.

// We rely on other rules to complete this proof.
// * whichFunctionSendsETH_EtherFiNode in Basic.spec proves
andrew-certora marked this conversation as resolved.
Show resolved Hide resolved
// that the only functions that move money out of EtherFiNode
// are withdrawFunds and moveFundsToManager.
use rule whichFunctionSendsETH_EtherFiNode;

// * withdrawFunds can only be called by EtherFiNodeManager
// (because of a modifier) and it transfers money to addresses
// passed by parameter
// see rule only_nodes_manager below

// * EtherFiNodesManager calls EtherFiNode.withdraw in
// distributePayouts which is internal and called by: fullWithdraw,
// partialWithdraw
// * whichFunctionSendsETHFromNode_NodesManager also
// proves that fullWithdraw / partialWithdraw
// are the only functions which cause
// are the only functions which cause money to move out of etherfiNode
use rule whichFunctionSendsETHFromNode_NodesManager;

// We then prove that for full/partial withdraw, money only
// flows to the expected recipients

function callMoneyMovementFunction(env e, method f, uint256 validator) {
if(f.selector == sig:EtherFiNodesManager.partialWithdraw(uint256).selector){
partialWithdraw(e, validator);
}
if(f.selector == sig:EtherFiNodesManager.fullWithdraw(uint256).selector){
fullWithdraw(e, validator);
}
if(f.selector == sig:EtherFiNodesManager.batchPartialWithdraw(uint256[]).selector){
uint256[] validators;
require validators.length == 1;
require validators[0] == validator;
batchPartialWithdraw(e, validators);
}
}

rule money_flow_from_node_full_withdraw {
// Money only flows to the expected recipients for full withdraw
rule money_flow_from_node (method f) filtered { f->
methodsCallEtherNode_NodesManager(f)
}{
uint256 validatorId;
env e;

// initialize ghost to currentContract
require money_recipient == currentContract;

// expected party addresses
address treasury = currentContract.treasuryContract;
address nodeOperator = auctionManager.getBidOwner(e, validatorId);
address bnftHolder = currentContract.bnft.ownerOf(e, validatorId);
address tnftHolder = currentContract.tnft.ownerOf(e, validatorId);

fullWithdraw(e, validatorId);

// If money was moved during this call it goes
// to one of the expected recipients. The
// case where money_recipient is currentContract
// models the case where nonzero money is not moved.
// temporarily made satisfy to check that this is a real result
// with the routing that I expect
assert money_recipient == currentContract ||
money_recipient == treasury ||
money_recipient == nodeOperator ||
money_recipient == bnftHolder ||
money_recipient == tnftHolder;
require treasury == currentContract.treasuryContract;
require nodeOperator == auctionManager.getBidOwner(e, validatorId);
require bnftHolder == currentContract.bnft.ownerOf(e, validatorId);
require tnftHolder == currentContract.tnft.ownerOf(e, validatorId);

require !sent_treasury;
require !sent_nodeOperator;
require !sent_bnftHolder;
require !sent_tnftHolder;

require !illegal_transfer;

callMoneyMovementFunction(e, f, validatorId);

// The following encodes that all of these recipient
// cases are reachable (and ensures that the above
// assertion isn't just trivially stuck in the initial state)

// This unconstrained ghost on which we branch is
// just here to encode nondeterminstic choice

assert !illegal_transfer;


satisfy treasury != nodeOperator &&
treasury != bnftHolder &&
treasury != tnftHolder &&
nodeOperator != bnftHolder &&
nodeOperator != tnftHolder &&
bnftHolder != tnftHolder;

mathint nondeterministic_choice;

if (nondeterministic_choice == 0) {
andrew-certora marked this conversation as resolved.
Show resolved Hide resolved
satisfy money_recipient == treasury;
// to generate call trace
satisfy sent_treasury;
} else if (nondeterministic_choice == 1) {
satisfy money_recipient == nodeOperator;
satisfy sent_nodeOperator;
} else if (nondeterministic_choice == 2) {
satisfy money_recipient == bnftHolder;
satisfy sent_bnftHolder;
} else {
satisfy money_recipient == tnftHolder;
satisfy sent_tnftHolder;
}

}

// Money only flows to the expected recipients for partial withdraw
/*
rule money_flow_from_node_partial_withdraw {
andrew-certora marked this conversation as resolved.
Show resolved Hide resolved
uint256 validatorId;
env e;

// initialize ghost to currentContract
require money_recipient == currentContract;
// // expected party addresses
require treasury == currentContract.treasuryContract;
require nodeOperator == auctionManager.getBidOwner(e, validatorId);
require bnftHolder == currentContract.bnft.ownerOf(e, validatorId);
require tnftHolder == currentContract.tnft.ownerOf(e, validatorId);

// expected party addresses
address treasury = currentContract.treasuryContract;
address nodeOperator = auctionManager.getBidOwner(e, validatorId);
address bnftHolder = currentContract.bnft.ownerOf(e, validatorId);
address tnftHolder = currentContract.tnft.ownerOf(e, validatorId);
require !illegal_transfer;

require !sent_treasury;
require !sent_nodeOperator;
require !sent_bnftHolder;
require !sent_tnftHolder;

partialWithdraw(e, validatorId);

// If money was moved during this call it goes
// to one of the expected recipients. The
// case where money_recipient is currentContract
// models the case where nonzero money is not moved.
assert money_recipient == currentContract ||
money_recipient == treasury ||
money_recipient == nodeOperator ||
money_recipient == bnftHolder ||
money_recipient == tnftHolder;
assert !illegal_transfer;

// The following encodes that all of these recipient
// cases are reachable (and ensures that the above
// assertion isn't just trivially stuck in the initial state)

satisfy treasury != nodeOperator &&
treasury != bnftHolder &&
treasury != tnftHolder &&
nodeOperator != bnftHolder &&
nodeOperator != tnftHolder &&
bnftHolder != tnftHolder;


// This unconstrained ghost on which we branch is
// just here to encode nondeterminstic choice
mathint nondeterministic_choice;

if (nondeterministic_choice == 0) {
satisfy money_recipient == treasury;
satisfy sent_treasury;
} else if (nondeterministic_choice == 1) {
satisfy money_recipient == nodeOperator;
satisfy sent_nodeOperator;
} else if (nondeterministic_choice == 2) {
satisfy money_recipient == bnftHolder;
satisfy sent_bnftHolder;
} else {
satisfy money_recipient == tnftHolder;
satisfy sent_tnftHolder;
}
}

*/

// These cause hardstops
// // frontrunning cannot cause withdraw to be blocked
// rule money_flow_from_node_full_withdraw_frontrunning (method f) {
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, that's expected. It's a difficult rule.
Maybe we can start by filtering to a single method that also involves ETH transfer?

Copy link
Author

@Roy-Certora Roy-Certora Oct 9, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just by simulating this in my head (and also from past experience with similar rules),
I could think of a case where the second call reverts if the contract doesn't have enough native balance to satisfy both transfers (that is, the original and the front-runner).
So it has enough ETH to satisfy each of the transfers individually, and not together.

This naturally leads to a need for some solvency assumption - that the contract has enough ETH for two validators at the same time.
We might deviate a bit from the original rule by trying to prove it (which isn't trivial) so perhaps we could simply assume it.

// uint256 validatorId;
// env e;
//
// storage init = lastStorage;
//
// fullWithdraw(e, validatorId);
//
// env e2;
// calldataarg args;
// f(e2, args);
//
// fullWithdraw@withrevert(e, validatorId) at init;
// assert !lastReverted;
// }

// // frontrunning cannot cause partial withdraw to be blocked
// rule money_flow_from_node_partial_withdraw_frontrunning (method f) {
// uint256 validatorId;
// env e;
//
// storage init = lastStorage;
//
// partialWithdraw(e, validatorId);
//
// env e2;
// calldataarg args;
// f(e2, args);
//
// partialWithdraw@withrevert(e, validatorId) at init;
// assert !lastReverted;
// }
//
//
// Show that only EtherFiNodesManager can call the
// funcitons of EtherFiNode that move money out
// functions of EtherFiNode that move money out

rule only_nodes_manager (method f) filtered { f ->
Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Didn't we have that in Basic.spec?

Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

No not exactly. We have rules that constrain which methods of EtherFiNode and EtherFiNodeManager can move money out of EtherFiNode, but we don't prove that the methods of EtherFiNode which move money out are only callable by the manager which is implicitly assumed with this setup.

!f.isView && f.contract == NodeA &&
methodsSendETH_EtherFiNode(f)
Expand Down