微信服务号

微信订阅号

2025年4月4日 12:15 星期五
首页 > 过刊浏览>2022年第33卷第6期 >2264-2287. DOI:10.13328/j.cnki.jos.006581
PDF HTML阅读 XML下载 导出引用 引用提醒
一种基于分离逻辑的块云存储系统验证工具
作者:
作者简介:

张博闻(1995−),男,博士生,CCF学生会员,主要研究领域为计算机程序的形式化验证,交互式定理验证工具;王捍贫(1964−),男,博士,教授,博士生导师,主要研究领域为程序逻辑,程序语义,计算机系统的描述与验证;金钊(1990−),男,博士生,主要研究领域为云存储程序的推理验证,可计算理论;曹永知(1974−),男,博士,教授,博士生导师,CCF专业会员,IEEE高级会员,主要研究领域为形式化方法及其应用,隐私性与安全性,不确定性推理

通讯作者:

王捍贫,E-mail:whpxhy@pku.edu.cn

中图分类号:

TP311

基金项目:

国家科技攻关计划(2018YFB1003904,2018YFC1314200);国家自然科学基金(61772035,61972005,61932001)


Tool for Verifying Cloud Block Storage Based on Separation Logic
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [65]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    云存储技术目前被广泛应用于人们的生产与生活中.验证云存储系统中管理程序的正确性,能够有效地提高整个系统的可靠性.块云存储系统(CBS)具有最接近底层的存储架构.运用交互式定理证明器Coq,实现了一种辅助验证工具,用于分析和验证CBS中管理程序的正确性.基于分离逻辑的思想,对工具中证明系统的实现主要包括:首先,将CBS抽象为两层堆结构,定义建模语言形式化表示CBS的状态和管理程序;其次,定义描述CBS状态性质的堆谓词,并说明堆谓词间的逻辑关系;最后,定义描述程序行为的CBS分离逻辑三元组,以及制定验证三元组所需的推理规则.此外,还引入了几个证明实例,以此展示工具对实际CBS管理程序表示和推理的能力.

    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.

    参考文献
    [1] Market and Market. Cloud computing market. 2020. https://www.marketsandmarkets.com/Market-Reports/cloud-computing-market-234.html
    [2] Xinhua. The 14th five-year plan for national economic and social development and the long-range objectives through the year 2035. 2021(in Chinese). http://www.gov.cn/xinwen/2021-03/13/content_5592681.htm
    [3] Mesbahi MR, Rahmani AM, Hosseinzadeh M. Reliability and high availability in cloud computing environments:A reference roadmap. Human-centric Computing and Information Sciences, 2018, 8(1):20-51.
    [4] Tung L. Amazon:Here's what caused the major AWS outage last week. 2020. https://www.zdnet.com/article/amazon-heres-what-caused-major-aws-outage-last-week-apologies/
    [5] Gawanmeh A, Alomari A. Challenges in formal methods for testing and verification of cloud computing systems. Scalable Computing:Practice and Experience, 2015, 16(3):321-332.
    [6] IBM Cloud Education. What is block storage?2019. https://www.ibm.com/cloud/learn/block-storage
    [7] Mike M, Gregory RG, Erik R. Object-based storage. IEEE Communications Magazine, 2003, 41(8):84-90.
    [8] Newcombe C, Rath T, Zhang F, Munteanu B, Brooker M, Deardeuff M. How Amazon Web services uses formal methods. Communications of the ACM, 2015, 58(4):66-73.
    [9] Wing JM. A specifier's introduction to formal methods. Computer, 1990, 23(9):8-22.
    [10] Wang J, Zhan NJ, Feng XY, Liu ZM. Overview of formal methods. Ruan Jian Xue Bao/Journal of Software, 2019, 30(1):33-61(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [11] Gallier JH. Logic for Computer Science:Foundations of Automatic Theorem Proving. Dover Publications, 2015.
    [12] Loveland DW. Automated Theorem Proving:A Logical Basis. Elsevier, 2016.
    [13] Fitting M. First-order Logic and Automated Theorem Proving. Springer Science& Business Media, 2012.
    [14] Reynolds JC. Separation logic:A logic for shared mutable data structures. In:Proc. of the 17th IEEE Symp. on Logic in Computer Science. 2002. 55-74.
    [15] O'Hearn PW. Separation logic. Communications of the ACM, 2019, 62(2):86-95.
    [16] Hoare CAR. An axiomatic basis for computer programming. Communications of the ACM, 1969, 12(10):576-580.
    [17] Qin SC, Xu ZW, Ming Z. Survey of research on program verification via separation logic. Ruan Jian Xue Bao/Journal of Software, 2017, 28(8):2010-2025(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5272.htm[doi:10.13328/j.cnki.jos. 005272]
    [18] Huang DM, Zeng QK. Program verification techniques based on separation logic. Ruan Jian Xue Bao/Journal of Software, 2009, 20(8):2051-2061(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/2051.htm
    [19] Pym D, Spring JM, O'Hearn PW. Why separation logic works. Philosophy& Technology, 2019, 32(3):483-516.
    [20] The Coq proof assistant. https://coq.inria.fr/
    [21] Jiang N, Li QA, Wang LM, Zhang XT, He YX. Overview on mechanized theorem proving. Ruan Jian Xue Bao/Journal of Software, 2020, 31(1):82-112(in Chinese with English abstract). http://www.jos.org.cn/1000-9825/5870.htm[doi:10.13328/j.cnki.jos. 005870]
    [22] Charguéraud A. Program verification through characteristic formulae. In:Proc. of the 16th ACM SIGPLAN Int'l Conf. on Functional Programming. 2010. 321-332.
    [23] Charguéraud A. Characteristic formulae for the verification of imperative programs. In:Proc. of the 17th ACM SIGPLAN Int'l Conf. on Functional Programming. 2011. 418-430.
    [24] Charguéraud A. Higher-order representation predicates in separation logic. In:Proc. of the 5th ACM SIGPLAN Conf. on Certified Programs and Proofs. 2016. 3-14.
    [25] Charguéraud A, Pottier F. Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits. Journal of Automated Reasoning, 2019, 62(3):331-365.
    [26] Charguéraud A. Characteristic formulae for mechanized program verification[Ph.D. Thesis]. Université Paris, 2010.
    [27] Charguéraud A. Separation logic for sequential programs (functional pearl). Proc. of the ACM on Programming Languages, 2020, 116(4):1-34.
    [28] Charguéraud A. Software Foundations, Vol.6:Separation Logic Foundations. Electronic Textbook, 2021.
    [29] Apache. HDFS architecture guide. 2020. https://hadoop.apache.org/docs/r1.2.1/hdfs_design.html
    [30] Jing YX, Wang HP, Huang Y, Zhang L, Xu J, Cao YZ. A modeling language to describe massive data storage management in cyber-physical systems. Journal of Parallel and Distributed Computing, 2017, 103:113-120.
    [31] Jin Z, Wang HP, Zhang BW, Zhang L, Cao YZ. Reasoning about cloud storage systems based on separation logic. Chinese Journal of Computers, 2020, 43(12):2227-2240(in Chinese with English abstract).
    [32] White T. Hadoop:The Definitive Guide. O'Reilly Media Inc., 2012.
    [33] Ghemawat S, Gobioff H, Leung ST. The Google file system. In:Proc. of the 19th ACM Symp. on Operating Systems Principles. 2003. 29-43.
    [34] Apache. HDFS federation. 2016. https://hadoop.apache.org/docs/r2.7.2/hadoop-project-dist/hadoop-hdfs/Federation.html
    [35] Apache. Disk balancer. 2017. https://hadoop.apache.org/docs/r3.0.0/hadoop-project-dist/hadoop-hdfs/HDFSDiskbalancer.html
    [36] Baier C, Katoen JP. Principles of Model Checking. MIT Press, 2008.
    [37] Arkoudas K, Zee K, Kuncak V, Rinard M. Verifying a file system implementation. In:Proc. of the Int'l Conf. on Formal Engineering Methods. 2004. 373-390.
    [38] Freitas L, Woodcock J, Fu Z. POSIX file store in Z/Eves:An experiment in the verified software repository. Science of Computer Programming, 2009, 74(4):238-257.
    [39] Gardner P, Ntzik G, Wright A. Local reasoning for the POSIX file system. In:Proc. of the European Symp. on Programming Languages and Systems. 2014. 169-188.
    [40] Chen HG, Ziegler D, Chajed T, Chlipala A, Kaashoek MF, Zeldovich N. Using Crash Hoare logic for certifying the FSCQ file system. In:Proc. of the 25th Symp. on Operating Systems Principles. 2015. 18-37.
    [41] Blanchard A, Kosmatov N, Lemerre M, Loulergue F. A case study on formal verification of the anaxagoros hypervisor paging system with Frama-C. In:Proc. of the Int'l Workshop on Formal Methods for Industrial Critical Systems. 2015. 15-30.
    [42] Bobba R, Grov J, Gupta I, Liu S. Survivability:Design, formal modeling, and validation of cloud storage systems using Maude. Assured Cloud Computing, 2018, 10-48.
    [43] Pereverzeva I, Laibinis L, Troubitsyna E, Holmberg M, Pöri M. Formal modelling of resilient data storage in cloud. In:Proc. of the Int'l Conf. on Formal Engineering Methods. 2013. 363-379.
    [44] Appel AW, Blazy S. Separation logic for small-step Cminor. In:Proc. of the Int'l Conf. on Theorem Proving in Higher Order Logics. 2007. 5-21.
    [45] Appel AW. Program Logics for Certified Compilers. Cambridge:Cambridge University Press, 2014.
    [46] Cao QX, Beringer L, Gruetter S, Dodds J, Appel AW. VST-Floyd:A separation logic tool to verify correctness of C programs. Journal of Automated Reasoning, 2018, 61(1):367-422.
    [47] Appel AW, Cao QX. Software Foundations, Vol.5:Verifiable C. Electronic Textbook, 2020.
    [48] Yu D, Hamid NA, Shao Z. Building certified libraries for PCC:Dynamic storage allocation. Science of Computer Programming, 2004, 50(1-3):101-127.
    [49] Ni ZZ, Shao Z. Certified assembly programming with embedded code pointers. In:Proc. of the 33rd ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages. 2006. 320-333.
    [50] Feng XY, Shao Z, Vaynberg A, Xiang S, Ni ZZ. Modular verification of assembly code with stack-based control abstractions. ACM SIGPLAN Notices, 2006, 41(6):401-414.
    [51] Feng XY, Ni ZZ, Shao Z, Guo Y. An open framework for foundational proof-carrying code. In:Proc. of the 2007 ACM SIGPLAN Int'l Workshop on Types in Languages Design and Implementation. 2007. 67-78.
    [52] Feng XY, Shao Z, Dong Y, Guo Y. Certifying low-level programs with hardware interrupts and preemptive threads. ACM SIGPLAN Notices, 2008, 43(6):170-182.
    [53] Zhan BH. AUTO2, a saturation-based heuristic prover for higher-order logic. In:Proc. of the Int'l Conf. on Interactive Theorem Proving. 2016. 441-456.
    [54] Jung R, Krebbers R, Jourdan JH, Bizjak A, Birkedal L, Dreyer D. Iris from the ground up:A modular foundation for higher-order concurrent separation logic. Journal of Functional Programming, 2018, 28.
    [55] Bengtson J, Jensen J B, Sieczkowski F, Birkedal L. Verifying object-oriented programs with higher-order separation logic in Coq. In:Proc. of the Int'l Conf. on Interactive Theorem Proving. 2011. 22-38.
    [56] Nanevski A, Morrisett G, Shinnar A, Govereau P, Birkedal L. Ynot:Dependent types for imperative programs. In:Proc. of the 13th ACM SIGPLAN Int'l Conf. on Functional Programming. 2008. 229-240.
    [57] Chlipala A. The Bedrock structured programming system:Combining generative metaprogramming and Hoare logic in an extensible program verifier. In:Proc. of the 18th ACM SIGPLAN Int'l Conf. on Functional programming. 2013. 391-402.
    [58] Calcagno C, Distefano D, Dubreil J, Gabi D, Hooimeijer P, Luca M, O'Hearn PW, Papakonstantinou I, Purbrick J, Rodriguez D. Moving fast with software verification. In:Proc. of the NASA Formal Methods Symp. 2015. 3-11.
    [59] Zou M, Ding HR, Du D, Fu M, Gu RH, Chen HB. Using concurrent relational logic with helpers for verifying the AtomFS file system. In:Proc. of the 27th Symp. on Operating Systems Principles. 2015. 259-274.
    附中文参考文献:
    [2] 新华社.中华人民共和国国民经济和社会发展第十四个五年规划和2035年远景目标纲要. 2021. http://www.gov.cn/xinwen/2021-03/13/content_5592681.htm
    [10] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报, 2019, 30(1):33−61. http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    [17] 秦胜潮,许智武,明仲.基于分离逻辑的程序验证研究综述.软件学报, 2017, 28(8):2010−2025. http://www.jos.org.cn/1000-9825/5272.htm[doi:10.13328/j.cnki.jos.005272]
    [18] 黄达明,曾庆凯.基于分离逻辑的程序验证技术.软件学报, 2009, 20(8):2051−2061. http://www.jos.org.cn/1000-9825/2051. htm
    [21] 江南,李清安,汪吕蒙,张晓瞳,何炎祥.机械化定理证明研究综述.软件学报, 2020, 31(1):82−112. http://www.jos.org.cn/1000-9825/5870.htm[doi:10.13328/j.cnki.jos.005870]
    [31] 金钊,王捍贫,张博闻,张磊,曹永知.基于分离逻辑的云存储系统验证.计算机学报, 2020, 43(12):2227−2240.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

张博闻,金钊,王捍贫,曹永知.一种基于分离逻辑的块云存储系统验证工具.软件学报,2022,33(6):2264-2287

复制
分享
文章指标
  • 点击次数:1005
  • 下载次数: 3839
  • HTML阅读次数: 3029
  • 引用次数: 0
历史
  • 收稿日期:2021-09-07
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-06-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19786036位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号