This PR addresses #69. It includes a single/simple change: we do not update stake[cur_epoch+1] when slashing the destination validator of a redelegation when an infraction committed by the source validator is processed.
This solution only works under the assumption that pipeline_offset>1, which is the case by default in Namada. Nevertheless, this was not required before.
A drawback is that there is one more epoch to misbehave multiple times with the same tokens.
I've run the Quint simulator and no violation was found. I've run the following experiments:
Furthermore, I have done a protocol analysis. Assume the following:
A user alice redelegates X tokens from src to dest validators at epoch e_1.
Assume that pipeline_lenght=2.
src misbehaves at epoch e_1+1, i.e., within the redelegation slashing window.
Q1: can alice withdraw its X tokens without getting slashed?
For this to happen, alice must withdraw before the slash is processed.
No matter when the infraction is discovered, it will be processed at the end of the epoch resulting from adding cubic_offset+unbonding_offset to the infraction epoch e_1+1. Thus, the slash is processed at the end of epoch e_2=e_1+1+cubic_offset+unbonding_offset.
Therefore, alice would be able to withdraw the tokens avoiding slashing if she withdraws them at an epoch <= e_2.
Assume to contradict that she is able to do it at e_2 (if we prove it for e_2, we prove it for any epoch < e_2):
Then, she unbonded the tokens at an epoch <= e_2-pipeline_offset-cubic_offset-unbonding_offset (the unbond end epoch)
The latest she unbonded ise_3=e_2-pipeline_offset-cubic_offset-unbonding_offset.
We have that e_2=e_1+1+cubic_offset+unbonding_offset, i.e., e_3=e_1+1-pipeline_offset.
Therefore, since pipeline_offset=2, e_3<e_1, a contradiction.
The above proof sketch proves by contradiction that alice can't withdraw its X tokens without getting slashed.
Q2: can alice be slashed before dest is slashed?
No matter when the infraction is discovered, it will be processed at the end of the epoch resulting from adding cubic_offset+unbonding_offset to the infraction epoch e_1+1. Thus, the slash is processed at the end of epoch e_2=e_1+1+cubic_offset+unbonding_offset.
For the required to happen, alice must be able to withdraw one epoch after the slash is processed: since do not update stake[cur_epoch+1], the only window for the required to happen is cur_epoch+1, where cur_epoch is the epoch at which the slash is processed. Thus alice should withdraw at e_2+1.
Let's compute at which epoch e_3alice must start unbonding the tokens:
(i) It has to be an epoch <= e_2+1-pipeline_offset-cubic_offset-unbonding_offset (the unbond end epoch)
(ii) Also, the unbonded epoch should be >= e_1+pipeline_offset; otherwise, the tokens would not have been relegated yet, and alice could not unbond them.
Then by (i) and (ii), e_1+pipeline_offset <= e_3 <= e_2+1-pipeline_offset-cubic_offset-unbonding_offset, i.e., e_1+pipeline_offset <= e_3 <= e_1+2-pipeline_offset.
there exists a e_3 only if pipeline_offset=1.
The above proof sketch proves that alice could be slashed before dest only if pipeline_offset=1. This should be fine as we expect pipeline_offset>=2. In any case, it is unclear that allowing the above is a problem.
Q3: can alice unbond the tokens after the infraction is processed but before dest is slashed?
No matter when the infraction is discovered, it will be processed at the end of the epoch resulting from adding cubic_offset+unbonding_offset to the infraction epoch e_1+1. Thus, the slash is processed at the end of epoch e_2=e_1+1+cubic_offset+unbonding_offset.
For the required to happen, alice must be able to unbond one epoch after the slash is processed: since do not update stake[cur_epoch+1], the only window for the required to happen is cur_epoch+1, where cur_epoch is the epoch at which the slash is processed. Thus alice should unbond at e_2+1.
The unbonded epoch should be >= e_1+pipeline_offset; otherwise, the tokens would not have been relegated yet, and alice could not unbond them.
Since e_2=e_1+1+cubic_offset+unbonding_offset and pipeline_offset<=unbonding_offset, then e_2+1>=e_1+pipeline_offset, as required.
The above proof sketch proves that alice can unbond the tokens after the infraction is processed but before dest is slashed. This is definitely something that was not allowed before the change introduced by this PR. The question now is whether this can be exploited or not.
This PR addresses #69. It includes a single/simple change: we do not update
stake[cur_epoch+1]when slashing the destination validator of a redelegation when an infraction committed by the source validator is processed.This solution only works under the assumption that
pipeline_offset>1, which is the case by default in Namada. Nevertheless, this was not required before.A drawback is that there is one more epoch to misbehave multiple times with the same tokens.
I've run the Quint simulator and no violation was found. I've run the following experiments:
Furthermore, I have done a protocol analysis. Assume the following:
aliceredelegatesXtokens fromsrctodestvalidators at epoche_1.pipeline_lenght=2.srcmisbehaves at epoche_1+1, i.e., within the redelegation slashing window.Q1: can
alicewithdraw itsXtokens without getting slashed?alicemust withdraw before the slash is processed.cubic_offset+unbonding_offsetto the infraction epoche_1+1. Thus, the slash is processed at the end of epoche_2=e_1+1+cubic_offset+unbonding_offset.alicewould be able to withdraw the tokens avoiding slashing if she withdraws them at an epoch<= e_2.e_2(if we prove it fore_2, we prove it for any epoch< e_2):<= e_2-pipeline_offset-cubic_offset-unbonding_offset(the unbond end epoch)e_3=e_2-pipeline_offset-cubic_offset-unbonding_offset.e_2=e_1+1+cubic_offset+unbonding_offset, i.e.,e_3=e_1+1-pipeline_offset.pipeline_offset=2,e_3<e_1, a contradiction.The above proof sketch proves by contradiction that
alicecan't withdraw itsXtokens without getting slashed.Q2: can
alicebe slashed beforedestis slashed?cubic_offset+unbonding_offsetto the infraction epoche_1+1. Thus, the slash is processed at the end of epoche_2=e_1+1+cubic_offset+unbonding_offset.alicemust be able to withdraw one epoch after the slash is processed: since do not updatestake[cur_epoch+1], the only window for the required to happen iscur_epoch+1, wherecur_epochis the epoch at which the slash is processed. Thusaliceshould withdraw ate_2+1.e_3alicemust start unbonding the tokens:<= e_2+1-pipeline_offset-cubic_offset-unbonding_offset(the unbond end epoch)>= e_1+pipeline_offset; otherwise, the tokens would not have been relegated yet, andalicecould not unbond them.e_1+pipeline_offset <= e_3 <= e_2+1-pipeline_offset-cubic_offset-unbonding_offset, i.e.,e_1+pipeline_offset <= e_3 <= e_1+2-pipeline_offset.e_3only ifpipeline_offset=1.The above proof sketch proves that
alicecould be slashed beforedestonly ifpipeline_offset=1. This should be fine as we expectpipeline_offset>=2. In any case, it is unclear that allowing the above is a problem.Q3: can
aliceunbond the tokens after the infraction is processed but beforedestis slashed?cubic_offset+unbonding_offsetto the infraction epoche_1+1. Thus, the slash is processed at the end of epoche_2=e_1+1+cubic_offset+unbonding_offset.alicemust be able to unbond one epoch after the slash is processed: since do not updatestake[cur_epoch+1], the only window for the required to happen iscur_epoch+1, wherecur_epochis the epoch at which the slash is processed. Thusaliceshould unbond ate_2+1.>= e_1+pipeline_offset; otherwise, the tokens would not have been relegated yet, andalicecould not unbond them.e_2=e_1+1+cubic_offset+unbonding_offsetandpipeline_offset<=unbonding_offset, thene_2+1>=e_1+pipeline_offset, as required.The above proof sketch proves that
alicecan unbond the tokens after the infraction is processed but beforedestis slashed. This is definitely something that was not allowed before the change introduced by this PR. The question now is whether this can be exploited or not.