Reasoning about Cloud Storage Systems Based on Separation Logic

被引：0
|
作者：
Jin Z. [1 ,3 ]
Wang H.-P. [1 ,2 ,3 ]
Zhang B.-W. [1 ,3 ]
Zhang L. [1 ,3 ]
Cao Y.-Z. [1 ,3 ]
机构：
[1] Department of Computer Science and Technology, Peking University, Beijing
[2] School of Computer Science and Cyber Engineering, Guangzhou University, Guangzhou
[3] Key Laboratory of High Confidence Software Technologies(MOE), Peking University, Beijing
来源：
Wang, Han-Pin (whpxhy@pku.edu.cn) | 1600年 / Science Press卷 / 43期
基金：
中国国家自然科学基金;
关键词：
Cloud storage systems; Formal verification; Hoare logic; Modeling language; Separation logic;
D O I：
10.11897/SP.J.1016.2020.02227
中图分类号：
学科分类号：
摘要：
The rapid growth of data has restricted the capability of traditional storage technologies to store and manage data. Massive growth in big data generated through Cloud Storage Systems (CSSs) has been observed. Compared with traditional storage systems, CSSs have lots of advantages, such as higher capacity, lower cost, and easier scalability. An important feature of CSSs is that data files are stored in a way of block. That is, the storage resources of CSSs consist of small block spaces with a fixed size. When storing a data file, the system may fist cut the file into some segments, and then put these segments into proper blocks, taking every segment as a whole. Hence, CSSs usually have two kinds of storage units: ordinary locations and block locations. At first glance, the above procedure of saving a file into blocks in a CSS looks similar to that of saving values into memory cells in a memory management system. But there are still some substantial differences. When user submit their data file to CSSs, the file of user uploaded is divided into lots of 128MB segments firstly (the last segment may be less than the others). Then the system allocate those segments to the blocks one by one, and the size of each block is also 128MB. Finally, the system will generate a file table to record the block addresses and the relation between file segments and blocks. These characteristics make the properties of CSS management very different from those of traditional memory management. Although the concept of block storage has been proposed for many years, it becomes more complicated in CSSs. In order to improve the reliability and safety of cloud storage service, the correctness of the cloud storage management problem needs to be verified, which is an urgent problem to solve. While the special characteristics of the cloud storage system make the problem challenging. Then how do we appeal formal methods to model, describe and reason about CSSs? Separation Logic (SL), which is a Hoare-style logic, has a strong theoretical and practical significance. By using SL, some verification systems have been implemented. In this paper, based on SL, we propose a systematic method to verify the correctness of management programs in CSSs. The main contributions are as follows. (1) A language is defined to describe the cloud storage management. The new commands mainly focus on block operations. Accordingly, its operational semantics is given by using the concepts of heap and store. (2) Assertions in SL are extended to describe the properties of blocks in CSSs. Quantifiers over block variables and file variables are incorporated with ordinary SL assertion. (3) Hoare-style rules are proposed to reason about the CSSs. Pre- and post-conditions are pairs of assertions. One component of every pair is used to describe the properties of ordinary locations, while the other component is used to describe the properties of block locations. The soundness of the rules is also proved. Using these methods, the partial correctness of cloud storage management can be verified. © 2020, Science Press. All right reserved.
引用
收藏
页码：2227 / 2240
页数：13
相关论文
共 28 条
  • [1] Hashem I A T, Yaqoob I, Anuar N B, Et al., The rise of "big data" on cloud computing: Review and open research issues, Information Systems, 47, pp. 98-115, (2015)
  • [2] Ghemawat S, Gobioff H, Leung S T., The Google file system, Proceedings of the 19th ACM Symposium on Operating Systems Principles(SOSP 2003), pp. 29-43, (2003)
  • [3] Shvachko K, Kuang H, Radia S, Et al., The Hadoop distributed file system, Proceedings of the 2010 IEEE 26th Symposium on Mass Storage Systems and Technologies, pp. 1-10, (2010)
  • [4] Gimson R., The formal documentation of a block storage service, (1987)
  • [5] Wang Y, Ngolah C F, Tan X, Et al., The formal design model of a file management system (FMS), International Journal of Software Science and Computational Intelligence, 3, 1, pp. 90-113, (2011)
  • [6] Serbanescu V, Pop F, Cristea V, Et al., Architecture of distributed data aggregation service, Proceedings of the 28th International Conference on Advanced Information Networking and Applications(AINA 2014), pp. 727-734, (2014)
  • [7] Serbanescu V, Pop F, Cristea V, Et al., A formal method for rule analysis and validation in distributed data aggregation service, World Wide Web, 18, 6, pp. 1717-1736, (2015)
  • [8] Bansal C, Bhargavan K, Delignat-Lavaud A, Et al., Keys to the cloud: Formal analysis and concrete attacks on encrypted Web storage, Proceedings of the 2nd International Conference on Principles of Security and Trust, pp. 126-146, (2013)
  • [9] Freitas L, Watson P., Formalizing workflows partitioning over federated clouds: Multi-level security and costs, International Journal of Computer Mathematics, 91, 5, pp. 881-906, (2014)
  • [10] James Stephen J, Savvides S, Seidel R, Et al., Program analysis for secure big data processing, Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, pp. 277-288, (2014)
123