Andrew #20
Andrew #20
Conversation
As suggested by Roy
There was a problem hiding this comment.
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.
There was a problem hiding this comment.
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.
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:
-
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.
There was a problem hiding this comment.
- 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.
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.
| @@ -5,11 +5,13 @@ | |||
| "src/EtherFiNodesManager.sol", | |||
| "src/BNFT.sol", | |||
| "src/TNFT.sol", | |||
| "src/AuctionManager.sol", | |||
There was a problem hiding this comment.
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.
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.
| // 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.
|
|
||
| // 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.
|
|
||
| // These cause hardstops | ||
| // // frontrunning cannot cause withdraw to be blocked | ||
| // rule money_flow_from_node_full_withdraw_frontrunning (method f) { |
There was a problem hiding this comment.
Yes, that's expected. It's a difficult rule.
Maybe we can start by filtering to a single method that also involves ETH transfer?
There was a problem hiding this comment.
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.
No description provided.