Computing attack types (#232)

Add light attack evidence handling

rust-spec/lightclient/README.md

@@ -10,12 +10,15 @@ with a trusted header and validator set. The light client
 protocol allows a client to then securely update its trusted state by requesting and
 verifying a minimal set of data from a network of full nodes (at least one of which is correct).
 
-The light client is decomposed into three components:
+The light client is decomposed into two main components:
 
-- Commit Verification - verify signed headers and associated validator
+- [Commit Verification](#Commit-Verification) - verify signed headers and associated validator
   set changes from a single full node, called primary
-- Fork Detection -  verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of forks)
-- Fork Accountability - given a fork, which validators are responsible for it.
+- [Attack Detection](#Attack-Detection) -  verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of a lightclient attack)
+
+In case a lightclient attack is detected, the lightclient submits evidence to a full node which is responsible for "accountability", that is, punishing attackers:
+
+- [Accountability](#Accountability) - given evidence for an attack, compute a set of validators that are responsible for it.
 
 ## Commit Verification
 
@@ -175,10 +178,23 @@ All lines in `results.csv` should report `Error`.
 
 The detailed experimental results are to be added soon.
 
-## Fork Accountability
+## Accountability
+
+
+The [English specification](attacks/isolate-attackers_002_reviewed.md) 
+defines the protocol that is executed on a full node upon receiving attack [evidence](detection/detection_003_reviewed.md#tmbc-lc-evidence-data1) from a lightclient. In particular, the protocol handles three types of attacks
+- lunatic
+- equivocation
+- amnesia
+
+As is discussed in the [last part](attacks/isolate-attackers_002_reviewed.md#Part-III---Completeness) of the English specification, computer-aided analysis of  [Tendermint Consensus in TLA+][tendermint-accountability] shows that these three types capture all possible attacks.
+
+
+The [TLA+ specification](attacks/Isolation_001_draft.tla)
+is a formal description of the
+protocol, including the safety property, which can be model checked with Apalache.
 
-There is no English specification yet. TODO: Jovan's work?
+Similar to the other specifications, [MC_5_3.tla](attacks/MC_5_3.tla) contains concrete parameters to run the model checker. The specification can be checked within seconds.
 
-TODO: there is a WIP [TLA+
-specification](https://github.com/informalsystems/verification/pull/13) in the
-verification repo that should be moved over here.
+[tendermint-accountability]:
+https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md

rust-spec/lightclient/attacks/isolate-attackers_002_reviewed.md

@@ -0,0 +1,221 @@
+# Lightclient Attackers Isolation
+
+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][verification] 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]][TMBC-FM-2THIRDS-link], this implies that if there was an attack then [[TMBC-FM-2THIRDS]][TMBC-FM-2THIRDS-link] 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][node-based-attack-characterization], the lightclient [attack detection mechanism][detection] computes data, so called evidence [[LC-DATA-EVIDENCE.1]][LC-DATA-EVIDENCE-link], that can be used 
+- to proof that there has been attack [[TMBC-LC-EVIDENCE-DATA.1]][TMBC-LC-EVIDENCE-DATA-link] 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
+
+After providing the [problem statement](#Part-I---Basics-and-Definition-of-the-Problem), we specify the [isolator function](#Part-II---Protocol) and close with the discussion about its [correctness](#Part-III---Completeness) which is based on computer-aided analysis of Tendermint Consensus.
+
+# Part I - Basics and Definition of the Problem
+
+For definitions of data structures used here, in particular LightBlocks [[LCV-DATA-LIGHTBLOCK.1]](https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-data-lightblock1), we refer to the specification of [Light Client Verification][verification].
+
+
+The specification of the [detection mechanism][detection] 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]][LC-DATA-EVIDENCE-link] and looks as follows
+
+```go
+type LightClientAttackEvidence struct {
+    ConflictingBlock   LightBlock
+    CommonHeight       int64
+}
+```
+
+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`.
+
+
+#### **[LCAI-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 in `bc[ev.CommonHeight].NextValidators`
+- Then: The output is 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.
+- Else: the empty set.
+
+
+# Part II - 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 III](#part-III---Completeness), we discuss why the solution is complete based on result from analysis with automated tools.
+
+## Isolation
+
+### Outline
+
+We first check whether the conflicting block can indeed be verified from the common height. We then first check whether it was a lunatic attack (violating validity). If this is not the case, we check for equivocation. If this also is not the case, we start the on-chain [accountability protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
+
+#### **[LCAI-FUNC-MAIN.1]**
+```go
+func isolateMisbehavingProcesses(ev LightClientAttackEvidence, bc Blockchain) []ValidatorAddress {
+
+    reference := bc[ev.conflictingBlock.Header.Height].Header
+    ev_header := ev.conflictingBlock.Header
+
+    ref_commit := bc[ev.conflictingBlock.Header.Height + 1].Header.LastCommit // + 1 !!
+    ev_commit := ev.conflictingBlock.Commit
+
+    if violatesTMValidity(reference, ev_header) {
+        // lunatic light client attack
+        signatories := Signers(ev.ConflictingBlock.Commit)
+        bonded_vals := Addresses(bc[ev.CommonHeight].NextValidators)
+        return intersection(signatories,bonded_vals)
+
+    } 
+    // If this point is reached the validator sets in reference and ev_header are identical
+    else if RoundOf(ref_commit) == RoundOf(ev_commit) {
+        // equivocation light client attack
+        return intersection(Signers(ref_commit), Signers(ev_commit))
+    } 
+    else {
+        // amnesia light client attack 
+        return IsolateAmnesiaAttacker(ev, bc)
+    } 
+}
+```
+- Implementation comment
+    - If the full node has only reached height `ev.conflictingBlock.Header.Height` then `bc[ev.conflictingBlock.Header.Height + 1].Header.LastCommit` refers to the locally stored commit for this height. (This commit must be present by the precondition on `length(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.
+- Expected precondition
+    - `length(bc) >= ev.conflictingBlock.Header.Height`
+    - `ValidAndVerifiedUnbonding(bc[ev.CommonHeight], ev.ConflictingBlock) == SUCCESS`
+    - `ev.ConflictingBlock.Header != bc[ev.ConflictingBlock.Header.Height]`
+    - `ev.conflictingBlock` satisfies basic validation (in particular all signed messages in the Commit are from the same round)
+- Expected postcondition
+    - [[FN-INV-Output.1]](#FN-INV-Output1) holds
+- Error condition 
+    - returns an error if precondition is violated.
+
+
+### Details of the Functions
+
+#### **[LCAI-FUNC-VVU.1]**
+```go
+func ValidAndVerifiedUnbonding(trusted LightBlock, untrusted LightBlock) Result
+```
+- Conditions are identical to [[LCV-FUNC-VALID.2]][LCV-FUNC-VALID.link] except the precondition "*trusted.Header.Time > now - trustingPeriod*" is substituted with
+    - `trusted.Header.Time > now - UnbondingPeriod`
+
+#### **[LCAI-FUNC-NONVALID.1]**
+```go
+func violatesTMValidity(ref Header, ev Header) boolean
+```
+- Implementation remarks
+    - checks whether the evidence header `ev` violates the validity property of Tendermint Consensus, by checking against a reference 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`
+
+
+```go
+func IsolateAmnesiaAttacker(ev LightClientAttackEvidence, bc Blockchain) []ValidatorAddress 
+```
+- Implementation remarks
+    - This triggers the [query/response protocol](https://docs.google.com/document/d/11ZhMsCj3y7zIZz4udO9l25xqb0kl7gmWqNpGVRzOeyY/edit).
+- Expected postcondition
+    - returns attackers according to [LCAI-INV-Output.1].
+
+```go
+func RoundOf(commit Commit) []ValidatorAddress 
+```
+- Expected precondition
+    - `commit` is well-formed. In particular all votes are from the same round `r`.
+- Expected postcondition
+    - returns round `r` that is encoded in all the votes of the commit
+- Error condition
+    - reports error if precondition is violated
+
+```go
+func Signers(commit Commit) []ValidatorAddress 
+```
+- Expected postcondition
+    - returns all validator addresses in `commit`
+
+```go
+func Addresses(vals Validator[]) ValidatorAddress[]
+```
+- Expected postcondition
+    - returns all validator addresses in `vals`
+
+
+
+# Part III - 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 signed 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 check in `isolateMisbehavingProcesses` is `violatesTMValidity`. It takes care of lunatic attacks. If this check passes, that is, if `violatesTMValidity` returns `FALSE` this means that [[LCAI-NONVALID-OUTPUT.1]](#LCAI-FUNC-NONVALID1]) 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, as we have two different blocks for the same height, it is sufficient to consider two different valid consensus values, that is, binary consensus.
+
+For this fixed group membership, we have analyzed the attacks using the TLA+ specification of [Tendermint Consensus in TLA+][tendermint-accountability]. We checked that indeed the only possible scenarios that can lead to violation of agreement are **equivocation** and **amnesia**. An independent study by Galois of the protocol based on [Ivy proofs](https://github.com/tendermint/spec/tree/master/ivy-proofs) led to the same conclusion.
+
+
+
+
+# References
+
+[[supervisor]] The specification of the light client supervisor.
+
+[[verification]] The specification of the light client verification protocol.
+
+[[detection]] The specification of the light client attack detection mechanism.
+
+[[tendermint-accountability]]: TLA+ specification to check the types of attacks
+
+[tendermint-accountability]:
+https://github.com/tendermint/spec/blob/master/rust-spec/tendermint-accountability/README.md
+
+[supervisor]: 
+https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/supervisor/supervisor_001_draft.md
+
+[verification]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md
+
+[detection]: 
+https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md
+
+
+[LC-DATA-EVIDENCE-link]: 
+https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#lc-data-evidence1
+
+[TMBC-LC-EVIDENCE-DATA-link]:
+https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#tmbc-lc-evidence-data1
+
+[node-based-attack-characterization]:
+https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/detection/detection_003_reviewed.md#node-based-characterization-of-attacks
+
+[TMBC-FM-2THIRDS-link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#tmbc-fm-2thirds1
+
+[LCV-FUNC-VALID.link]: https://github.com/tendermint/spec/blob/master/rust-spec/lightclient/verification/verification_002_draft.md#lcv-func-valid2

rust-spec/tendermint-accountability/001indinv-apalache.csv

@@ -0,0 +1,13 @@
+no,filename,tool,timeout,init,inv,next,args
+1,MC_n4_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+2,MC_n4_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+3,MC_n5_f1.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+4,MC_n5_f2.tla,apalache,10h,TypedInv,TypedInv,,--length=1 --cinit=ConstInit
+5,MC_n4_f1.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
+6,MC_n4_f2.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
+7,MC_n5_f1.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
+8,MC_n5_f2.tla,apalache,20h,Init,TypedInv,,--length=0 --cinit=ConstInit
+9,MC_n4_f1.tla,apalache,20h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+10,MC_n4_f2.tla,apalache,20h,TypedInv,Accountability,,--length=0 --cinit=ConstInit
+11,MC_n5_f1.tla,apalache,20h,TypedInv,Agreement,,--length=0 --cinit=ConstInit
+12,MC_n5_f2.tla,apalache,20h,TypedInv,Accountability,,--length=0 --cinit=ConstInit

rust-spec/tendermint-accountability/MC_n4_f1.tla

@@ -0,0 +1,22 @@
+----------------------------- MODULE MC_n4_f1 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence, action 
+
+INSTANCE TendermintAccDebug_004_draft WITH
+  Corr <- {"c1", "c2", "c3"},
+  Faulty <- {"f1"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

rust-spec/tendermint-accountability/MC_n4_f2.tla

@@ -0,0 +1,22 @@
+----------------------------- MODULE MC_n4_f2 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
+
+INSTANCE TendermintAccDebug_004_draft WITH
+  Corr <- {"c1", "c2"},
+  Faulty <- {"f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

rust-spec/tendermint-accountability/MC_n4_f2_amnesia.tla

@@ -0,0 +1,40 @@
+---------------------- MODULE MC_n4_f2_amnesia -------------------------------
+EXTENDS Sequences
+
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
+
+\* the variable declared in TendermintAccTrace3
+VARIABLE
+  toReplay
+
+\* old apalache annotations, fix with the new release
+a <: b == a  
+
+INSTANCE TendermintAccTrace_004_draft WITH
+  Corr <- {"c1", "c2"},
+  Faulty <- {"f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2,
+  Trace <- <<
+    "UponProposalInPropose",
+    "UponProposalInPrevoteOrCommitAndPrevote",
+    "UponProposalInPrecommitNoDecision",
+    "OnRoundCatchup", 
+    "UponProposalInPropose",
+    "UponProposalInPrevoteOrCommitAndPrevote",
+    "UponProposalInPrecommitNoDecision"
+  >> <: Seq(STRING)
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================    

rust-spec/tendermint-accountability/MC_n4_f3.tla

@@ -0,0 +1,22 @@
+----------------------------- MODULE MC_n4_f3 -------------------------------
+CONSTANT Proposer \* the proposer function from 0..NRounds to 1..N
+
+\* the variables declared in TendermintAcc3
+VARIABLES
+  round, step, decision, lockedValue, lockedRound, validValue, validRound,
+  msgsPropose, msgsPrevote, msgsPrecommit, evidence, action
+
+INSTANCE TendermintAccDebug_004_draft WITH
+  Corr <- {"c1"},
+  Faulty <- {"f2", "f3", "f4"},
+  N <- 4,
+  T <- 1,
+  ValidValues <- { "v0", "v1" },
+  InvalidValues <- {"v2"},
+  MaxRound <- 2
+
+\* run Apalache with --cinit=ConstInit
+ConstInit == \* the proposer is arbitrary -- works for safety
+  Proposer \in [Rounds -> AllProcs]
+
+=============================================================================