search

informalsystems / verification

Specifications of the protocols and the experiments on their verification
9 stars 2 forks source link

light-client/Blockchain.tla false properties pass #10

Open ancazamfir opened 4 years ago

ancazamfir commented 4 years ago

Tried to run the false properties starting with: https://github.com/informalsystems/verification/blob/05aa2eed768759eb6ef2537a51aa419f404ca354/spec/light-client/Blockchain.tla#L236

They all pass. This is on develop branch.

konnov commented 4 years ago

I have added the script check-blockchain.sh that checks the properties NeverStuck, NeverStuckFalse2, NeverStuckFalse1, and NeverUltimateHeight. The first one holds true and the last two are violated. The property NeverStuckFalse2 is unexpectedly violated. As a result, a block can be added, even though the last block is not trusted anymore.

We should understand, whether NeverStuckFalse2 is expected to be violated or not.

konnov commented 4 years ago

For some reason, TLA+ Toolbox failed on Blockchain.tla. Perhaps, I have to re-install it. The script should work without any problem though.

josef-widder commented 4 years ago

It is a corner case that corresponds to the case where no block has been added for two weeks or so. In my understanding (which I have written in the first draft of the Blockchain English spec), more than 2/3 are correct until the trusting period and until the next block is added. Normally the first condition kicks in, but if consensus does not terminate the second one applies. Then, my current understanding is that the TLA+ spec currently only captures the condition on the trusting period.

In any case, this corner case raises questions for the light client. We should understand whether sequential verification would be acceptable if two subsequent blocks are 3 weeks apart. It would be interesting to understand how applications handle unbonding in this case. I am not sure anyone has considered that by now?

ebuchman commented 4 years ago

Was this addressed?

We should understand whether sequential verification would be acceptable if two subsequent blocks are 3 weeks apart. It would be interesting to understand how applications handle unbonding in this case. I am not sure anyone has considered that by now?

It's great this is coming up, because it's directly related to the attacks by validators that control the timestamp - they can just fast forward it beyond trusting period. This is a big motivation behind moving to proposer-based-time. Issues like this have been discussed in a few contexts like https://github.com/tendermint/tendermint/issues/2653.

josef-widder commented 4 years ago

Thanks for link. I will try to catch-up with the discussion there, then we should coordinate how to treat the case of blocks being 3 weeks apart. And you are right, if the time on the blocks is subject to faults, this is not just a theoretical question.

I am not sure what is the state w.r.t. the TLA+ spec. Perhaps we should move the issue to tendermint-rs since the blockchain model is now part of https://github.com/informalsystems/tendermint-rs/pull/314/

For the viewpoint of the light clients, if two blocks are 3 weeks apart, we cannot do much, as trust in the old header is lost.

milosevic commented 4 years ago

Is unbonding period in Gaia hybrid, i.e., number of blocks and elapsed time? @cwgoes

cwgoes commented 4 years ago

Is unbonding period in Gaia hybrid, i.e., number of blocks and elapsed time? @cwgoes

Yes. See the SDK x/evidence code.

milosevic commented 4 years ago

Thanks Chris. This is evidence related logic. Is there an explicit unbonding period computation or it is only defined with respect to the evidence validity logic?

cwgoes commented 4 years ago

Thanks Chris. This is evidence related logic. Is there an explicit unbonding period computation or it is only defined with respect to the evidence validity logic?

I'm not quite sure what you mean by "explicit" - there is separate logic in Tendermint (which handles expiry of evidence from gossip, not slashing itself) - both parts of the unbonding period are kept in the consensus parameters (this line), so they are explicitly represented there, but as separate variables.

milosevic commented 4 years ago

By explicit logic I mean computing and managing set of validators that are within current unbonding period that is consulted to decide if evidence is still valid or not for example.

cwgoes commented 4 years ago

By explicit logic I mean computing and managing set of validators that are within current unbonding period that is consulted to decide if evidence is still valid or not for example.

Ah yes, the SDK does track this (also for unbonding delegations). Thanks for mentioning it, it reminded me to check, and actually I think this logic needs to be updated - https://github.com/cosmos/cosmos-sdk/issues/6478.