| 本文已被：浏览 1783次 下载 5077次 |
码上扫一扫！ |
|
|
| 一种基于分离逻辑的块云存储系统验证工具 |
|
张博闻1,2, 金钊1,2, 王捍贫1,3,2, 曹永知1,2
|
|
1.北京大学计算机学院, 北京 100871;2.高可信软件技术教育部重点实验室(北京大学), 北京 100871;3.广州大学计算机科学与网络工程学院, 广东 广州 510006
|
|
| 摘要: |
| 云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力. |
| 关键词: 分离逻辑 交互式定理证明器 块云存储系统 形式化验证 Coq |
| DOI：10.13328/j.cnki.jos.006581 |
| 分类号:TP311 |
| 基金项目:国家科技攻关计划(2018YFB1003904,2018YFC1314200);国家自然科学基金(61772035,61972005,61932001) |
|
| Tool for Verifying Cloud Block Storage Based on Separation Logic |
|
ZHANG Bo-Wen1,2, JIN Zhao1,2, WANG Han-Pin1,3,2, CAO Yong-Zhi1,2
|
|
1.School of Computer Science, Peking University, Beijing 100871, China;2.Key Laboratory of High Confidence Software Technologies of Ministry of Education (Peking University), Beijing 100871, China;3.School of Computer Science and Cyber Engineering, Guangzhou University, Guangzhou 510006, China
|
| Abstract: |
| 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. |
| Key words: separation logic interactive theorem prover cloud block storage formal verification Coq |
