A Tendermint Light Client

TL;DR

This paper introduces a Tendermint light client protocol that efficiently verifies blockchain state by reducing data download and signature verification, formalized with proofs and model checking.

Contribution

It formalizes the Tendermint dynamic fault model and proposes a novel light client protocol with verified safety and liveness properties.

Findings

Significantly reduces data download for blockchain verification

Decreases computational load by minimizing signature checks

Ensures safety and liveness through formal proofs and model checking

Abstract

In Tendermint blockchains, the proof-of-stake mechanism and the underlying consensus algorithm entail a dynamic fault model that implies that the active validators (nodes that sign blocks) may change over time, and a quorum of these validators is assumed to be correct only for a limited period of time (called trusting period). The changes of the validator set are under control of the blockchain application, and are committed in every block. In order to check what is the state of the blockchain application at some height h, one needs to know the validator set at that height so that one can verify the corresponding digital signatures and hashes. A naive way of determining the validator set for height h requires one to: (i) download all blocks before h, (ii) verify blocks by checking digital signatures and hashes and (iii) execute the corresponding transactions so the changes in the validator sets are reproduced. This can potentially be very slow and computationally and data intensive. In this paper we formalize the dynamic fault model imposed by Tendermint, and describe a light client protocol that allows to check the state of the blockchain application that, in realistic settings, reduces significantly the amount of data needed to be downloaded, and the number of required computationally expensive signature verification operations. In addition to mathematical proofs, we have formalized the light client protocol in TLA+, and checked safety and liveness with the APALACHE model checker.