Andrew #20
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,43 @@ | ||
| { | ||
| "files": [ | ||
| "src/LiquidityPool.sol", | ||
| "src/EETH.sol", | ||
| "src/EtherFiNodesManager.sol", | ||
| "src/BNFT.sol", | ||
| "src/TNFT.sol", | ||
| "certora/harnesses/EtherFiNodeA.sol", | ||
| "certora/harnesses/EtherFiNodeB.sol", | ||
| "src/RoleRegistry.sol", | ||
| ], | ||
| "verify": "EtherFiNodesManager:certora/specs/Basic.spec", | ||
| "link":[ | ||
| /// ===================== | ||
| "LiquidityPool:eETH=EETH", | ||
| "LiquidityPool:nodesManager=EtherFiNodesManager", | ||
| "LiquidityPool:tNft=TNFT", | ||
| "LiquidityPool:roleRegistry=RoleRegistry", | ||
| /// ===================== | ||
| "EtherFiNodesManager:tnft=TNFT", | ||
| "EtherFiNodesManager:bnft=BNFT", | ||
| "EtherFiNodesManager:roleRegistry=RoleRegistry", | ||
| /// ===================== | ||
| "EtherFiNodeA:etherFiNodesManager=EtherFiNodesManager", | ||
| "EtherFiNodeB:etherFiNodesManager=EtherFiNodesManager", | ||
| /// ===================== | ||
| "EETH:liquidityPool=LiquidityPool", | ||
| ], | ||
| "packages": [ | ||
| "@openzeppelin=lib/openzeppelin-contracts", | ||
| "@openzeppelin-upgradeable=lib/openzeppelin-contracts-upgradeable", | ||
| "forge-std=lib/forge-std/src", | ||
| ], | ||
| "build_cache": true, | ||
| "solc":"solc8.24", | ||
| "contract_recursion_limit":"2", | ||
| /// Notice optimistic settings | ||
| "loop_iter": "2", | ||
| "optimistic_loop": true, | ||
| "optimistic_fallback": true, | ||
| "rule_sanity": "basic", | ||
| "msg": "Money flow EtherFiNodesManager" | ||
| } |
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,8 @@ | ||
| // SPDX-License-Identifier: MIT | ||
| pragma solidity ^0.8.20; | ||
|
|
||
| contract CallHookHelper { | ||
| // This funciton is just a way to save msg.sender and msg.value | ||
| // from unresolved calls. This gets routed to a CVL function. | ||
| function HarnessCallHook() external {} | ||
Roy-Certora marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| } | ||
|
There was a problem hiding this comment. The verification is not yet complete.
There was a problem hiding this comment.
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).
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 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. There was a problem hiding this comment. 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:
There was a problem hiding this comment.
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.
I looked into how these values are sent and I don't see a way to specify this other than essentially to rewrite
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. There was a problem hiding this comment. 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 |
|---|---|---|
| @@ -0,0 +1,157 @@ | ||
| // import "./ERC721Receiver.spec"; | ||
| // import "./EtherFiNodeInterface.spec"; | ||
| // import "./EtherFiNodesManagerSetup.spec"; | ||
| // import "./EigenLayerMethods.spec"; | ||
| 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 [ | ||
Roy-Certora marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| CallHookHelper.HarnessCallHook() | ||
| ] default NONDET; | ||
|
|
||
| function CallHookHelper.HarnessCallHook() external with (env e) => CVLCallHook(e); | ||
|
|
||
| } | ||
|
|
||
| // This function is used to catch all cases where there is | ||
andrew-certora marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| // 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; | ||
| } | ||
| } | ||
|
|
||
| // the only possible flow of validator funds is eigenpod -> etherfiNode -> | ||
| // expectedParties where expected parties in the current contract are currently | ||
| // bnftHolder / tnftHolder / nodeOperator / treasury. An upcoming change from @V | ||
| // will be adjusting that mechanism slightly so that all funds flow directly to | ||
| // the liquidity pool. But the important piece of the property to me is simply | ||
| // that funds can't possibly be transferred to an unexpected target. This would | ||
| // give the assurance that the worst case scenario of a logic bug is simply that | ||
| // some validator funds could be temporarily stuck until we upgrade with a fix, | ||
| // but user funds would never be lost. | ||
|
|
||
| // * 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. | ||
| // * withdrawFunds can only be called by EtherFiNodeManager | ||
| // (because of a modifier) and it transfers money to addresses | ||
| // passed by parameter | ||
| // * 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 | ||
|
|
||
| rule money_flow_from_node_full_withdraw { | ||
|
There was a problem hiding this comment. I think it's better to check all the addresses whose native balance could change. There was a problem hiding this comment. I don't see how this is any better than checking the recipients of nonzero values in terms of security. In fact I think checking the recipient of nonzero value aligns more closely with what the customer requested. |
||
| 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; | ||
|
|
||
| // 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 | ||
| mathint nondeterministic_choice; | ||
| if (nondeterministic_choice == 0) { | ||
andrew-certora marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| satisfy money_recipient == treasury; | ||
| } else if (nondeterministic_choice == 1) { | ||
| satisfy money_recipient == nodeOperator; | ||
| } else if (nondeterministic_choice == 2) { | ||
| satisfy money_recipient == bnftHolder; | ||
| } else { | ||
| satisfy money_recipient == tnftHolder; | ||
| } | ||
|
|
||
| } | ||
|
|
||
| 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 | ||
| address treasury = currentContract.treasuryContract; | ||
| address nodeOperator = auctionManager.getBidOwner(e, validatorId); | ||
| address bnftHolder = currentContract.bnft.ownerOf(e, validatorId); | ||
| address tnftHolder = currentContract.tnft.ownerOf(e, validatorId); | ||
|
|
||
| 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; | ||
|
|
||
| // 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 | ||
| mathint nondeterministic_choice; | ||
| if (nondeterministic_choice == 0) { | ||
| satisfy money_recipient == treasury; | ||
| } else if (nondeterministic_choice == 1) { | ||
| satisfy money_recipient == nodeOperator; | ||
| } else if (nondeterministic_choice == 2) { | ||
| satisfy money_recipient == bnftHolder; | ||
| } else { | ||
| satisfy money_recipient == tnftHolder; | ||
| } | ||
| } | ||
|
|
||
| // Show that only EtherFiNodesManager can call the | ||
| // funcitons of EtherFiNode that move money out | ||
| rule only_nodes_manager (method f) filtered { f -> | ||
|
There was a problem hiding this comment. Didn't we have that in Basic.spec? There was a problem hiding this comment. 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) | ||
| }{ | ||
| calldataarg args; | ||
| env e; | ||
| f(e, args); | ||
| assert e.msg.sender == NodeA.etherFiNodesManager; | ||
| } | ||
There was a problem hiding this comment.
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?
There was a problem hiding this comment.
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.getBidOwnerwhich 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.