Skip to content

Latest commit

 

History

History
628 lines (466 loc) · 30.5 KB

L1_2.md

File metadata and controls

628 lines (466 loc) · 30.5 KB
Raw

IBC Connection Handshake (ICS3) English Spec

L1. Problem statement / outside view

Suppose there are two chains (e.g., distributed ledgers) that execute independently of each other. What should be an abstraction for representing a path of communication between the two? We use a connection abstraction to represent this path of communication (see the ICS 003 spec).

The IBC connection handshake protocol, at the highest level of abstraction, enables two chains to establish -- i.e., open -- a connection with each other. Once open, connections cannot be closed, so a closing handshake does not exist. Whenever we speak of connection handshake, we implicitly mean the opening handshake. Throughout the rest of this document, we will often use the abbreviation "ICS3" to stand for connection handshake problem (or protocol, depending on the context).

A connection involves the two parties (the respective chains) involved in the communication, as well as a relayer which handles message transmission between the chains. The relayer carries a central responsibility in handshaking and maintaining a connection. That is, a connection handshake is essentially a three-party protocol: two chains, plus a relayer. This document focuses on the functionality of the two chains, while providing a minimal description of the relayer.

Sequential problem statement

Definitions

A chain comprises three elements that are relevant for connections:

  • a module, or the "connection handshake module" or "ICS3 module": this is a process (running as a component of the chain) which implements the ICS3 protocol;
  • the store of the chain, alternatively called the "consensus state" or just "state" of the chain;
  • a client: a process running on the chain, which represents a window onto the store of the other chain.

We give concrete names, Alice and Bob, to the chains involved in our problem, to simplify description. The diagram below sketches the system model of the connection handshake problem. Note that the client on Alice points to the store on Bob; vice versa is true for the client on Bob (but there is no corresponding arrow to keep the figure cleaner). Alice and Bob have no direct medium for communicating with each other, so a relayer process sits between the two chains and enables their communication (more details on this will follow).

                     IBC Connection Handshake
                        High-level Model
        Alice                               Bob
     +-----------+                     +-----------+
     |   Chain   |     +---------+     |   Chain   |
     |           |<--->| Relayer |<--->|           |
     | +-------+ |     +---------+     | +-------+ |
     | |Module | |                     | |Module | |
     | +-------+ |                     | +-------+ |
     | +-------+ |                     | +-------+ |
     | | Store | |                    -->| Store | |
     | +-------+ |            -------/ | +-------+ |
     |+---------+|   --------/         |+---------+|
     || Client  |---/                  || Client  ||
     |+---------+|                     |+---------+|
     +-----------+                     +-----------+
Problem statement and guarantees

A connection handshake allows, briefly, that the modules on two chains agree on a consistent view of their state (i.e., their store), and each module allocates a new connection associated with this state.

We identify two basic (high-level) requirements that a connection handshake should guarantee:

  • [ICS3-Seq-1-Agreement] If Alice finishes a handshake by opening a new connection c1 with Bob, and Bob finishes the handshake opening the connection c2, then c1 == c2. In other words, if a connection handshake finishes, the two parties have a consistent view of this connection. We say that Alice stores one end of the connection, label c1, and Bob stores the other end of the same connection, label c2.

  • [ICS3-Seq-2-Termination] Eventually, the modules of Alice and Bob should both finish the handshake, opening a connection. Opening a connection means that Alice and Bob both allocate in their local store a new connection.

Requirement [ICS3-Seq-1-Agreement] represents the basic safety guarantee, while [ICS3-Seq-2-Termination] is the basic liveness guarantee we would like to have.

L2. Protocol specification / protocol view

2.1 System model specification

System model

A chain is a deterministic state machine. Each chain may be replicated, i.e., consisting of a replicated state machine (RSM), or it may be a standalone process. As a side note, there are certain requirements a chain must satisfy in practice(e.g., see [ICS 024]); at this level of specification, however, we model each chain as consisting of those three components we described earlier: module, store, and a client.

In ICS3, actors represent entities that may trigger this protocol and provide external feedback to the protocol. To quote from IBC terminology:

An actor, or a user (used interchangeably), is an entity interacting with the IBC protocol. An actor can be a human end-user, a module or smart contract running on a blockchain, or an off-chain relayer process capable of signing transactions. [IBC terminology]

