计算机应用 ›› 2016, Vol. 36 ›› Issue (2): 505-510.DOI: 10.11772/j.issn.1001-9081.2016.02.0505

• 网络空间安全 • 上一篇    下一篇

面向服务计算的拜占庭容错方案及其正确性证明

陈柳1, 周伟2   

  1. 1. 武汉工程大学 电气信息学院, 武汉 430073;
    2. 华中师范大学 计算机学院, 武汉 430079
  • 收稿日期:2015-08-31 修回日期:2015-10-09 出版日期:2016-02-10 发布日期:2016-02-03
  • 通讯作者: 周伟(1980-),男,湖北襄阳人,讲师,博士,CCF会员,主要研究方向:拜占庭容错、服务计算。
  • 作者简介:陈柳(1979-),女,湖北丹江口人,讲师,博士研究生,主要研究方向:拜占庭容错、引文推荐。
  • 基金资助:
    湖北省教育厅科学技术研究项目(B2015322);武汉工程大学青年基金资助项目(Q201407)。

Byzantine fault tolerance schema for service-oriented computing and its correctness proof

CHEN Liu1, ZHOU Wei2   

  1. 1. School of Electrical and Information Engineering, Wuhan Institute of Technology, Wuhan Hubei 430073, China;
    2. School of Computer, Central China Normal University, Wuhan Hubei 430079, China
  • Received:2015-08-31 Revised:2015-10-09 Online:2016-02-10 Published:2016-02-03

摘要: 针对现有拜占庭容错协议的假设(要求被保护的对象是被动的和独立的)不适用于服务计算等新兴计算模型的问题,提出一种面向服务计算的拜占庭容错协议。该协议在服务请求方和服务提供方两端均创建服务复制品,采用基于状态机的主动复制技术,在服务复制品间进行三轮通信,就该请求的编号和内容达成一致,随后该请求被提交给上层应用逻辑处理;收到应答后,服务请求方的复制品进行三轮通信就应答的编号和内容达成一致后接受该应答。针对现有面向服务计算的拜占庭容错协议只有简单的正确性推理缺乏形式化验证的问题,采用I/O自动机和模拟关系方法进行正确性证明,更加严谨和正式。构造一个高度抽象的简单I/O自动机S,此自动机满足安全性和及时性;将协议中的各方分解成若干简单I/O自动机:前端自动机、后端自动机和多播通道自动机;最后用模拟关系方法证明各成员自动机构成的系统实现了自动机S,从而证明协议的正确性。使用I/O自动机可以精确描述协议,以此为基础进行证明比感性推理的证明方法更加规范。

关键词: 服务计算, 拜占庭容错, 状态机复制, 复制品, 模拟关系

Abstract: A Byzantine Fault Tolerance (BFT) schema was proposed to solve the problem that most Byzantine fault tolerance protocols were not suitable for service-oriented computing and other emerging computing models because of the assumption that the services were passive and independent. Service replicas were created on both sides of service requester and service provider. State machine replication algorithm was used to reach agreement on the ID and the content of the request after three rounds of communications among service replicas. After receiving a request, replicas submitted the request to upper application logic. After receiving the reply, replicas on service requester reached agreement on the ID and the content of the reply after three rounds of communications among services replicas and then accepted the reply. To deal with the problem of only having simple correctness reasoning and lacking of formal verification, an I/O automaton was used to model the protocol and simulation relation method was used as a tool to prove the correctness of the protocol more formally and rigorously. A highly abstract simple I/O automata S was constructed, which meeted safety and liveness. The parties of the protocol were broken down into several simple member I/O automata including front-end automaton, back-end automaton and multicast channel automaton. It is proved that the system composed of member I/O automata realizes the automata S. I/O automaton can accurately describe the protocol, which makes the correctness proof more standard than inductive reasoning.

Key words: service-oriented computing, Byzantine Fault Tolerance(BFT), state machine replication, replica, simulation relation

中图分类号: