Parsec: discussion about Liveness proof

If something is fully asynchronous then it may never reach a decision.

It’s not exactly that but you’re close. We do have an issue with proving Liveness in an asynchronous setting because of a specific part of our algorithm: the concrete coin. It is not theoritically impossible to get liveness in an asynchronous setting. In fact, I am pretty convinced that when we get a bit of time away from the coding and look at the concrete coin again, we can create one that is strictly asynchronous.

The only reason we’re not alarmed about it and trying desperately to fix this part of the algorithm at the moment is because being strictly live in an asynchronous setting may not be necessary to be practically live in an asynchronous setting.

For instance HashGraph has a similar issue (actually, they’ve put less thought into fixing it than we have with our concrete coin, so theirs is more likely to be an issue in practice) but they haven’t bothered trying to address it because they don’t think it’s an issue.
Even the blockchain isn’t asynchronously live in theory, but it doesn’t prevent it from being useful without any use of time.

15 Likes

When it comes to cryptography or mathematics, it’s generally not enough that something “seems” good. Especially if it’s a novel proposition. If there were proof, Vlad wouldn’t just be quiet. He would possibly even promote the tech.

But I’m grateful to Pierre for taking the time to explain some of this stuff non-formally here.

2 Likes

Vlad is sitting on the throne with one of the biggest crypto market cap project, he has alot to lose and don’t want anything to be as good or better than what they are doing. He clearly shows that in the conversation between him and Maidsafe but Parsec was that good that he couldn’t resist give them a compliment, something like “They show more skills than most other crypto project teams”. I think it was his way of saying that they did a realy good job because he is tied to say anything that would compromise Ethereums power position.

4 Likes

If there were proof

We have proofs for our claims in the paper. There is an issue with the liveness proof as discussed here (for now), but the general approach is mathematically proven.

7 Likes

I did a summary of the conversation between Vlad and Maidsafe awhile ago, if you have not read it and want to take a look. Not just another decentralized web whitepaper? - #26 by tobbetj

1 Like

Specifically, we prove Validity, Agreement, Integrity and Termination (aka Liveness). The last one has a hidden syncrhony assumption, which is why we don’t claim to be fully async, but all the rest holds.

These are the properties you need to prove to prove a BFT consensus protocol.

8 Likes

