Formal Verification of Data Modifications in Cloud Block Storage Based on Separation Logic

扫码查看

原文链接

万方数据

外文摘要：Cloud storage is now widely used,but its reliability has always been a major concern.Cloud block storage(CBS)is a famous type of cloud storage.It has the closest architecture to the underlying storage and can provide interfaces for other types.Data modifications in CBS have potential risks such as null reference or data loss.Formal verification of these operations can improve the reliability of CBS to some extent.Although separation logic is a mainstream approach to verifying program correctness,the complex architecture of CBS creates some challenges for verifications.This paper develops a proof system based on separation logic for verifying the CBS data modifica-tions.The proof system can represent the CBS architecture,describe the properties of the CBS system state,and specify the behavior of CBS data modifications.Using the interactive verification approach from Coq,the proof sys-tem is implemented as a verification tool.With this tool,the paper builds machine-checked proofs for the functional correctness of CBS data modifications.This work can thus analyze the reliability of cloud storage from a formal per-spective.

外文关键词：

Formal verificationSeparation logicCloud block storageVerification toolCoq

作者：

Bowen ZHANG、Zhao JIN、Hanpin WANG、Yongzhi CAO

展开 >

作者单位：

Key Laboratory of High Confidence Software Technologies(MOE),School of Computer Science,Peking University,Beijing 100871,China

School of Computer and Artificial Intelligence,Zhengzhou University,Zhengzhou 450001,China

School of Computer Science and Cyber Engineering,Guangzhou University,Guangzhou 510006,China

基金：

National Key R&D Program of ChinaNational Natural Science Foundation of ChinaNational Natural Science Foundation of ChinaNational Natural Science Foundation of China

项目编号：

2021YFF1201102619720056217201661932001

出版年：

2024

DOI：

10.23919/cje.2022.00.116

电子学报(英文)

CSTPCDEI

ISSN：1022-4653

年,卷(期)：2024.33(1)

参考文献量43