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

ZHANG Bowen; JIN Zhao; WANG Hanpin; CAO Yongzhi

doi:10.23919/cje.2022.00.116

Volume 33 Issue 1

Jan. 2024

Turn off MathJax

Article Contents

Article Navigation > Chinese Journal of Electronics > 2024 > 33(1): 112-127

Bowen ZHANG, Zhao JIN, Hanpin WANG, et al., “Formal Verification of Data Modifications in Cloud Block Storage Based on Separation Logic,” Chinese Journal of Electronics, vol. 33, no. 1, pp. 112–127, 2024 doi: 10.23919/cje.2022.00.116

Citation:

Bowen ZHANG, Zhao JIN, Hanpin WANG, et al., “Formal Verification of Data Modifications in Cloud Block Storage Based on Separation Logic,” Chinese Journal of Electronics, vol. 33, no. 1, pp. 112–127, 2024 doi: 10.23919/cje.2022.00.116

Citation:

PDF( 3422 KB)

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

doi: 10.23919/cje.2022.00.116

ZHANG Bowen^1
,,
JIN Zhao^{3, 1
,},
WANG Hanpin^{2, 1
,
,},
CAO Yongzhi^1
,

1.
Key Laboratory of High Confidence Software Technologies (MOE), School of Computer Science, Peking University, Beijing 100871, China
2.
School of Computer Science and Cyber Engineering, Guangzhou University, Guangzhou 510006, China
3.
School of Computer and Artificial Intelligence, Zhengzhou University, Zhengzhou 450001, China

More Information

Author Bio:
Bowen ZHANG is a Ph.D. candidate at the School of Computer Science, Peking University, China. His current research interests include formal verification, interactive theorem proving, cloud block storage, and Coq. (Email: zhangbowen@pku.edu.cn)

Zhao JIN received the Ph.D. degree from the Peking University, China, in 2022. He is working in the School of Computer and Artificial Intelligence, Zhengzhou University, China. His current research interests include program semantics, programming logic, and formal verification. (Email: jinzhao@pku.edu.cn)

Hanpin WANG received the Ph.D. degree from the Beijing Normal University, China, in 1993. He is a Professor at the School of Computer Science, Peking University, China. His current research interests include programming logic, formal semantics, description and verification of computer systems. (Email: whpxhy@pku.edu.cn)

Yongzhi CAO received the Ph.D. degree from the Beijing Normal University, China, in 2003. He is a Professor at the School of Computer Science, Peking University, China. His current research interests include formal methods and their applications, privacy and security, and reasoning about uncertainty. (Email: caoyz@pku.edu.cn)
Corresponding author: Email: whpxhy@pku.edu.cn
Received Date: 2022-05-03
Accepted Date: 2022-10-08

Available Online: 2022-12-11

Publish Date: 2024-01-05

Abstract

Abstract

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.
- Formal verification,
- Separation logic,
- Cloud block storage,
- Verification tool,
- Coq

FullText(HTML)

References(43)

References

