- 提交验证 - 验证来自单个全节点（称为 primary）的已签名区块头及其关联的验证者集合变更
- 攻击检测 - 跨多个全节点（称为 secondaries）验证提交，并检测冲突（即是否存在轻客户端攻击）
- 问责 - 给定攻击证据，计算应对此负责的一组验证者
提交验证
英文规范 以时间属性 LCV-DIST-SAFE.1 和 LCV-DIST-LIVE.1 描述了轻客户端的提交验证问题。提交验证被假定运行在 Cosmos 故障模型之中，在该模型下，验证者中有超过 2/3 在某个时间段内是正确的，并且验证者集合在每个高度都可以任意变化。 这里还给出了一个轻客户端协议，包含为满足这些时间属性而必须对区块头、提交和验证者集合执行的全部检查，因此轻客户端可以持续与区块链保持同步。客户端可以利用可信与不可信验证者集合之间的重叠，跳过可能大量的中间区块头。当重叠不足时，可以使用二分例程找到一组能够提供所需重叠的最小区块头集合。 TLA+ 规范 ver. 001 是对客户端执行的提交验证协议的形式化描述，包含安全性与终止性，可使用 Apalache 进行模型检查。 更详细的 TLA+ 规范 轻客户端验证 ver. 003 目前正在同行评审中。MC*.tla 文件为 TLA+ 规范 提供了具体参数，以便执行模型检查。例如，MC4_3_faulty.tla 包含了节点、高度、信任期、时钟漂移、主节点正确性以及故障进程比例的如下参数：
$DIR 中，并执行以下命令：
results.csv 中的所有行都应报告为 Deadlock，这表示算法已经终止，且未发现任何不变式违反。
与 002bmc-apalache-ok.csv 类似，文件 003bmc-apalache-error.csv 指定了应当产生反例的一组实验：
results.csv 中的所有行都应报告为 Error。
下表汇总了轻客户端验证 version 001 的实验结果。相关 TLA+ 属性可见于 TLA+ 规范。实验运行于一台配备 32GB RAM 和 4 核 Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz 的 AWS 实例上。我们用“✗=k”表示在深度 k 处报告了一个错误，用“✓<=k”表示截至深度 k 未报告任何错误。
version 003 的实验结果将随后补充。
攻击检测
英文规范 定义了轻客户端攻击（以及它们与区块链分叉的区别），并描述了轻客户端如何通过与全节点网络通信来检测这些攻击的问题，其中至少有一个全节点是正确的。 该规范还包含一个检测协议，用于检查通过验证协议从 primary 获取的区块头是否与 secondaries 提供的对应区块头一致。如果不一致，协议会分析相关全节点的验证轨迹，并生成可提交给全节点的不当行为证据，以便惩罚存在故障的验证者。 TLA+ 规范 是对双对等节点检测协议的形式化描述，包含安全性与终止性，可使用 Apalache 进行模型检查。LCD_MC*.tla 文件为 TLA+ 规范 提供了具体参数，以便运行模型检查器。例如，LCD_MC4_4_faulty.tla 包含了节点、高度、信任期、时钟漂移、节点正确性以及故障进程比例的如下参数：
$DIR 中，并执行以下命令：
results.csv 中的所有行都应报告为 Deadlock，这表示算法已经终止，且未发现任何不变式违反。
与 004bmc-apalache-ok.csv 类似，文件 005bmc-apalache-error.csv 指定了应当产生反例的一组实验：
results.csv 中的所有行都应报告为 Error。
详细实验结果将很快补充。
问责
英文规范 定义了全节点在接收到来自轻客户端的攻击证据后所执行的协议。特别地，该协议处理三类攻击：- lunatic
- equivocation
- amnesia
This directory contains work-in-progress English and TLA+ specifications for the Light Client protocol. Implementations of the light client can be found in Rust and Go. Light clients are assumed to be initialized once from a trusted source 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 two main components:
- Commit Verification - verify signed headers and associated validator set changes from a single full node, called primary
- Attack Detection - verify commits across multiple full nodes (called secondaries) and detect conflicts (ie. the existence of a lightclient attack)
- Accountability - given evidence for an attack, compute a set of validators that are responsible for it.
Commit Verification
The English specification describes the light client commit verification problem in terms of the temporal properties LCV-DIST-SAFE.1 and LCV-DIST-LIVE.1. Commit verification is assumed to operate within the Cosmos Failure Model, where +2/3 of validators are correct for some time period and validator sets can change arbitrarily at each height. A light client protocol is also provided, including all checks that need to be performed on headers, commits, and validator sets to satisfy the temporal properties - so a light client can continuously synchronize with a blockchain. Clients can skip possibly many intermediate headers by exploiting overlap in trusted and untrusted validator sets. When there is not enough overlap, a bisection routine can be used to find a minimal set of headers that do provide the required overlap. The TLA+ specification ver. 001 is a formal description of the commit verification protocol executed by a client, including the safety and termination, which can be model checked with Apalache. A more detailed TLA+ specification of Light client verification ver. 003 is currently under peer review. TheMC*.tla files contain concrete parameters for the
TLA+ specification, in order to do model checking.
For instance, MC4_3_faulty.tla contains the following parameters
for the nodes, heights, the trusting period, the clock drifts,
correctness of the primary node, and the ratio of the faulty processes:
$DIR and run the following commands:
results.csv should report Deadlock, which means that the algorithm
has terminated and no invariant violation was found.
Similar to 002bmc-apalache-ok.csv,
file 003bmc-apalache-error.csv specifies
the set of experiments that should result in counterexamples:
results.csv should report Error.
The following table summarizes the experimental results for Light client verification
version 001. The TLA+ properties can be found in the
TLA+ specification.
The experiments were run in an AWS instance equipped with 32GB
RAM and a 4-core Intel® Xeon® CPU E5-2686 v4 @ 2.30GHz CPU.
We write “✗=k” when a bug is reported at depth k, and “✓<=k” when
no bug is reported up to depth k.
The experimental results for version 003 are to be added.
Attack Detection
The English specification defines light client attacks (and how they differ from blockchain forks), and describes the problem of a light client detecting these attacks by communicating with a network of full nodes, where at least one is correct. The specification also contains a detection protocol that checks whether the header obtained from the primary via the verification protocol matches corresponding headers provided by the secondaries. If this is not the case, the protocol analyses the verification traces of the involved full nodes and generates evidence of misbehavior that can be submitted to a full node so that the faulty validators can be punished. The TLA+ specification is a formal description of the detection protocol for two peers, including the safety and termination, which can be model checked with Apalache. TheLCD_MC*.tla files contain concrete parameters for the
TLA+ specification,
in order to run the model checker.
For instance, LCD_MC4_4_faulty.tla
contains the following parameters
for the nodes, heights, the trusting period, the clock drifts,
correctness of the nodes, and the ratio of the faulty processes:
$DIR and run the following commands:
results.csv should report Deadlock, which means that the algorithm
has terminated and no invariant violation was found.
Similar to 004bmc-apalache-ok.csv,
file 005bmc-apalache-error.csv specifies
the set of experiments that should result in counterexamples:
results.csv should report Error.
The detailed experimental results are to be added soon.
Accountability
The English specification defines the protocol that is executed on a full node upon receiving attack evidence from a lightclient. In particular, the protocol handles three types of attacks- lunatic
- equivocation
- amnesia