龙腾：基于可合并并行机制的分布式系统安全性验证【JSA，2022】

2022-09-06     发布：[bat365正版唯一官网]    点击：442次

随着信息和网络技术的发展，分布式系统越来越流行，如何应用形式化的方法来提高分布式系统的质量引起了社会的广泛关注。安全属性保证不会发生任何不好的事情，包括协议的正确性、无法访问的错误状态、没有死锁等。 验证分布式程序的安全属性具有挑战性。一个原因是分布式执行中的高度异步事件。由于异步事件的存在，不变量变得更加复杂。以两阶段提交协议为例，由于它包含无限数量的数据库节点，其完整的异步不变量将近 150 行。另一方面，异步不变量与无限长度的消息缓冲区的内容有关。 以服务器和客户端之间进行任务分发为例，其发送的内容与它的预期接收是否正确有关。分布式系统安全性问题的相关证明需要跟踪消息的内容，增加了相关验证工作的难度。现有工作通常涉及普遍量化的复杂不变量，难以提高效率，也难以复用成熟的验证工具。 

针对上述科学问题，我院“软件服务工程与智慧物联网”团队的龙腾副教授及其合作者，基于Lipton原理提出一种分布式异步到同步的约简机制，在安全性验证方面使得程序的执行可以简化为具有固定顺序集的执行，并证明其可靠性。该方法可用于基于多类拓扑结构的分布式协议，从而扩展了分布式系统验证问题的范围。 

工作的创新与贡献如下：

1我们的工作旨在扩展与异步消息传递程序相关的问题验证的适用性，并采用简化方法。为了解决更多的实际问题，我们提出了可合并并行的概念，并在此基础上对原程序进行等价变换。在这种变换上，任何给定的可合并程序轨迹都可以看作是重写后的并发程序的一些样本实例上的执行顺序，从而扩大了应用范围。

2 我们提出了适用于异步消息传递机制的推理规则（图1-3），扩展了异步消息传递程序相关的问题验证的适用性。

3 我们在名为 ASYSIM 的原型工具中实现了所提出的方法，并对涵盖通信拓扑、并发性和共识机制等各种特性的示例进行了实验。实验结果表明，我们的方法在分布式案例子类中是精确和可行的，并且我们的工具比可以处理更多的案例（图4-6）。 

本文提出的可合并消息传递程序的正确性可以整合最先进的验证框架。实验涉及Multi-party协议、多轮次协议、Paxos系列协议等，涵盖线性、循环、多对多等拓扑结构。实验结果表明，我们的方法是有效的，适用于各种消息传递情况。取得的成果对基于区块链的协议验证等科学问题有重要参考意义。

图1 异步的发送规则

图2 异步的接收规则

图3 带条件的顺序化规则

图4 Multi-Party案例运行结果

图5多阶段案例运行结果

图6线性拓扑案例运行结果与对比 

上述研究成果发表在计算机领域国际权威刊物, 中国计算机学会推荐学术期刊 CCF B类《Journal of Systems Architecture》上：Teng Long*, et al. Verifying Safety Properties of Distributed Systems via Mergeable Parallelism [J]. Journal of Systems Architecture 2022 102646. [JCR Q1, IF 2022=5.836]

全文链接：https://doi.org/10.1016/j.sysarc.2022.102646