Quorum_Intersection - a tool for verifying quorum intersection property.

fixxxpoint

Hi Stellar community!
tl;dr I'd like to enter into the SBC for Aug 15th. My project is a tool written in C++ that verifies if a given stellar network configuration satisfies quorum intersection property (defined by https://www.stellar.org/papers/stellar-consensus-protocol.pdf).

I was interested in designing an algorithm for checking if all quorums of the stellar network satisfies the quorum intersection property, which seems to be crucial for the network to operate correctly (https://www.stellar.org/papers/stellar-consensus-protocol.pdf). During my research, I discovered that this problem is NP-complete (complexity of finding disjoint quorums; therefore checking if configuration satisfies QIP is coNP-complete), hence it can be rather difficult to devise an efficient algorithm for it in general. Nevertheless, I tried to invent some method that has a potential to be more efficient than simple enumeration and verification of all subsets of nodes. So, the good thing is that this tool is able to verify current stellar's network configuration (enumeration method won't be able to verify all subsets of a set containing 177 nodes - as per http://stellarbeat.io). This tool can provide some insight into the 'health' of the current network configuration (naturally only if we believe provided data). It also outputs some simple graphviz representation of the network, where nodes are partitioned by their strongly connected components (directed graph defined by quorum sets of nodes). This can be helpful when one tries to declare quorum sets that satisfy quorum intersection property ^[1]. Additionally, I am planning to implement some scoring for nodes based on the idea of pagerank - it can show how 'important' particular nodes are.
I've already finished implementing this tool (except the pagerank part). I'll open source it before Aug 15th.

This work wouldn't be possible without data provided by http://stellarbeat.io - thanks a lot.

[1] easy way of ensuring that all quorums are intersecting is to ensure that:
1) there is a single strongly connected component that is the greatest element of the relation defined by connectivity of strongly connected components
2) make sure that all quorum slices of a node contains more than half of the nodes in its strongly connected component
3) make sure that all of our quorum slices contain at least one node from different strongly connected component
Organizations probably tend to configure their nodes as cliques (with some assumed resilience, e.g. 3 out of 4 nodes) and it seems rather hard to convince somebody to trust you, hence these rules look for me quite natural.

jeffditullio

fixxxpoint nice work! In David Mazieres's talk https://www.youtube.com/watch?v=vmwnhZmEZjc 56:28 he says Stellar Core has some diagnostic mode to help with this. I haven't read the code or seen any docs on it, curious if you looked at it and how your work compares to it? Possibly you could merge some of your work into that feature. Also if you find docs or the LoC for it please let me know where it is.

fixxxpoint

https://github.com/fixxxedpoint/quorum_intersection

fixxxpoint

jeffditullio Thanks! I found something like this: https://github.com/stellar/stellar-core/blob/6964a5ef991d27fbdc1dfab9e90d3f4f03f73df1/src/history/InferredQuorum.cpp#L160 . stellar-core has a command "--checkquorum" (https://github.com/stellar/stellar-core/blob/master/docs/software/commands.md) for executing this method. For me it looks like powerset enumeration, so probably you won't get any answer from it (if your instance saw majority of currently available nodes, i.e. > 100). I use a different method.

fixxxpoint

Simplified description of the used method.
Definitions:
Minimal quorum := a quorum for which non of its proper subsets is also a quorum.

Dependency graph := a directed graph in which vertices represent stellar nodes and edges represent inclusion in quorum sets, i.e. A -> B means node A has node B in one of its quorum sets.

Used properties:
1) Quorum intersection property holds, that is all quorums are intersecting, if and only if all minimal quorums are intersecting.
2) Every minimal quorum is contained in a strongly connected component of network's dependency graph. It is easy to prove.

Algorithm:
1) If the number of strongly connected components of the dependency graph containing a quorum is bigger than 1, return False.
2) Take the only strongly connected component that contains a quorum and enumerate all of its minimal quorums (NOTE: I use a different method than powerset enumeration). You can just enumerate all minimal quorums of size smaller or equal to half of the size of that strongly connected component. While enumerating, check if the complement of that quorum in its strongly connected component also contains a quorum. If so, return False.
3) Return True.

