一种基于分离逻辑的块云存储系统验证工具

Tool for Verifying Cloud Block Storage Based on Separation Logic

云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

Cloud storage is now widely used in production and people’s life. Verifying the correctness of hypervisors in cloud storage can effectively improve the reliability of the whole system. Cloud block storage(CBS) has the closest storage architecture to the bottom layer.In this study, a tool is implemented for analyzing and verifying the correctness of hypervisors in CBS, by using the interactive theorem prover Coq. Based on separation logic, the implementation of the proof system in the tool mainly consists: First, a modeling language is defined to abstract the CBS into a two-tier structure, and to formally represent the CBS state and the hypervisor;second, several predicates are defined to describe the state properties of the CBS, and the logical relationships between predicates are illustrated;finally, a separation logic triple for CBS is defined to describe the behavior of a program, and the reasoning rules required to verify the triples are stated. In addition, several proof examples are introduced in this study, to present the tool’s ability to represent and reason about the real hypervisor in CBS.