# Lightclient Attackers Isolation
Warning: This is the beginning of an unfinished draft. Don't continue reading!
Adversarial nodes may have the incentive to lie to a lightclient about the state of a Tendermint blockchain. An attempt to do so is called attack. Light client verification (opens new window) checks incoming data by checking a so-called "commit", which is a forwarded set of signed messages that is (supposedly) produced during executing Tendermint consensus. Thus, an attack boils down to creating and signing Tendermint consensus messages in deviation from the Tendermint consensus algorithm rules.
As Tendermint consensus and light client verification is safe under the assumption of more than 2/3 of correct voting power per block [TMBC-FM-2THIRDS] (opens new window), this implies that if there was an attack then [TMBC-FM-2THIRDS] (opens new window) was violated, that is, there is a block such that
- validators deviated from the protocol, and
- these validators represent more than 1/3 of the voting power in that block.
In the case of an attack (opens new window), the lightclient attack detection mechanism (opens new window) computes data, so called evidence [LC-DATA-EVIDENCE.1] (opens new window), that can be used
- to proof that there has been attack [TMBC-LC-EVIDENCE-DATA.1] (opens new window) and
- as basis to find the actual nodes that deviated from the Tendermint protocol.
This specification considers how a full node in a Tendermint blockchain can isolate a set of attackers that launched the attack. The set should satisfy
- the set does not contain a correct validator
- the set contains validators that represent more than 1/3 of the voting power of a block that is still within the unbonding period
# Outline
TODO when preparing a version for broader review.
# Part I - Basics
For definitions of data structures used here, in particular LightBlocks [LCV-DATA-LIGHTBLOCK.1] (opens new window), cf. Light Client Verification (opens new window).
# Part II - Definition of the Problem
The specification of the detection mechanism (opens new window) describes
- what is a light client attack,
- conditions under which the detector will detect a light client attack,
- and the format of the output data, called evidence, in the case an attack is detected. The format is defined in [LC-DATA-EVIDENCE.1] (opens new window) and looks as follows
The isolator is a function that gets as input evidence ev
and a prefix of the blockchain bc
at least up to height ev.ConflictingBlock.Header.Height + 1
. The output is a set of peerIDs of validators.
We assume that the full node is synchronized with the blockchain and has reached the height ev.ConflictingBlock.Header.Height + 1
.
# [FN-INV-Output.1]
When an output is generated it satisfies the following properties:
- If
bc[CommonHeight].bfttime
is within the unbonding period w.r.t. the time at the full node,ev.ConflictingBlock.Header != bc[ev.ConflictingBlock.Header.Height]
- Validators in
ev.ConflictingBlock.Commit
represent more than 1/3 of the voting power inbc[ev.CommonHeight].NextValidators
- Then: A set of validators in
bc[CommonHeight].NextValidators
that- represent more than 1/3 of the voting power in
bc[ev.commonHeight].NextValidators
- signed Tendermint consensus messages for height
ev.ConflictingBlock.Header.Height
by violating the Tendermint consensus protocol.
- represent more than 1/3 of the voting power in
- Else: the empty set.
# Part IV - Protocol
Here we discuss how to solve the problem of isolating misbehaving processes. We describe the function isolateMisbehavingProcesses
as well as all the helping functions below. In Part V, we discuss why the solution is complete based on result from analysis with automated tools.
# Isolation
# Outline
Describe solution (in English), decomposition into functions, where communication to other components happens.
# [LCAI-FUNC-MAIN.1]
- Implementation comment
- If the full node has only reached height
ev.conflictingBlock.Header.Height
thenbc[ev.conflictingBlock.Header.Height + 1].Header.LastCommit
refers to the locally stored commit for this height. (This commit must be present by the precondition onlength(bc)
.) - We check in the precondition that the unbonding period is not expired. However, since time moves on, before handing the validators over Cosmos SDK, the time needs to be checked again to satisfy the contract which requires that only bonded validators are reported. This passing of validators to the SDK is out of scope of this specification.
- If the full node has only reached height
- Expected precondition
length(bc) >= ev.conflictingBlock.Header.Height
ValidAndVerifiedUnbonding(bc[ev.CommonHeight], ev.ConflictingBlock) == SUCCESS
ev.ConflictingBlock.Header != bc[ev.ConflictingBlock.Header.Height]
- TODO: input light blocks pass basic validation
- Expected postcondition
- [FN-INV-Output.1] holds
- Error condition
- returns an error if precondition is violated.
# Details of the Functions
# [LCAI-FUNC-VVU.1]
- Conditions are identical to [LCV-FUNC-VALID.2] (opens new window) except the precondition "trusted.Header.Time > now - trustingPeriod" is substituted with
trusted.Header.Time > now - UnbondingPeriod
# [LCAI-FUNC-NONVALID.1]
- Implementation remarks
- checks whether the evidence header
ev
violates the validity property of Tendermint Consensus, by checking agains a reference header
- checks whether the evidence header
- Expected precondition
ref.Height == ev.Height
- Expected postcondition
- returns evaluation of the following disjunction
[[LCAI-NONVALID-OUTPUT.1]] ==
ref.ValidatorsHash != ev.ValidatorsHash
or
ref.NextValidatorsHash != ev.NextValidatorsHash
or
ref.ConsensusHash != ev.ConsensusHash
or
ref.AppHash != ev.AppHash
or
ref.LastResultsHash != ev.LastResultsHash
- returns evaluation of the following disjunction
- Implementation remarks TODO: What should we do here? Refer to the accountability doc?
- Expected postcondition TODO: What should we do here? Refer to the accountability doc?
- Expected precondition
commit
is well-formed. In particular all votes are from the same roundr
.
- Expected postcondition
- returns round
r
that is encoded in all the votes of the commit
- returns round
- Expected postcondition
- returns all validator addresses in
commit
- returns all validator addresses in
- Expected postcondition
- returns all validator addresses in
vals
- returns all validator addresses in
# Part V - Completeness
As discussed in the beginning of this document, an attack boils down to creating and signing Tendermint consensus messages in deviation from the Tendermint consensus algorithm rules.
The main function isolateMisbehavingProcesses
distinguishes three kinds of wrongly signing messages, namely,
- lunatic: signing invalid blocks
- equivocation: double-signing valid blocks in the same consensus round
- amnesia: signing conflicting blocks in different consensus rounds, without having seen a quorum of messages that would have allowed to do so.
The question is whether this captures all attacks.
First observe that the first checking in isolateMisbehavingProcesses
is violatesTMValidity
. It takes care of lunatic attacks. If this check passes, that is, if violatesTMValidity
returns FALSE
this means that [FN-NONVALID-OUTPUT] evaluates to false, which implies that ref.ValidatorsHash = ev.ValidatorsHash
. Hence after violatesTMValidity
, all the involved validators are the ones from the blockchain. It is thus sufficient to analyze one instance of Tendermint consensus with a fixed group membership (set of validators). Also it is sufficient to consider two different valid consensus values, that is, binary consensus.
TODO we have analyzed Tendermint consensus with TLA+ and have accompanied Galois in an independent study of the protocol based on Ivy proofs (opens new window).
# References
[supervisor (opens new window)] The specification of the light client supervisor.
[verification (opens new window)] The specification of the light client verification protocol
[detection (opens new window)] The specification of the light client attack detection mechanism.