Thanks guys! I was a bit worried there was more to Vlad’s first criticism, but now I guess PARSEC really is solid. Not being a mathematician myself it’s difficult to say. (I have studied a bit of logic, and I did prove 2>1 or something like that for some assignment at uni about 20 years ago. As I recall it required about four handwritten notebook pages. Now I wouldn’t even know where to start. :slight_smile:

4 Likes

14 Likes

Hi,
Quick question please:

Did you get a chance to look at Cosmos-Tendermint Byzantine fault-tolerant (BFT) consensus
(https://cosmos.network) ?

Thanks

@pierrechevalier83 Just need to comment how happy I am to be somewhat close to understand the livness issue. :rofl: When Vlad mentioned it I had to look up the definition of statistical livness. :sweat_smile: I’ve also studied logic and half a year of statistics but I can assure that it was not enough. Remember my bachelor thesis where I was lucky that the examiner was not that expert on statistics. Should have done a multiple panel regression but we had no support so it ended up as a simple cross-section regression. The examiner only commented that maybe 0.6 correlation of some variable could be close to auto-correlation, then i laughed inside my head and thought that maybe if the correlation was over 0.8 then maybe I would consider auto-correlation. Just a funny memory to share. :grinning:

2 Likes

I guess I skipped the spreadsheet stage (except for keeping track of what hen lays her eggs where she’s supposed to, instead of hiding them in the woods). But I have learned how to turn a raccoon dog into a piece of clothing using just a knife and some salt. So also back to basics in its own way. :wink:

6 Likes

2 Likes

Tendermint is a variation of PBFT, from Castro and Liskov, and is not asynchronous (to be more precise without the very weak synchrony assumptions that have Parsec) and not leaderless.

In fact, removing the gossip termination mechanism and the leader election, is quite similar to the consensus that is currently working in the Safe Testnet 2 witch is also inspired of PBFT.

Hi @pierrechevalier83 and all,

To understand the topic of this thread in a bit more layman terms, so firstly this is limited to the consensus algorithm per the https://docs.maidsafe.net/Whitepapers/pdf/PARSEC.pdf paper only right.

I see Vlad’s thoughts here https://twitter.com/VladZamfir/status/1002236364258131968 .

@pierrechevalier83 which is the “hidden synchrony assumption” on termination you mention above?

What was the deal about in the first place even - any real world use of Parsec would need to have some kind of timeout on participants, meaning if you would maintain the participants set constant even on obvious participant timeout, the algorithm would function as long as 3/4 of participants are responsive isn’t it so -

Does Parsec have any locking or blocking special case, or any obvious locking behaviour in situations where still 3/4:s of participants are alive & communicating according to best effort?

(By 3/4:s we mean: In case of 4 nodes, 1 may fail; in case of 7 nodes, 2 may fail; in case of 10 nodes, 3 may fail.)

Pierre you mentioned “to fix this part of the algorithm”, was there anything to fix really, did you fix it?

2 Likes

The issue with the synchrony assumption is related to the way the concrete coin is defined. The risk it presents is that a powerful adversary with the ability to control the scheduler could in theory stall consensus forever, even without owning more than the threshold of malicious nodes (>=1/3).
It is a mostly theoretical attack, but still: one better addressed for soundness of the proofs.
In the latest version of the white paper which is currently undergoing the academic review process, this flaw is addressed (with use of a rigorous common coin).
In the implementation, at the moment we use a predictable common coin, which is also flawed theoretically but not considered a high risk in practice at this stage. It will be replaced with the rigorous common coin in due time.
The predictable common coin is even worse in theory than the concrete coin, but it is really simple to code and helps maintain some invariants which are useful for tests, which is why we went from concrete coin to that while awaiting implementation of the proper common coin.

18 Likes

Hi @pierrechevalier83 ,

Thanks for responding.

Actually what do you mean by the possibility that a malevolent parter could “control the scheduler”, do you mean that that party could gossip especially crafted evil GossipEvent structures that would somehow force the consensus to his choice?

If you have a criterium to detect such a forever-stalling participant, he could be banned. You would obviously already have considered that, meaning this theoretical issue is more subtle and problematic, or?

When do you expect to update your Rust impl and published whitepaper to the rigorous common coin - in terms of complexity for Parsec will this be a very small code update?

Are any more updates planned to Parsec?

Thanks!
Guy

2 Likes

Controlling the scheduler is not about what you gossip, it’s about impacting the timing of communication between honest participants. Say the adversary has a super powerful botnet they use for ddossing half the network. Say it’s enough that this half of the network can’t process receiving communications from the other nodes for a while. These kind of powers can be used to influence the scheduling of messages. The extreme example of this power is full control of the scheduler.

11 Likes

Hi @pierrechevalier83, aha, thank you for clarifying.

Of course in face of perfectly hijacked interconnect, where he exercises perfect control of the delivery order of messages, Parsec will not function.

How does your upcoming rigorous common coin work, what gives it its qualitative difference vs. the current whitepaper & implementation coins?

With the upcoming rigorous common coin, would “control the scheduler” attack no longer stall Parsec, or what’s the point with the rigorous common coin’s introduction?

Also again, do you have any thought about when you will release the updated paper & when implement it, and code-wise is this a very small update

Thanks,
Guy

2 Likes

When we speak of “controlling the scheduler”, the adversary can impose any arbitrary but finite delay in any communication. In a truly asynchronous algo, it shouldn’t affect Liveness, which means that consensus should still eventually be reached.

This is traditionally done by using a common coin which consists of creating a common unpredictable value so that by the time such an adversary influences the communication timing, they don’t have enough information to do so effectively (in fact, no-one can because the coin could fall either way).

For the timing: the whitepaper update is “order of months” (academia timescales).
For the PARSEC update, it will be a small to medium size task once BLS support is implemented (which is one of the active milestones). It isn’t high priority as far as I know, but you should ask the current team for updates (like @Jean-Philippe or @bart for instance) as I’ve moved on to a different job.

11 Likes

Really appreciate you taking the time to clarify things even after moving on. That’s quite awesome of you.

9 Likes