Formal methods on some PoS stuff
In Paris, I received a description of a distributed consensus mechanism. If the description below looks ambiguous or impenetrable, this post is for you. I banged my head to formal verification tools called Alloy and Isabelle/HOL to clarify my understanding (code).
Here is the description:
Message types:
* commit(HASH, view), 0 <= view
* prepare(HASH, view, view_source), -1 <= view_source < view
Slashing conditions:
* [i] commit(H, v) REQUIRES 2/3 prepare(H, v, vs) for some consistent vs
* [ii] prepare(H, v, vs) REQUIRES 2/3 prepare(H_anc, vs, vs') for some consistent vs', where H_anc is a (v-vs)-degree ancestor of H, UNLESS vs = -1
* [iii] commit(X, v) + prepare(Y, w, u) ILLEGAL if u < v < w, EVEN IF X = Y
* [iv] prepare(X1, v, vs1) + prepare(X2, v, vs2) ILLEGAL unless X1 = X2 and vs1 = vs2
If it’s vague for you, read on. Or, otherwise, if you believe you understand everything, this post is for you too because I can show you many hidden assumptions.
To me the whole thing was vague. Somehow I figured:
- the whole description would be used by a node at a point of time, to determine the set of slashed nodes;
- at any point of time, the node sees some messages that have been signed by nodes;
- the whole situation is about the set of messages visible;
- the number of all nodes is known, and perhaps is fixed;
- “2/3 prepare(H, v, vs)” would mean at least two-thirds of the nodes have signed “prepare(H, v, vs)”;
- other messages that are not prefixed with ‘2/3’ are signed by the node under consideration for slashing; ‘commit(X, v) + prepare(Y, w, u)’ probably means that the same node has signed two messages.
Still, there are ambiguities inherent in natural languages. For examples, “REQUIRES 2/3 prepare(H, v, vs) for some consistent vs” can require two-thirds to sign the same message, or possibly, can be satisfied by 2/3 of the nodes signing various messages containing different vs’s. I guessed that the former is the case (later confirmed somehow) because these mechanisms usually are justified by an argument “2/3 doing A and 2/3 doing B imply 1/3 doing both”. For this form of arguments to work, having two-thirds of the nodes doing the same thing sounds very useful.
The worst part of all this: I’m still unsure if I have explained everything. Any sentence somehow assumes knowledge, and the assumptions are in the background. I guess that’s how people’s mind works. That’s why I bang my head against interactive theorem provers.
I also received two desired properties of the mechanism.
- Accountable safety: if two hashes are committed, and the two hashes are not in descendant-ancestor relation, at least one-third of the nodes are slashed.
- Plausible liveness: if less than one-third of the nodes are slashed, the remaining two-thirds can commit new hashes.
I guessed plausible liveness also requires the two-thirds to remain unslashed.
Starting from this vagueness, below is how to get a complete understanding.
I was not sure if I can start typing the correct logical formulas in theorem provers, so I turned to a tool called Alloy. Alloy is a modeling tool, or a logical prototyping tool. Alloy can take incomplete descriptions and incorrect desired properties, and it draws counter-examples as pictures. Alloy does not guarantee the desired properties for unlimitedly large examples, but Alloy is good for testing one’s understanding against. Its quick response brings many aha moments.
In my git repository, I’ve stored those aha moments:
I had just told Alloy that a Prepare message has a hash and two views. And Alloy came up with this example. Now, I see a view’s previous view is itself. That should not happen. So I added
fact {
no x : View | x in x.(^v_prev)
}meaning “no View should be its own ancestor.”
Then I told Alloy about Hashes, and Commit messages. Somehow I chose to model (h, v) pairs as Hashes (because otherwise, I needed to keep track of pairs of Hashes and Views, which crowds the example drawings unnecessarily). I started talking as if a Hash belong to a View (I had some good justifications in mind if anybody asks). Then Alloy came up with this example:
Yes, a hash’s previous hash should belong to the previous view of the original hash:
fact prev_does_not_match {
all h : Hash |
h.h_prev.h_view = h.h_view.v_prev
}The graphs started resembling protocol executions, so I started asking Alloy if accountable safety can be violated. And yes:
Accountable safety was broken because I forgot to say that Views are in total order.
fact {
all v0, v1 : View | v0 in v1.(*v_prev) or v1 in v0.(*v_prev)
}Literally, this says “for all Views v0 and v1, at least one of these hold: v0 is an ancestor-or-self of v1, or v1 is an ancestor-or-self of v0”.
After adding these conditions, I get closer to the correct description of the protocol. The closer I get, Alloy comes up with bigger, annoying examples.
I made a mistake in slashing condition [ii]. The condition requires existence of some previous Prepare messages that belong to a particular view, but I forgot to say this.
fact {
all p : Prepare |
(p.p_sender in SaneNode && some p.p_view_src.v_prev) implies
some h_anc : Hash | some v_src : View |
- h_anc in p.p_hash.(^h_prev) &&
+ h_anc in p.p_hash.(^h_prev) && h_anc.h_view = p.p_view_src &&
(#{n : Node | some p' : Prepare | p'.p_sender = n && p'.p_hash = h_anc && p'.p_view_src = v_src }). mul[ 3] >= (#{n : Node}).mul[ 2 ]
}After I fix these, Alloy cannot break accountable safety. Also, when I break the slashing conditions intensionally, Alloy can almost always find a way to break accountable safety. That’s very good because I cleared the fog of “did I explain everything?” I have explained everything to a computer program, I guess.
Alloy is also great for experimenting new slashing conditions. What about 2/5 instead of 1/3? Alloy instantly finds a counterexample with one honest node with two slashed nodes.
However, Alloy does not give the final guarantee. It just finds small counterexample containing at most a dozen boxes.
The slashing conditions are designed to work with many hashes and some number of nodes. The desired properties should hold for an arbitrary number of nodes or hashes or views. Machine-checked proofs (which Isabelle, Coq and HOL systems check) give better guarantee than bounded model checking (which Alloy offers).
After a couple of days work, I managed to prove the two properties. The Isabelle/HOL development forced me to spell out every single assumption. For instance, the number of nodes is finite. Another assumption: only finitely many messages have been signed. Another assumption: a hash’s descendant is always found. These are usually forgotten assumptions, but now I have told everything in the Isabelle theory.
The statements of thereoms should be somehow readable, so I list them here. Note: ‘⟹’ stands for implication; ‘A ⟹ B ⟹ C’ says “A implies (B implies C)”. Also ‘∧’ stands for conjunction; ‘A ∧ B’ says “A and B”.
lemma accountable_safety :
situation_has_finitely_many_nodes s ⟹
committed s x ⟹ committed s y ⟹
not_on_same_chain s x y ⟹ one_third_slashed s
The accountable safety says: for any situation (containing nodes and messages), if the situation has finitely many nodes, and if two hashes x and y are committed in the situation, and if these hashes are not on the same chain, at least one-third of the nodes are slashed in the situation.
lemma plausible_liveness:
"situation_has_finitely_many_nodes s ⟹
no_invalid_view s ⟹
new_descendant_available s ⟹
finite_messages s ⟹
¬ one_third_slashed s ⟹
∃ s_new h_new.
¬ committed s h_new ∧
unslashed_can_extend s s_new ∧
committed s_new h_new ∧
no_new_slashed s s_new"
The plausible liveness says: for any situation with finitely many nodes, if no messages contain invalid view (i.e. we have ignored all messages like Prepare (h, -2, -1)), new hashes are always available after any hash, if the situation does not contain infinitely many messages, if less than one-third of the nodes are slashed, there exists a situation s_new with a hash h_new. Moreover, the hash h_new is not committed in situation s but in s_new. The situation s_new can be reached from situation s, just by unslashed nodes sending messages. In the new situation, no nodes are slashed unless they are already slashed in the original situation.
I don’t have neat pictures out of the Isabelle/HOL development. I can offer a PDF document, which should be slightly more readable than the source. To be honest, I want to brush up the proofs and annotate each lemma before anybody looks at it. I can tell you some impression. For me the accountable safety was easier because it follows some tight line of reasoning. In contrast, the proof of plausible liveness has so much slack space, e.g. you can choose whichever new hash and whichever relatively new views. The freedom makes life a bit harder.
To put this kind of mechanism into cryptoeconomic uses, it’s important to enumerate all the ways things can fail. I guess formal methods help there. Anyway properties like these take only under a week to verity, so why not.
On similar topics, I found more serious efforts using Isabelle/HOL, and some automation that involves extending SMT solvers.