Communication assumptions

A relayer intermediates communication between Alice and Bob. We model communication as a shared mutable state. Each chain exposes an API comprising read, write, as well as a queue (FIFO) functionality. So there are two parts to the communication API:

  1. a read/write store:

    • this holds the entire state of the chain;
    • each module can write to this store, and we primarily concerned with the function setConnection that write a new connection into the store;
    • external processes -- in our case, any relayer -- can read from the store via a function getConnection;

  2. a queue of datagrams, or messages:

    • each module can pop datagrams stored in this queue;
    • external processes (relayers) can push to this queue.

We describe the API in the code snippet below. Connection handshake modules implement this interface. Note that we use the modifiers 'private' and 'public' to denote which API function can be invoked by external processes (e.g., relayer) and which functions are private to the module implementing this interface. The data types (Identifier and ConnectionEnd) are defined below.

type CommunicationLayer interface {
    // Write a new value (a connection) to the local store, indexed by the
    // identifier of the connection on the local party.
    private setConnection(i Identifier, e ConnectionEnd)

    // Relayer invokes this to `read` from a chains' local store.
    public getConnection(i Identifier) -> ConnectionEnd
    
    // Relayer invokes this to append a datagram into a chain's 
    // local store.
    public push("outstandingDatagrams", g Datagram)

    // A module consumes elements from its local store 
    // "outstandingDatagrams".
    private pop("outstandingDatagrams") -> Datagram
    // The typical use case is that for each datagram, this module invokes the 
    // corresponding handler, e.g., ConnTryHandler.
}

Preconditions:

  • the datagram g as well as Identifier i and Connection e (respectively for push, setConnection and getConnection) are non-null;

Postconditions:

  • for setConnection: the local store on the module implementing this function stores at position i the value e;
  • for push: the outstandingDatagrams queue will append the Datagram g

Error conditions:

  • getConnection may fail (returning null) if no ConnectionEnd exists for the input parameter i;
  • before invoking the function setConnection, the caller should make sure that the client in the Identifier field was created;

Properties of the communication layer:

  • [ICS3-CommAssumption-1-RWIntegrity] If some connection e is returned from getConnection(i) then the setConnection(i, e) was previously invoked.

  • [ICS3-CommAssumption-2-QueueIntegrity] If some module d returns a datagram g from Pop("outstandingDatagrams"), then a process previously invoked Push("outstandingDatagrams", g).

  • [ICS3-CommAssumption-3-QueueNoLoss] If some process invokes Push("outstandingDatagrams", g), then eventually a Pop operation will return g.

Refinement remarks (relation to L3):

  • The push function is a more abstract version of submitDatagram (ICS 018).
  • The setConnection function is a more abstract version of the functionality accomplished by provableStore.set and addConnectionToClient (ICS 003).
  • The getConnection function is the analogy to getConnection (ICS 018).
Fault assumptions

The chains Alice and Bob (and their module, local store, and client, respectively) may be subject to arbitrary (Byzantine) faults. The properties we define below are guaranteed to hold iff both Alice and Bob behave correctly, i.e., do not deviate from any protocol we describe below. Beside these two parties, the system comprises an arbitrary number of other parties, any of which may be Byzantine; these other chains may, for instance, try to impersonate Alice or Bob or attack them in some way. The termination property of the ICS3 protocol depends on the existence of at least one correct relayer. Additionally, there may be an arbitrary number of relayers that can communicate (i.e., read/push) to Alice and Bob and are subject to Byzantine faults.

Additional remarks on the system model

We explicitly overlook here two assumptions of synchrony that may be necessary for achieving liveness of other protocols, but they are not necessary within the ICS3 protocol. These assumptions are: (i) partial synchrony is necessary for achieving liveness of a chain if that chain is implemented using a deterministic consensus protocol (e.g., Tendermint Core); (ii) synchrony is necessary for guaranteeing message delivery in any connection-oriented protocol such as TCP, which is most likely the underlying network transport layer (implementing the CommunicationLayer between modules and relayers).

Properties

Preliminary abstractions

We introduce several abstractions that are relevant at this point:

  1. A ConnectionParty is a data type encapsulating the details that identify a party.
