基于Coq的Paxos形式化建模与验证-李亚男，邓玉欣，刘静.pdf

上善若水

249

13页

0次

2022-05-24

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software,2020,31(8):2362−2374 [doi: 10.13328/j.cnki.jos.005960] http://www.jos.org.cn

基于 Coq 的 Paxos 形式化建模与验证

∗

李亚男

邓玉欣

刘

静

(上海市高可信计算重点实验室(华东师范大学),上海 200062)

通讯作者: 邓玉欣, E-mail: yxdeng@sei.ecnu.edu.cn

摘要: Paxos 是一个在不可靠的分布式处理器网络中解决共识问题的算法族.共识问题是指分布式系统中一组

参与者就一个结果达成一致的过程.随着 Paxos 在大型分布式系统中的广泛运用,比如区块链系统以及谷歌文件系

统等,其安全性证明越来越重要.在定理证明工具 Coq 中,形式化描述和定义了 Lamport 的 Basic Paxos 算法,并且证

明了其满足共识性.

关键词: 分布式系统;Basic Paxos;定理证明工具;Coq;验证

中图法分类号: TP311

中文引用格式: 李亚男,邓玉欣,刘静.基于 Coq 的 Paxos 形式化建模与验证.软件学报,2020,31(8):2362−2374. h ttp :// ww w.jos .

org.cn/1000-9825/5960.htm

英文引用格式: Li YN, Deng YX, Liu J. For mal mo deling and verification of Paxo s based on Coq . Ruan Jian Xu e Bao/Journal of

Software, 2020,31(8):2362−2374 (in Chinese). http://www.jos.org.cn/1000-9825 /5960.htm

Formal Modeling and Verification of Paxos Based on Coq

LI Ya-Nan, DENG Yu-Xin, LIU Jing

(Shanghai Key Laboratory of Trustworthy Computing (East China Normal University), Shanghai 200062, China)

Abstra ct : Paxos is a family of algorithms that solve consensus problems in unreliable distributed processor networks. Consensus is a

process in which a group of participants in the system reach agreement on a result. As Paxos is widely used in large distr ibuted systems,

such as block chain system and Google file system, its security verification becomes more and more important. With Coq, a theorem

proving tool, the formal description and definition of Lamport’s basic Paxos algorithm are described, and it is proved th at it satisfies the

consensus property.

Key words: distributed system; Basic Paxos; th eorem proof assistant; Coq; v erification

随着大数据的普及,分布式系统成为计算机科学十分热门的一个研究方向.分布式系统主要面临两方面的

考验:在出现节点错误时,分布式系统需要保证其可以正常地将错误节点切换到其他备用节点;在某个节点进行

数据更新时,分布式系统需要保证其更新顺序可以被其他节点以相同的顺序复制,以此来保证整个系统数据副

本的一致性.为了解决分布式系统的这些问题,人们提出了大量的分布式算法.然而,它们的正确性常常被非形

式化地证明.当算法变得复杂时,非形式化的正确性证明就容易出错.一个证明如果能被严格验证,就可以获得

更高的可信度.

形式化方法是计算机科学的重要理论基础,它以严格的数学化和机械化方法为基础,对数学理论或者计算

系统进行建模、规约和验证,并以此解决和改善一系列数学方面或者软件安全性方面的问题.大量的工业实践

表明:在开发复杂的硬件和软件系统时,我们将更多的精力花在验证系统的正确性上,而不是构建系统上.经过

∗ 基金项目: 国家自然科学基金(61672229, 61832015)

Foundation item: National Natural Science Foundation of China (61672229, 61832015 )

本文由“面向新兴系统的形式化建模与验证方法”专题特约编辑陈振邦副教授、冯新宇教授、刘志明教授推荐.

收稿时间: 2019-0 8-31; 修改时间: 2019-11-02, 2019-12-30; 采用时间: 2020-02-07; jos 在线出版时间: 2020-04-18

李亚男等:基于 Coq 的 Paxos 形式化建模与验证

2363

几十年的不断努力和发展,形式化方法在验证越来越多的数学证明和新兴系统中发挥着越来越重要的作用.形

式化验证大致有两类方法:模型检验和定理证明.模型检验对系统模型的状态空间进行了穷举,以确定在执行所

有状态之后是否满足目标结果.虽然模型检验有很多优势,比如其检验过程基本上是自动化的以及如果存在不

满足系统所需的属性时会给出一个反例等,但是模型检验在随着待验证系统的规模越来越大时,不可避免地会

遇到状态爆炸问题,以致于难以解决规模大的实际问题.另一方面,定理证明的基本思想是将系统规范转化为数

学理论,然后通过生成中间证明步骤来构造定理证明,或者反驳它.因为定理证明利用数学上的递归、归纳原理

能够很好地解决系统模型过大的问题,故其相对于模型检测有一定的优势.

