基于对称性和量化的分布式协议验证新方法
On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
摘要：
证明一个无界的分布式协议满足给定的安全属性相当于找到一个量化的归纳不变量，它意味着协议的所有可能的实例大小的属性。现有的解决这个问题的方法可以描述为搜索过程的不变量的量化前缀适合一个特定的模板。我们提出了一种替代建设性的方法，不规定，先验，一个特定的量词前缀。相反，通过仔细分析协议的结构对称性，自动推断出所需的前缀，而无需任何搜索。这种方法背后的关键见解是，对称性和量化是密切相关的概念，表达协议的不变性下，其组件的不同重新安排。我们提出了对称增量感应，有限域IC 3/PDR算法的扩展，自动推导出所需的量化归纳不变量，利用对称性和量化之间的连接。虽然已经进行了各种尝试，利用对称性在验证应用程序，据我们所知，这是第一次演示的对称性和量化的上下文中的小句学习过程中的增量归纳的直接联系。我们还描述了一个程序，自动找到一个最小的有限大小，截止，产生一个量化的不变证明安全的任何大小。我们的方法在IC 3 PO中实现，IC 3 PO是一种新的分布式协议验证器，其性能显着优于最先进的技术，更快地扩展数量级，并完全自动地稳健地导出紧凑的归纳不变量。
英文摘要：
Proving that an unbounded distributed protocol satisfies a given safety property amounts to finding a quantified inductive invariant that implies the property for all possible instance sizes of the protocol. Existing methods for solving this problem can be described as search procedures for an invariant whose quantification prefix fits a particular template. We propose an alternative constructive approach that does not prescribe, a priori, a specific quantifier prefix. Instead, the required prefix is automatically inferred without any search by carefully analyzing the structural symmetries of the protocol. The key insight underlying this approach is that symmetry and quantification are closely related concepts that express protocol invariance under different re-arrangements of its components. We propose symmetric incremental induction, an extension of the finite-domain IC3/PDR algorithm, that automatically derives the required quantified inductive invariant by exploiting the connection between symmetry and quantification. While various attempts have been made to exploit symmetry in verification applications, to our knowledge, this is the first demonstration of a direct link between symmetry and quantification in the context of clause learning during incremental induction. We also describe a procedure to automatically find a minimal finite size, the cutoff, that yields a quantified invariant proving safety for any size. Our approach is implemented in IC3PO, a new verifier for distributed protocols that significantly outperforms the state-of-the-art, scales orders of magnitude faster, and robustly derives compact inductive invariants fully automatically.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