type ConnectionParty interface {
    connectionIdentifier    Identifier
    clientIdentifier        Identifier
    prefix                  Prefix
}
  1. A ConnectionState captures the state of a connection, and may have one of the following values.
enum ConnectionState {
    UNINIT,
    INIT,
    TRYOPEN,
    OPEN,
}
  1. A ConnectionEnd is a data type that captures all the details of a connection at a party. This includes a remote and a local field, so that the local party is the one storing this object, and the remote party is the other one. One of the goals of the connection handshake protocol is to allocate an object of this type at each of Alice and Bob.
type ConnectionEnd interface {
    state           ConnectionState
    remoteParty     ConnectionParty
    localParty      ConnectionParty
    version         []String
}
  1. The ConnProof and ClientProof are two data types that abstracts over the details of a cryptographic proof that any module can create, and another module can verify. Intuitively, a proof is helpful for some module to guarantee that it is in a certain state. We are concerned with connection proofs (ConnProof type) and client proofs (ClientProof) here.
type ConnProof struct {
    proof CommitmentProof // The proof for the connection that the remote party claims to have.
}
type ClientProof struct {
    proof  CommitmentProof // The proof for the client that the remote party claims to have.
    height uint64          // The height which the client (on remote party) claims having.
}

We now restate the connection handshake problem in a slightly more precise (or lower level) formulation:

A connection handshake enables two ICS3 modules to agree on a consistent view of their chain state, to verify each other's state, and to allocate a new connection.

Guarantees

We refine the safety guarantee [ICS3-Seq-1-Agreement] (defined in the sequential problem statement) by splitting this into three complementary safety properties:

  • [ICS3-Proto-1-ConnectionUniqueness] A module accepts (i.e., initializes on) a ConnectionEnd e at most once.

  • [ICS3-Proto-2-ConnectionIntegrity] If any two modules open a connection e, then either one module or the other or both modules accepted (i.e., initialized with) e.

  • [ICS3-Proto-3-StateConsistency] If any two modules open a connection, then the client in the first module is consistent with the state of the second module.

The liveness property below is equivalent to [ICS3-Seq-2-Termination] (the livenes property in the sequential specification above):

  • [ICS3-Proto-4-Termination] If the two parties involved in a connection handshake are correct, then the connection handshake eventually terminates. Specifically, termination implies that each module allocates in the local store a new ConnectionEnd object with state field set to OPEN.

Remarks:

  • Uniqueness property essentially provides a safeguard against overwriting a connection in the store with some new set of parameters.

  • The integrity property, in conjunction with uniqueness, ensures that there is continuity between the connections that a module initializes and the connections that this module opens.

  • One of the mechanisms that enforces the connection integrity property consists of cryptographic proofs, specifically the ConnProof type, which asserts that a certain chain stores a certain connection in a certain state.

  • The ClientProof type guarantees the state consistency property, by asserting that the client on a chain is updated to a consensus state of the remote chain.

  • Note that the consistency property works both ways. This property applies to any two modules (there is no predefined "first" or "second" module here).

2.2 Protocol

The ICS3 protocol comprises four steps, summarized below.

  1. An actor invokes the ConnInitHandler handler at the ICS3 module in one of the chains; this sets off the connection handshake protocol. In our example, we will use Alice as the party to execute ConnInitHandler. Once Alice does so, this handler marks the connection on her end as initialized (i.e., INIT).

  2. This comprises two sub-steps:

    • 2.a. Upon observing that Alice has executed ConnInitHandler (meaning that her state contains a connection that is INIT), the relayer constructs a datagram of type ConnOpenTry and pushes this at Bob's module;
    • 2.b. Bob handles this datagram via the ConnTryHandler handler. Once this handler finishes, the connection on his end is marked as TRYOPEN.

  3. This comprises two sub-steps:

    • 3.a. Upon observing that Bob has finished executing ConnTryHandler (i.e., his state contains a TRYOPEN connection), the relayer constructs a datagram of type ConnOpenAck and pushes this at Alice's module;
    • 3.b. Alice handles this datagram by invoking the ConnAckHandler handler. Once this handler finishes, Alice considers her ConnectionEnd in state OPEN.

  4. This comprises two sub-steps:

    • 4.a. When the relayer observes that Alice finished handling the ConnOpenAck datagram (and consequently the connection is open on her side), the relayer constructs a ConnOpenConfirm datagram and pushes it on Bob's side.
    • 4.b. Finally, Bob's module processes the ConnOpenConfirm datagram through an eponymous handler, which sets the connection state to OPEN for him and thereby marks the termination of the ICS3 protocol.

