第7章：拜占庭故障与协议验证

从崩溃到任意行为

崩溃节点停止行动，拜占庭节点可能对不同对象发送矛盾消息、伪造状态或偏离协议。数字签名帮助确认消息来源，却不能阻止持有合法密钥的节点主动说谎。

经典部分同步 BFT 状态机复制常用 $n\ge3f+1$，以 $2f+1$ 个投票形成证书。两个此类 quorum 至少相交于 $f+1$ 个节点，其中至少一个诚实节点；再配合诚实节点的投票和锁定规则，才能证明不同决定不会同时成立。

这个界属于具体模型与保证，不能说所有同步、异步、签名模型都只有同一阈值。quorum 算式本身也不是完整 BFT 协议。

不变量与反例执行

协议证明通常先找不变量，例如“已经提交的日志项不会被后续合法领导者覆盖”。再逐类检查消息、超时、重启和配置变更是否保持它。

反例不需要大集群。三个节点、一次延迟和一次崩溃就可能暴露错误。将事件写成发送、接收、持久化、响应的序列，比只看正常路径更容易发现漏洞。

故障注入

测试可以主动丢包、延迟、重复、分区和重启，记录客户端调用与返回，再检查历史是否满足所需一致性。有限测试未发现问题不是证明，但能找到具体违反保证的执行。

需同时检查安全性与活性：协议永远不返回当然容易避免错误答案，却没有提供可用服务；超时强行返回又可能破坏安全。

综合练习

1. 在三节点复制服务中枚举“写入本地、复制一份、回复客户端、主节点崩溃”的不同顺序，判断何时可能丢失已确认写。
2. 对一个简化锁服务加入进程长暂停，验证新旧持有者是否可能同时写外部资源，并加入 fencing 修复。
3. 为键值服务写明支持的故障数、持久存储假设、读取一致性和恢复活性条件，再据此设计故障测试。

系统名称和协议名不能代替这些保证。一个可评估的设计需要说明它接受哪些故障执行、拒绝哪些结果，以及何时能够继续推进。