fixxxpoint

I just implemented the PageRank algorithm for the dependency graph of the network.
To try it just use the -p switch (for more details use -h).

tinco

@fixxxpoint this is very nice! I'm trying to find out if I can use the info on http://quorumexplorer.com, I'd like it to be a little more informative than just "yes" or "no" so I'm trying to grok your code. Such a shame you chose to do it in C++ ?

tinco

Hi @fixxxpoint I made a very naieve implementation that finds the largest fully connected set of quorumslices in javascript, it takes about 15 seconds to run on my laptop:

https://github.com/tinco/quorum_explorer/blob/master/src/lib/quorum-intersection.js

I ran your code on a server instance, and it finished in less than a second, so that's a lot faster. What I got from your code is that you find strongly connected components, and then look for quorums in there. I suppose that is a nice heuristic, do you think it's the main reason why your code is so much faster than mine?

If you have the strongly connected components, do you find the quorum by simply dropping nodes from it until you've got a configuration that's a fully connected graph?

Btw, Mr Nicolas pointed me to https://github.com/stellar/stellar-core/blob/master/src/history/InferredQuorum.cpp which seems to be a C++ version that does roughly the same thing as mine does, I've not run it yet, perhaps it's as slow as mine as well.

fixxxpoint

tinco The trick with strongly connected components is not a heuristic (or perhaps we are using different definitions of what a heuristic is), but some heuristic is hidden little bit deeper. Normally, you consider algorithm's complexity parameterized just by the size of the input. You can look at my algorithm as additionally parameterized by the number of different quorums in the smallest strongly connected component. It can be easily proved that all minimal quorums are contained within some strongly connected component and if all quorums are intersecting, then all of the minimal quorums are contained in same strongly connected component. Thanks to this property, you can filter out all other strongly connected components. Based on this experimental code, it appears that all minimal quorums are contained within some very small strongly connected component (you can check it by yourself using the -v switch), namely of size 4. This is currently the main reason why it is so fast. But, generally the problem of finding disjoint quorums is NP-hard. I also tested it on network configurations with bigger main strongly connected component (but with small number of minimal quorums) and its performance was acceptable ?. This small size also means that the current network is very "centralized" and has very low resilience - those 4 nodes have full control of the network and if only 2 of them are down it can block the whole network.

Regarding your second question, this is the place where I used some heuristic. There are several ways of finding all quorums/all minimal quorums. Each can depend on a different parameter of the structure of the network. You can follow quorum slices using some strategy similar to DFS, returning a value every time you find that the current set is a quorum/minimal quorum. If each node has a small number of quorum slices (small quorum sets, big/small thresholds), then this method can be very efficient. Unfortunately, it can also visit same quorums several times. Another way, which I'm using, is a standard enumeration method: you consider all nodes in some order and recursively solve two subproblems - one where you decide to remove a node and another where you decide to leave it in your set. You also maintain two sets, one containing nodes you are going to consider next and other containing all selected nodes. Then you keep track of whether all selected nodes are part of the biggest quorum included in the set of "selected" plus "available" nodes. My heuristic selects which node should be considered next based on how many other nodes are pointing at it (plus some randomization). Luckily, if a node is "popular" it should be in some minimal quorum (but not necessarily). This way I'm trying to process only minimal quorums. The complexity of this method is something like (#of quorums in the main strongly connected component * n^O(1)) (which in worst case can be exponential). Space complexity is linear.

In my previous post I already pointed https://github.com/stellar/stellar-core/blob/master/src/history/InferredQuorum.cpp. This probably has exponential complexity regardless of actual number of quorums. It also looks like it has exponential worst case space complexity, by keeping list of all discovered quorums. Additionally, it also process that list twice, instead of just processing it once and checking complementary for each set. Its complexity looks for me like: time = 2ⁿ * n^O(1) (always), space worst case = O(2ⁿ ).