分而治之：一种基于组合学的博弈论安全方法

《Proceedings of the ACM on Programming Languages》：Divide and Conquer: A Compositional Approach to Game-Theoretic Security

区块链等去中心化系统的安全分析采用组合式推理方法，将博弈论中的经济激励问题转化为SMT求解，通过分治策略将大规模协议分解为可增量分析的子博弈，确保整体安全性且扩展至数百万节点。

　　

摘要

我们提出了一种组合方法，用于结合和扩展在去中心化系统安全（如区块链）静态分析中的自动化推理能力。我们的重点在于对这些系统的博弈论安全分析，这使我们能够研究用户行为背后的经济激励因素。在这种情况下，特别重要的是要证明偏离去中心化协议的预期、诚实行为并不会带来任何利益：只要用户遵循协议，无论其他用户如何行为，他们都不会受到经济损失。对区块链协议的这种经济分析可以编码为一阶实数算术理论中的自动化推理问题，从而将博弈论推理简化为满足性模理论（SMT）问题。然而，将整个博弈论模型（称为“博弈”）作为一个单一的SMT实例进行分析并不足以处理具有数百万交互行为的协议。为了解决这一挑战，我们提出了一种基于对博弈进行组合推理的安全分析方法。我们的组合分析是渐进式的：我们将博弈划分为子博弈，这样对某个子博弈的更改无需重新分析整个博弈，而只需重新分析其父节点即可。我们的方法是可靠、完备且有效的：通过组合子博弈的安全属性，可以得出整个博弈的安全性。实验结果表明，组合推理能够在处理具有数百万节点的博弈时发现博弈内部的特性和错误，从而实现对大型协议的安全分析。