在定理证明中,会用到许多交互定理证明器,也被称为辅助证明工具,Coq 便是最受欢迎的定理证明工具之

一.Coq 实现了一种被称为 Gallina 语言的高级数学语言

[1]

,该语言基于一种被称为归纳构造演算(CIC)的基础理

论,这个理论将高阶逻辑和多类型的函数式编程语言结合在一起,用户对 Coq 中已证明定理的信心便来自于构

造演算的性质.在推理和编程方面,Coq 拥有强大的表达能力,可以构造简单的项,执行简单的证明,学习复杂的

算法,直到建立完整的理论.Coq 具有一个交互式的编译环境,用户可以边证明、边调整、边修改,使证明中的错

误和不足及时得到改正和补充,非常地友好.除了用于形式化地验证数学定理,例如著名的四色定理

[2]

外,Coq 还

成功地应用于确保系统的硬件和软件系统的可靠性,包括乘法器电路

[3]

、编译器

[4]

、邮件服务协议

[5]

和自稳定

协议

[6]

等.

本文将在辅助证明工具 Coq 中,对分布式共识算法 Basic Paxos 进行形式化地建模与验证.分布式共识是分

布式计算中的一个基本问题,它要求一组进程在某些值上达成一致.当为了容错而复制分布式服务时,共识是必

不可少的,因为非故障副本必须一致.不幸的是, 当进程或消息信道可能失败时, 很难达成共识.Paxos

[7]

是

Lamport 为解决分布式共识而开发的一种重要算法, 已经在许多重要的分布式服务中使用,例如 Google

Chubby

[8]

,Microsoft Autopilot

[9]

以及 WeChat PaxosStore

[10]

等.Basic Paxos 处理在没有共享内存的情况下并发运

行的进程就单个值达成一致的问题,在这种情况下,进程可能崩溃,稍后可能恢复,消息可能会无限期丢失或延

迟.在 Basic Paxos 中,每个进程可能重复提出一些值,并等待来自进程的适当子集的适当答复,同时也适当答复

其他进程;如果足够多的进程没有错误,可以对某些值进行投票,最终达成共识.

自 20 世纪 90 年代末创建以来,人们常常很难理解 Paxos

[11]

.后来,Lamport 针对 Basic Pax os

[12]

写了一个更简

单的算法阶段的描述.许多工作已经花费在 Pax os 的形式化规范和验证上.比如:La mport 基于 TLA+

[13]

和

TLAPS

[14]

完成了对 Simple Paxos 的形式化规范和验证,在此基础上,Cha nd 等人完成了对 Multi-Paxos 的验证

[15]

他们运用动作时序逻辑,将算法的规范和证明分别在不同的辅助工具中完成;Kellomaki 采用模型检验的方法,

在 PVS 里将 Simple Paxos 算法抽象为状态、行为以及状态和行为之间的转移关系,对其做了初步地规范和验

证

[16]

;Jaskelioff 等人将 DiskPaxos 的基于 TLA+的规范转换到 Isabe lle/HOL 进行正确性验证

[17]

.近些年来, Padon

等人

[18]

使用一种自动验证分布式协议的 EPR 框架,在这种框架中,他们将算术运算、集合操作以及高阶逻辑全

部抽象为一阶逻辑处理;同时,他们在算法抽象中改变了一些细节处理,如算法的某些请求只是要求向大部分参

与者发送,但是他们要求向所有参与者发送等一些算法层面的改动.Garcia 等人

[19]

将算法抽象为基于多轮次的

读/写的寄存器类抽象,将整个算法区分为不同的模块,基于 Rely/Guarante e 框架实现了模块化的验证.从总体方

法学上讲,本文和上述文献属于同一类工作,依然是采用基于模型的形式化验证,不是对 Paxos 算法在某个具体

程序语言中的代码实现进行验证.与这些工作不同的是,我们基于交互式定理证明工具 Coq, 利用高阶逻辑和归

纳构造演绎原理,将 Basic Paxos 算法涉及的基础类型、数据结构和算法流程进行抽象,以精确的数理定义形式

给出其形式化定义,整个建模过程没有对算法层面做任何更改;同时,整个建模和验证都在 Coq 里完成,没有借助

额外的辅助工具.我们对验证过程的信心完全基于 Coq 的归纳构造演绎原理,没有引入其他的自定义逻辑和验

证框架.此外,与模型检验相比,交互式定理证明的好处是:在算法验证中,我们只要求参与投票的进程数量有限,

而不限制其具体大小.在 Paxos 的形式化建模与验证中,主要解决了以下几个困难点.

(1) 用投票轮次的全序关系解决算法的时序复杂性.

Paxos 是在非拜占庭的异步消息传递系统中解决分布式共识问题的算法.系统中的消息传递可能会延时、

of 13

免费下载

软件学报计算机技术

关注

评论