Cloud storage systems are crucial for ensuring business stability and data reliability. Among them, block-based cloud storage systems (BCSSs) have been widely adopted in the industry due to their high efficiency and strong performance. However, system failures occur from time to time, causing significant financial losses to companies. Therefore, verifying the reliability of BCSSs has become important and urgent. Nevertheless, since blocks in these systems are of finite but variable sizes, it is difficult to describe and verify properties using first-order logic or separation logic. To address this issue, we propose Sequence-Heap Separation Logic (SeqSL), which introduces sequence values and sequence variables into separation logic. Our logic can simplify property expressions while enhancing the ability to describe these systems. To provide a theoretical foundation for verification, we study the decidability of this logic, with the main conclusions as follows. 1) The satisfiability problem of the fragment with a single quantifier alternation is decidable, and belongs to 2-EXPTIME (2-Exponential Time). As a by-product, we propose a decision procedure for this decidable fragment. 2) The satisfiability problem of the fragment with two quantifier alternations is undecidable.

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 modifications. 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 system 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 perspective.