[1]	M. R. Mesbahi, A. M. Rahmani, and M. Hosseinzadeh, “Reliability and high availability in cloud computing environments: a reference roadmap,” Human-Centric Computing and Information Sciences, vol. 8, no. 1, article no. 20, 2018. doi: 10.1186/s13673-018-0143-8
[2]	L. Tung, “Amazon: here’s what caused the major AWS outage last week,” Available at: https://www.zdnet.com/article/amazon-heres-what-caused-major-aws-outage-last-week-apologies/, 2020.
[3]	A. Gawanmeh and A. Alomari, “Challenges in formal methods for testing and verification of cloud computing systems,” Scalable Computing:Practice and Experience, vol. 16, no. 3, pp. 321–332, 2015. doi: 10.12694/scpe.v16i3.1104
[4]	IBM Cloud Education, “What is block storage?,” Available at: https://www.ibm.com/cloud/learn/block-storage, 2019.
[5]	M. Mesnier, G. R. Ganger, and E. Riedel, “Object-based storage,” IEEE Communications Magazine, vol. 41, no. 8, pp. 84–90, 2003. doi: 10.1109/MCOM.2003.1222722
[6]	K. Shvachko, H. R. Kuang, S. Radia, et al., “The hadoop distributed file system,” in Proceedings of the 26th IEEE Symposium on Mass Storage Systems and Technologies, Incline Village, NV, USA, pp. 1–10, 2010.
[7]	Apache, “HDFS architecture guide,” Available at: https://hadoop.apache.org/docs/r1.2.1/hdfs_design.html, 2020.
[8]	C. Newcombe, T. Rath, F. Zhang, et al., “How Amazon web services uses formal methods,” Communications of the ACM, vol. 58, no. 4, pp. 66–73, 2015. doi: 10.1145/2699417
[9]	J. M. Wing, “A specifier’s introduction to formal methods,” Computer, vol. 23, no. 9, pp. 8–22, 1990. doi: 10.1109/2.58215
[10]	J. H. Gallier, Logic for Computer Science: Foundations of Automatic Theorem Proving, 2nd ed., Dover Publications, New York, NY, USA, pp. 1–12, 2015.
[11]	J. C. Reynolds, “Separation logic: A logic for shared mutable data structures,” in Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, Copenhagen, Denmark, pp. 55–74, 2002.
[12]	P. O'Hearn, “Separation logic,” Communications of the ACM, vol. 62, no. 2, pp. 86–95, 2019. doi: 10.1145/3211968
[13]	C. A. R. Hoare, “An axiomatic basis for computer programming,” Communications of the ACM, vol. 12, no. 10, pp. 576–580, 1969. doi: 10.1145/363235.363259
[14]	S. C. Qin, Z. W. Xu, and Z. Ming, “Survey of research on program verification via separation logic,” Journal of Software, vol. 28, no. 8, pp. 2010–2025, 2017. (in Chinese) doi: 10.13328/j.cnki.jos.005272
[15]	D. Pym, J. M. Spring, and P. O'Hearn, “Why separation logic works,” Philosophy & Technology, vol. 32, no. 3, pp. 483–516, 2019. doi: 10.1007/s13347-018-0312-8
[16]	Inria, “The Coq proof assistant,” Available at: https://coq.inria.fr/, 2021.
[17]	N. A. Hamid and Z. Shao, “Interfacing Hoare logic and type systems for foundational proof-carrying code,” in Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics, Park City, UT, USA, pp. 118–135, 2004.
[18]	B. W. Zhang, Z. Jin, H. P. Wang, et al., “A tool for verifying cloud block storage based on separation logic,” Journal of Software, vol. 33, no. 6, pp. 2264–2287, 2022. (in Chinese) doi: 10.13328/j.cnki.jos.006581
[19]	J. Backfield, Becoming Functional: Steps for Transforming Into A Functional Programmer. O’Reilly Media, Inc., Sebastopol, CA, USA, pp. 1–3, 2014.
[20]	T. White, Hadoop: The Definitive Guide, 3rd ed., O'Reilly Media, Inc., Sebastopol, CA, USA, pp. 43–53, 2012.
[21]	Apache, “Append to files in HDFS,” Available at: https://issues.apache.org/jira/browse/HADOOP-1700, 2016.
[22]	Apache, “HDFS truncate,” Available at: https://issues.apache.org/jira/ browse/HDFS-3107, 2016.
[23]	Amazon, “Amazon elastic block store,” Available at: https://docs.aws.amazon.com/AWSEC2/latest/UserGuide/AmazonEBS.html, 2022.
[24]	L. Cardelli and P. Wegner, “On understanding types, data abstraction, and polymorphism,” ACM Computing Surveys, vol. 17, no. 4, pp. 471–523, 1985. doi: 10.1145/6041.6042
[25]	B. Biering, L. Birkedal, and N. Torp-Smith, “BI hyperdoctrines and higher-order separation logic,” in Proceedings of the 14th European Symposium on Programming, Edinburgh, UK, pp. 233–247, 2005.
[26]	C. Baier and J. P. Katoen, Principles of Model Checking. MIT Press, Cambridge, MA, USA, pp. 7–16, 2008.
[27]	H. G. Chen, D. Ziegler, T. Chajed, et al., “Using Crash Hoare logic for certifying the FSCQ file system,” in Proceedings of the 25th Symposium on Operating Systems Principles, Monterey, CA, USA, pp. 18–37, 2015.
[28]	H. G. Chen, T. Chajed, A. Konradi, et al., “Verifying a high-performance crash-safe file system using a tree specification,” in Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, pp. 270–286, 2017.
[29]	K. Arkoudas, K. Zee, V. Kuncak, et al., “Verifying a file system implementation,” in Proceedings of the 6th International Conference on Formal Engineering Methods, Seattle, WA, USA, pp. 373–390, 2004.
[30]	P. Gardner, G. Ntzik, and A. Wright, “Local reasoning for the POSIX file system,” in Proceedings of the 23rd European Symposium on Programming Languages and Systems, Grenoble, France, pp. 169–188, 2014.
[31]	I. Pereverzeva, L. Laibinis, E. Troubitsyna, et al., “Formal modelling of resilient data storage in cloud,” in Proceedings of the 15th International Conference on Formal Engineering Methods, Queenstown, New Zealand, pp. 363–379, 2013.
[32]	R. Bobba, J. Grov, I. Gupta, et al., “Survivability: Design, formal modeling, and validation of cloud storage systems using Maude,” in Assured Cloud Computing, R. H. Campbell, C. A. Kamhoua, and K. A. Kwiat, Eds. Wiley-IEEE Press, Hoboken, NJ, USA, pp. 10–48, 2018.
[33]	A. Blanchard, N. Kosmatov, M. Lemerre, et al., “A case study on formal verification of the Anaxagoros hypervisor paging system with Frama-C,” in Proceedings of the 20th International Workshop on Formal Methods for Industrial Critical Systems, Oslo, Norway, pp. 15–30, 2015.
[34]	Y. X. Jing, H. P. Wang, Y. Huang, et al., “A modeling language to describe massive data storage management in cyber-physical systems,” Journal of Parallel and Distributed Computing, vol. 103, pp. 113–120, 2017. doi: 10.1016/j.jpdc.2016.12.008
[35]	Z. Jin, H. P. Wang, B. W. Zhang, et al., “Reasoning about cloud storage systems based on separation logic,” Chinese Journal of Computers, vol. 43, no. 12, pp. 2227–2240, 2020. (in Chinese) doi: 10.11897/SP.J.1016.2020.02227
[36]	Z. Jin, B. W. Zhang, L. Zhang, et al., “An adaptation-complete proof system for local reasoning about cloud storage systems,” Theoretical Computer Science, vol. 903, pp. 39–73, 2022. doi: 10.1016/j.tcs.2021.12.018
[37]	A. Charguéraud, “Separation logic for sequential programs (functional pearl),” Proceedings of the ACM on Programming Languages, vol. 4, no. ICFP, article no. 116, 2020. doi: 10.1145/3408998
[38]	A. Charguéraud, “Software foundations (6): Separation logic foundations,” Electronic Textbook, Version 1.6 (Coq 8.17 or later), 2023-08-23.
[39]	R. Jung, R. Krebbers, J. H. Jourdan, et al., “Iris from the ground up: A modular foundation for higher-order concurrent separation logic,” Journal of Functional Programming, vol. 28, article no. e20, 2018. doi: 10.1017/S0956796818000151
[40]	J. Bengtson, J. B. Jensen, F. Sieczkowski, et al., “Verifying object-oriented programs with higher-order separation logic in Coq,” in Proceedings of the 2nd International Conference on Interactive Theorem Proving, Berg en Dal, The Netherlands, pp. 22–38, 2011.
[41]	A. Nanevski, G. Morrisett, A. Shinnar, et al., “Ynot: Dependent types for imperative programs,” in Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, Victoria, BC, Canada, pp. 229–240, 2008.
[42]	A. Chlipala, “The Bedrock structured programming system: combining generative metaprogramming and Hoare logic in an extensible program verifier,” in Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, Boston, MA, USA, pp. 391–402, 2013.
[43]	C. Calcagno, D. Distefano, J. Dubreil, et al., “Moving fast with software verification,” in Proceedings of the 7th International Symposium on NASA Formal Methods, Pasadena, CA, USA, pp. 3–11, 2015.