The diagram below sketches these fours steps of handshake protocol.

               The four steps comprising
             IBC Connection Handshake Protocol
        Alice                                   Bob
     +-----------+                         +-----------+
     |ICS3 Module|                         |ICS3 Module|
     |           |                         |           |
     |         step 1                      |           |
     |     ConnInitHandler                 |           |
     |  ►INIT    |                         |           |
     |           |<-2.a--Relayer-----2.a-->|           |
     |           |                 |       |           |
     |           |                  \-> step 2.b       |
     |           |                     ConnTryHandler  |
     |           |                         | ►TRYOPEN  |
     |           <--3.a------Relayer--3.a->|           |
     |           |        |                |           |
     |      step 3.b <---/                 |           |
     |     ConnAckHandler                  |           |
     |  ►OPEN    |                         |           |
     |           |<-4.a---Relayer----4.a-->|           |
     |           |                 |       |           |
     |           |                  \-> step 4.b       |
     |           |              ConnConfirmHandler     |
     |           |                         | ►OPEN     |
     +-----------+                         +-----------+

Protocol handler signatures

We first present the signatures of the four protocol handlers; the connection handshake module at each party implements and exposes these handlers.

func ConnInitHandler(
    local ConnectionParty,
    remote ConnectionParty)

func ConnTryHandler(
    local ConnectionParty,
    remote ConnectionParty,
    remoteVersions []String,
    proofsHeight uint64,
    remoteConnectionProof ConnProof,
    remoteClientProof ClientProof)

func ConnAckHandler(
    local ConnectionParty,
    remoteVersion String,
    proofsHeight uint64,
    remoteConnectionProof ConnProof,
    remoteClientProof ClientProof)

func ConnConfirmHandler(
    local ConnectionParty,
    proofsHeight uint64,
    remoteConnectionProof ConnProof)

Main Protocol Handlers

We first define the four protocol handlers, and then describe the datagrams. Finally, we discuss some helper functions.

ConnInitHandler

This is step 1.

func ConnInitHandler(local ConnectionParty, remote ConnectionParty)
{
    // Create local end of the connection in the state 'INIT'.
    connectionEnd = newConnectionEnd('INIT', local, remote, getCompatibleVersions())

    // Uniqueness check.
    // The Init handler for a given connection may run only once.
    // Abort, unless this is the first time initializing this connection.
    abortTransactionUnless(getConnection(local.connectionIdentifier) == nil)

    // Now save this connection end in the local store.
    // This connectionEnd is in state INIT, the relayer will continue with
    // next steps of the connection handshake protocol.
    setConnection(local.connectionIdentifier, connectionEnd)
}

Preconditions:

  • The parameters local and remote should be valid, i.e., a syntactically correct (see validation).
  • This handler must not have executed previously with the same local input parameter (in particular, the same local.connectionIdentifier field).

Postconditions:

  • The module executing this handler stores a ConnectionEnd (matching with the input arguments local and remote) in state INIT.
  • Uniqueness is satisfied because this handler aborts if a key with the identifier local.connectionIdentifier already exists in the store (at-most-once semantics).
  • To ensure termination of the ICS3 protocol, this handler must execute either on one of the chains or both (at-least-once semantics).
  • Handler produces no output; may abort if preconditions not met.
ConnTryHandler

This is step 2.b.

