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,51 @@ | ||
| { | ||
| "files": [ | ||
| "src/LiquidityPool.sol", | ||
| "src/EETH.sol", | ||
| "src/EtherFiNodesManager.sol", | ||
| "src/BNFT.sol", | ||
| "src/TNFT.sol", | ||
| "src/AuctionManager.sol", | ||
| "certora/harnesses/EtherFiNodeA.sol", | ||
| "certora/harnesses/EtherFiNodeB.sol", | ||
| "src/RoleRegistry.sol", | ||
| ], | ||
| "verify": "EtherFiNodesManager:certora/specs/RecipientsDontChange.spec", | ||
| "link":[ | ||
| /// ===================== | ||
| "LiquidityPool:eETH=EETH", | ||
| "LiquidityPool:nodesManager=EtherFiNodesManager", | ||
| "LiquidityPool:tNft=TNFT", | ||
| "LiquidityPool:roleRegistry=RoleRegistry", | ||
| /// ===================== | ||
| "EtherFiNodesManager:tnft=TNFT", | ||
| "EtherFiNodesManager:bnft=BNFT", | ||
| "EtherFiNodesManager:roleRegistry=RoleRegistry", | ||
| "EtherFiNodesManager:auctionManager=AuctionManager", | ||
| /// ===================== | ||
| "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", | ||
| ], | ||
| "parametric_contracts": [ | ||
| "AuctionManager", | ||
| "EtherFiNodeA", | ||
| "EtherFiNodeB", | ||
| "EtherFiNodesManager" | ||
| ], | ||
| "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": "recipients do not change EtherFiNodesManager" | ||
| } |
|
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,196 @@ | ||
| // Status: All Rules PASSING: https://prover.certora.com/output/65266/ff3119ec04544fdbb502959ea809567e/?anonymousKey=36c40fc440497ae114c993ed9818d44ad0577708 | ||
| import "./Basic.spec"; | ||
|
|
||
| using AuctionManager as auctionManager; | ||
|
|
||
| // 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 -> | ||
| // 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. | ||
|
|
||
| // 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 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); | ||
| } | ||
| } | ||
|
|
||
| // 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; | ||
|
|
||
| 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) { | ||
| // to generate call trace | ||
| satisfy sent_treasury; | ||
| } else if (nondeterministic_choice == 1) { | ||
| satisfy sent_nodeOperator; | ||
| } else if (nondeterministic_choice == 2) { | ||
| satisfy sent_bnftHolder; | ||
| } else { | ||
| satisfy sent_tnftHolder; | ||
| } | ||
|
|
||
| } | ||
|
|
||
| // // These cause hardstops | ||
| // // // frontrunning cannot cause withdraw to be blocked | ||
| // rule money_flow_from_node_full_withdraw_frontrunning (method f) | ||
| // filtered { f-> | ||
| // methodsCallEtherNode_NodesManager(f) | ||
| // }{ | ||
| // 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) | ||
| // filtered { f-> | ||
| // methodsCallEtherNode_NodesManager(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 | ||
| // functions 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.