Requirements for Fork Detection in IBC + Accountability (#424)

* start of so-called accountability

* more thoughts

* requirements

* ready to be discussed

* Update docs/spec/lightclient/detection/req-ibc-detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update docs/spec/lightclient/detection/req-ibc-detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update docs/spec/lightclient/detection/req-ibc-detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update docs/spec/lightclient/detection/req-ibc-detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* Update docs/spec/lightclient/detection/req-ibc-detection.md

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

* one of Zarko's comments + md clean-up

Co-authored-by: Zarko Milosevic <zarko@informal.systems>

docs/spec/lightclient/detection/req-ibc-detection.md

@@ -0,0 +1,296 @@
+# Requirements for Fork Detection in the IBC Context
+
+
+## What you need to know about IBC
+
+In the following, I distilled what I considered relevant from
+
+https://github.com/cosmos/ics/tree/master/spec/ics-002-client-semantics
+
+### Components and their interface 
+
+#### Tendermint Blockchains
+
+> I assume you know what that is.
+
+#### Handler
+
+A blockchain runs a **handler** that passively collects information about
+  other blockchains. It can be thought of a state machine that takes
+  input events.
+
+- the state includes a lightstore (I guess called `ConsensusState`
+  in IBC)
+
+- The following function is used to pass a header to a handler
+
+```go
+type checkValidityAndUpdateState = (Header) => Void
+```
+
+  For Tendermint, it will perform
+  `ValidandVerified`, that is, it does the trusting period check and the
+  +1/3 check (+2/3 for sequential headers). 
+  If it verifies a header, it adds it to its lightstore,
+  if it does not pass verification it drops it.
+  Right now it only accepts a header more recent then the latest
+  header,
+  and drops older
+  ones or ones that could not be verified. 
+
+> The above paragraph captures what I believe what is the current
+  logic of `checkValidityAndUpdateState`. It may be subject to
+  change. E.g., maintain a lightstore with state (unverified, verified)
+
+- The following function is used to pass  "evidence" (this we
+  will need to make precise eventually) to a handler
+
+```go
+type checkMisbehaviourAndUpdateState = (bytes) => Void
+```
+     
+  We have to design this, and the data that the handler can use to
+  check that there was some misbehavior (fork) in order react on
+  it, e.g., flagging a situation and
+  stop the protocol. 
+
+- The following function is used to query the light store (`ConsensusState`)
+
+```go
+type queryChainConsensusState = (height: uint64) => ConsensusState
+```
+
+#### Relayer
+
+- The active components are called **relayer**. 
+
+- a relayer contains light clients to two (or more?) blockchains
+
+- the relayer send headers and data to the handler to invoke
+  `checkValidityAndUpdateState` and
+  `checkMisbehaviourAndUpdateState`. It may also query
+  `queryChainConsensusState`.
+
+- multiple relayers may talk to one handler. Some relayers might be 
+  faulty. We assume existence of at least single correct relayer.
+
+
+## Informal Problem Statement: Fork detection in IBC
+
+### Relayer requirement: Evidence for Handler
+
+- The relayer should provide the handler with
+  "evidence" that there was a fork. 
+
+- The relayer can read the handler's consensus state. Thus the relayer can
+  feed the handler precisely the information the handler needs to detect a
+  fork. 
+  What is this
+  information needs to be specified.
+
+- The information depends on the verification the handler does. It
+  might be necessary to provide a bisection proof (list of
+  lightblocks) so that the handler can verify based on its local
+  lightstore a header *h* that is conflicting with a header *h'* in the
+  local lightstore, that is, *h != h'* and *h.Height = h'.Height*
+
+### Relayer requirement: Fork detection
+
+Let's assume there is a fork at chain A. There are two ways the
+relayer can figure that out:
+
+1. as the relayer contains a light client for A, it also includes a fork
+   detector that can detect a fork.
+
+2. the relayer may also detect a fork by observing that the
+   handler for chain A (on chain B)
+   is on a different branch than the relayer
+
+
+- in both detection scenarios, the relayer should submit evidence to 
+  full nodes of chain A where there is a fork. As we assume a fullnode
+  has a complete list of blocks, it is sufficient to send "Bucky's
+  evidence" (https://github.com/tendermint/tendermint/issues/5083),
+  that is, 
+     - two lightblocks from different branches + 
+	 - a lightblock (perhaps just a height) from which both blocks 
+	   can be verified.
+
+- in the scenario 2., the relayer must feed the A-handler (on chain B)
+  a proof of a fork on A so that chain B can react accordingly
+
+### Handler requirement
+
+- there are potentially many relayers, some correct some faulty
+
+- a handler cannot trust the information provided by the relayer, 
+  but must verify 
+  (Доверя́й, но проверя́й)
+
+- in case of a fork, we accept that the handler temporarily stores
+  headers (tagged as verified). 
+
+- eventually, a handler should be informed
+ (`checkMisbehaviourAndUpdateState`)
+ by some relayer that it has
+  verified a header from a fork. Then the handler should do what is
+ required by IBC in this case (stop?)
+
+### Challenges in the handler requirement
+
+- handlers and relayers work on different lightstores. In principle
+  the lightstore need not intersect in any heights a priori
+
+- if a relayer  sees a header *h* it doesn't know at a handler (`queryChainConsensusState`), the
+  relayer needs to
+  verify that header. If it cannot do it locally based on downloaded
+  and verified (trusted?) light blocks, it might need to use
+  `VerifyToTarget` (bisection). To call `VerifyToTarget` we might keep
+  *h* in the lightstore. If verification fails, we need to download the
+  "alternative" header of height *h.Height* to generate evidence for
+  the handler.
+
+- we have to specify what precisely `queryChainConsensusState`
+  returns. It cannot be the complete lightstore. Is the last header enough?
+
+- we would like to assume that every now and then (smaller than the
+  trusting period) a correct relayer checks whether the handler is on a
+  different branch than the relayer. 
+  And we would like that this is enough to achieve
+  the Handler requirement.
+
+   - here the correctness argument would be easy if a correct relayer is
+     based on a light client with a *trusted* state, that is, a light
+     client who never changes its opinion about trusted. Then if such a
+     correct relayer checks-in with a handler, it will detect a fork, and
+     act in time.
+
+   - if the light client does not provide this interface, in the case of
+     a fork, we need some assumption about a correct relayer being on a
+     different branch than the handler, and we need such a relayer to 
+	 check-in not too late. Also
+     what happens if the relayer's light client is forced to roll-back
+     its lightstore?
+     Does it have to re-check all handlers?
+
+
+
+
+## On the interconnectedness of things
+
+In the broader discussion of so-called "fork accountability" there are
+several subproblems
+
+- Fork detection 
+
+- Evidence creation and submission
+
+- Isolating misbehaving nodes (and report them for punishment over abci)
+
+
+### Fork detection
+
+The preliminary specification ./detection.md formalizes the notion of
+a fork. Roughly, a fork exists if there are two conflicting headers
+for the same height, where both are supported by bonded full nodes
+(that have been validators in the near past, that is, within the
+trusting period). We distinguish between *fork on the chain* where two
+conflicting blocks are signed by +2/3 of the validators of that
+height, and a *light client fork* where one of the conflicting headers
+is not signed by  +2/3 of the current height, but by +1/3 of the
+validators of some smaller height.
+
+In principle everyone can detect a fork
+
+- ./detection talks about the Tendermint light client with a focus on 
+  light nodes. A relayer runs such light clients and may detect 
+  forks in this way
+
+- in IBC, a relayer can see that a handler is on a conflicting branch
+    - the relayer should feed the handler the necessary information so
+      that it can halt
+	- the relayer should report the fork to a full node
+
+### Evidence creation and submission
+
+- the information sent from the relayer to the handler could be called
+  evidence, but this is perhaps a bad idea because the information sent to a
+  full node can also be called evidence. But this evidence might still
+  not be enough as the full node might need to run the "fork
+  accountability" protocol to generate evidence in the form of
+  consensus messages. So perhaps we should
+  introduce different terms for:
+
+  - proof of fork for the handler (basically consisting of lightblocks)
+  - proof of fork for a full node (basically consisting of (fewer) lightblocks)
+  - proof of misbehavior (consensus messages)
+
+
+
+### Isolating misbehaving nodes
+
+- this is the job of a full node. 
+
+- might be subjective in the future: the protocol depends on what the
+  full node believes is the "correct" chain. Right now we postulate
+  that every full node is on the correct chain, that is, there is no
+  fork on the chain.
+
+- The full node figures out which nodes are
+    - lunatic
+	- double signing
+	- amnesic; **using the challenge response protocol**
+
+- We do not punish "phantom" validators
+    - currently we understand a phantom validator as a node that
+	    - signs a block for a height in which it is not in the
+          validator set
+        - the node is not part of the +1/3 of previous validators that
+          are used to support the header. Whether we call a validator
+          phantom might be subjective and depend on the header we
+          check against. Their formalization actually seems not so
+          clear.
+	- they can only do something if there are +1/3 faulty validators
+      that are either lunatic, double signing, or amnesic.
+    - abci requires that we only report bonded validators. So if a
+      node is a "phantom", we would need the check whether the node is
+      bonded, which currently is expensive, as it requires checking
+      blocks from the last three weeks.
+	- in the future, with state sync, a correct node might be
+      convinced by faulty nodes that it is in the validator set. Then
+      it might appear to be "phantom" although it behaves correctly
+
+
+## Next steps
+
+> The following points are subject to my limited knowledge of the
+> state of the work on IBC. Some/most of it might already exist and we
+> will just need to bring everything together.
+
+- "proof of fork for a full node" defines a clean interface between
+  fork detection and misbehavior isolation. So it should be produced
+  by protocols (light client, the relayer). So we should fix that
+  first.
+
+- Given the problems of not having a light client architecture spec,
+  for the relayer we should start with this. E.g.
+
+    - the relayer runs light clients for two chains
+	- the relayer regularly queries consensus state of a handler
+	- the relayer needs to check the consensus state
+	    - this involves local checks
+		- this involves calling the light client
+	- the relayer uses the light client to do IBC business (channels,
+      packets, connections, etc.)
+	- the relayer submits proof of fork to handlers and full nodes
+	  
+> the list is definitely not complete. I think part of this
+> (perhaps all)  is
+> covered by what Anca presented recently.
+	
+We will need to define what we expect from these components
+
+- for the parts where the relayer talks to the handler, we need to fix
+  the interface, and what the handler does
+
+- we write specs for these components.