func ConnTryHandler(
	local ConnectionParty,
	remote ConnectionParty,
	remoteVersions []String,
	proofsHeight uint64,
	remoteConnectionProof ConnProof,
	remoteClientProof ClientProof)
{ 
    // Create local end of the connection. 
    connectionEnd = newConnectionEnd('TRYOPEN', local, remote, pickVersion(remoteVersions))

    // Uniqueness check.
    // Verify that if there is a connection then the Init handler previously executed 
    // with these same parameters).
    current = getConnection(local.connectionIdentifier)
    abortTransactionUnless(
        current == nil || 
        current.state == 'INIT' && matchingEnds(connectionEnd, current))

    // Verify proofs.
    expectedRemoteConnection = newConnectionEnd('INIT', remote, local, remoteVersions)
    abortTransactionUnless(verifyProofs(
        expectedRemoteConnection, proofsHeight, remoteConnectionProof, remoteClientProof)

    // Handler done, store the updated connectionEnd.
    setConnection(local.connectionIdentifier, connectionEnd)
}

Preconditions:

  • The input parameters should be valid; among others validation criteria, it is important that the module running this handler supports at least one of the versions supplied in the input list remoteVersions (see validation).
  • The two proofs remoteConnectionProof and remoteClientProof should be correct. This is necessary in connection to properties [ICS3-Proto-2-ConnectionIntegrity] and [ICS3-Proto-3-StateConsistency]. Correctness of proofs means that they pass verification (verifyProof function).

Postconditions:

  • The module executing this handler stores a ConnectionEnd (matching with the arguments local and remote) in state TRYOPEN.
  • No output; may abort if preconditions not met.
ConnAckHandler

Step 3.b.

func ConnAckHandler(
	local ConnectionParty,
	remoteVersion String,
	proofsHeight uint64,
	remoteConnectionProof ConnProof,
	remoteClientProof ClientProof)
{ 
    // Search the details of this connection in local store.
    connectionEnd = getConnection(local.connectionIdentifier)

    // This verification helps guarantee uniqueness and integrity.
    abortTransactionUnless(connectionEnd != nil && connectionEnd.local == local)

    // Should not overwrite a connection that is already `OPEN`.
    abortTransactionUnless(connectionEnd.state == INIT || connectionEnd.state == TRYOPEN)

    // Verify proofs.
    expectedRemoteConnection = newConnectionEnd('TRYOPEN', remote, local, remoteVersion)
    abortTransactionUnless(verifyProofs(
        expectedRemoteConnection, proofsHeight, remoteConnectionProof, remoteClientProof)

    // Termination (partial -- only at this end)
    connectionEnd.state = OPEN
    connectionEnd.version = remoteVersion

    // Update the connectionEnd in local state.
    setConnection(local.connectionIdentifier, connectionEnd)
}

Preconditions:

  • The module executing this handler already has a ConnectionEnd stored locally, matching the local argument, and in state INIT or TRYOPEN.
  • The input parameters are valid (see validation).
  • The two proofs remoteConnectionProof and remoteClientProof are correct; for guaranteeing properties [ICS3-Proto-2-ConnectionIntegrity] and [ICS3-Proto-3-StateConsistency].

Postconditions:

  • The module executing this handler stores a ConnectionEnd (matching with the arguments local) in state OPEN.
  • No output; may abort if preconditions not met.
ConnConfirmHandler

Step 4.b.

func ConnConfirmHandler(
    local ConnectionParty,
    proofsHeight uint64,
    remoteConnectionProof ConnProof)
{
    // Search the details of this connection in the local store.
    connectionEnd = getConnection(local.connectionIdentifier)

    // Helps guarantee integrity and uniqueness.
    abortTransactionUnless(connectionEnd != nil && connectionEnd.local == local)

    // Integrity check: the handler should not overwrite a connection that is
    // already OPEN. And should not be working with a connection that is 
    // INIT. The only acceptable state is TRYOPEN.
    abortTransactionUnless(connectionEnd.state == TRYOPEN)

    // Connection proof verification.
    expectedRemoteConnection = newConnectionEnd('OPEN', remote, local, connectionEnd.version)
    abortTransactionUnless(verifyProofs(
        expectedRemoteConnection, proofsHeight, remoteConnectionProof, nil)

    // Termination.
    connectionEnd.state = OPEN
    setConnection(local.connectionIdentifier, connectionEnd)
}

Preconditions:

  • The module executing this handler has a ConnectionEnd stored locally, (matching the input argument local) and in state TRYOPEN.
  • The input parameters are valid (see validation).
  • The input proof remoteConnectionProof is correct; for guaranteeing property [ICS3-Proto-2-ConnectionIntegrity].

Postconditions:

  • The module executing this handler stores a ConnectionEnd (matching with the input argument local) in state OPEN.
  • No output; may abort if preconditions not met.
Datagrams

A correct relayer can push the following datagrams at a chain. Upon popping a datagram of a certain type, e.g., ConnOpenConfirm, a correct chain handles the datagram by first validating the datagram (syntactic validation, e.g., well-formed parameters, see validation) and then invoking the corresponding handler.

type ConnOpenInit struct {
    local   ConnectionParty
    remote  ConnectionParty
}

type ConnOpenTry struct {
    local                 ConnectionParty
    remote                ConnectionParty
    remoteVersions        []String
    proofsHeight          uint64
    remoteConnectionProof ConnProof
    remoteClientProof     ClientProof
}

type ConnOpenAck struct {
    local                 ConnectionParty
    remoteVersion         String
    proofsHeight          uint64
    remoteConnectionProof ConnProof
    remoteClientProof     ClientProof
}

type ConnOpenConfirm struct {
    local                 ConnectionParty
    proofsHeight          uint64
    remoteConnectionProof ConnProof
}

Notice that the fields in each datagram match with the corresponding protocol handler signature.

Helper functions & application-level predicates

matchingEnds(endLocal, endRemote)

Checks that the connection ends in the local and remote arguments match. (NB: This does not check the connection state, only the connection parties).

Validation

When we talk of validation we usually mean a verification that is done before a handler executes, checking that the input parameters of that handler are syntactically correct, e.g., valid local connection party, non-null proofs, non-zero proofs height. With respect to the local parameter, similar in functionality with validateConnectionIdentifier from ICS 003, we also validate the local.connectionIdentifier field. Additionally, if a version or remoteVersion input parameter is present, this should also be validated prior to invoking a handler with that version.

pickVersion(counterpartyVersions)

This is identical with the one in ICS 003.

getCompatibleVersions()

This is identical with the one in ICS 003.

Proof Verification

This function handles everything related to proof verification. It requires four arguments: the connection end as it expected to be on the remote party, the height where the proofs were taken, a connection proof, and a client proof; the last argument may be nil. This function invokes a lower-level method client.verifyProof, which executes from a client context and handles the cryptographic verification of a given proof; this method is analogous to verifyMembership of the ICS 023, except it must additionally get the commitment root from the consensuss state and perform serialization on the expected data. The pseudocode for the verifyProofs is provided below.

func verifyProofs(
    expectedConnection ConnectionEnd,
    proofsHeight,
    remoteConnectionProof ConnProof,
    remoteClientProof ClientProof)
{
    // Proofs verification.
    // Generic proof check: Local client should exists and be updated with the
    // height which the two proofs target (proofsHeight).
    client = clientState(expectedConnection.remote.clientIdentifier)
    abortTransactionUnless(client != nil)
    clientConsensusState = clientConsensusState(expectedConnection.remote.clientIdentifier), proofsHeight)
    abortTransactionUnless(clientConsensusState != nil)

    // Connection proof specific verification.
    abortTransactionUnless(client.verifyProof(
        clientConsensusState, remoteConnectionProof,
        connectionPath(local.connectionIdentifier), expectedConnection))

    if remoteClientProof == nil {
        return // Client proof is missing, so skip any further verification.
    }

    // Client proof verification ensures state consistency: the remote
    // client should be consistent with the state of local party.
    expectedRemoteClientConsensus = localConsensusState(remoteClientProof.height)
    abortTransactionUnless(remoteClientProof.height <= getCurrentHeight())
    abortTransactionUnless(client.verifyProof(
        clientConsensusState, remoteClientProof,
        clientPath(local.clientIdentifier, remoteClientProof.height),
        expectedRemoteClientConsensus))
}
localConsensusState and clientConsensusState

These are analogous to getConsensusState and queryClient functions. The clientConsensusState, in particular, has an implicit requirement that it may not return the consensus state of a client if the height is older than a certain threshold; the proofsHeight should not be outdated by more than 100 heights, specifically. (This means that proofs must not be too old.)

Open questions:

  • Standard cryptographic assumptions (collision-resistant hash functions, public-key signatures). We should mention these once we have more details about the implementation.

  • How to capture aborts or incorrect termination? See issue raised by Anca. Is this necessary? To inform this discussion, more implementation details are needed.

  • Verification of the unbonding period in ConnTryHandler. See ICS/#403.

  • Missing link to L3: what is the mechanism that implements the pop functionality at the implementation/L3 level (hint: it's in the SDK, the layer sitting between the consensus module and IBC Handler).

References