微信服务号

微信订阅号

2025年4月3日 15:39 星期四
首页 > 过刊浏览>2021年第32卷第6期 >1581-1596. DOI:10.13328/j.cnki.jos.006238
PDF HTML阅读 XML下载 导出引用 引用提醒
C2P:基于Pi演算的协议C代码形式化抽象方法和工具
作者:
作者简介:

张协力(1992-),男,硕士,主要研究领域为网络安全协议.
顾纯祥(1976-),男,博士,教授,博士生导师,主要研究领域为网络安全,密码学.
祝跃飞(1962-),男,博士,教授,博士生导师,主要研究领域为网络安全,密码学.
陈熹(1988-),男,硕士,讲师,主要研究领域为网络空间安全,密码学,计算机网络.

通讯作者:

顾纯祥，gcxiang5209@163.com

基金项目:

国家重点研发计划（2019QY1302）


C2P: Formal Abstraction Method and Tool for C Protocol Code Based on Pi Caculus
Author:
Fund Project:

National Key Research and Development Program of China (2019QY1302)

  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [21]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    形式化方法为安全协议分析提供了理论工具，但经过形式化验证过的协议标准在转换为具体程序实现时，可能无法满足相应的安全属性.为此，提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型，基于Pi演算模型对协议安全属性形式化验证.最后给出了方案转换的正确性证明，并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合，能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助.

    Abstract:

    Formal method provides a theoretical tool for security protocol analysis, but the theoretical security is not equivalent to the actual security. A verified protocol standard may not meet the required security properties when converted into a concrete program. Hence, a formal verification method for detecting semantic logic errors in security protocol code is proposed. By automatically abstracting the C source code of the protocol into Pi calculus model, protocol security properties are verified based on the Pi calculus. Finally, the correctness of the scheme transformation is proved and the validity of the method is verified by a Kerberos protocol instance code. C2P tools implemented can help protocol developers to detect semantic logic errors in code.

    参考文献
    [1] Goubault-Larrecq J, Parrennes F. Cryptographic protocol analysis on real C code. In:Cousot R, ed. Proc. of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin:Springer-Verlag, 2005. 363-379.[doi:10.1007/978-3-540-30579-8_24]
    [2] Avalle M, Pironti A, Sisto R. Formal verification of security protocol implementations:A survey. Formal Aspects of Computing, 2014,26(1):99-123.[doi:10.1007/s00165-012-0269-9]
    [3] Meng B, Lu JT, Wang DJ, He XD. Survey of security analysis of security protocol implementations. Journal of Shandong University (Natural Science), 2018,53(1):1-18(in Chinese with English abstract).[doi:10.6040/j.issn.1671-9352.2.2017.067]
    [4] Zhang HG, Wu FS, Wang HZ, Wang ZY. A survey:Security verification analysis of cryptographic protocols implementations on real code. Chinese Journal of Computers, 2018,41(2):288-308(in Chinese with English abstract).[doi:10.11897/SP.J.1016.2018. 00288]
    [5] Kobeissi N. Formal verification for real-world cryptographic protocols and implementations[Ph.D. Thesis]. Paris:Ecole Normale Supérieure de Paris, 2018.
    [6] He X, Liu Q, Chen S, Huang C, Wang DJ, Meng B. Analyzing security protocol Web implementations based on model extraction with applied PI calculus. IEEE Access, 2020,8:26623-26636.[doi:10.1109/ACCESS.2020.2971615]
    [7] Li ZM, Meng B, Wang DJ, et al. Mechanized verification of cryptographic security of cryptographic security protocol implementation in JAVA through model extraction in the computational model. Journal of Software Engineering, 2015,9(1):1-32.[doi:10.3923/jse.2015.1.32]
    [8] Chaki S, Datta A. ASPIER:An automated framework for verifying security protocol implementations. In:Proc. of the 22nd IEEE Computer Security Foundations Symp. New York:IEEE, 2009. 172-185.[doi:10.1109/CSF.2009.20]
    [9] Aizatulin M, Gordon AD, Jürjens J. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In:Chen Y, ed. Proc. of the 18th ACM Conf. on Computer and Communications Security. New York:ACM, 2011. 331-340.[doi:10.1145/2046707.2046745]
    [10] Aizatulin M, Gordon AD, Jürjens J. Computational verification of C protocol implementations by symbolic execution. In:Yu T, ed. Proc. of the 2012 ACM Conf. on Computer and Communications Security. New York:ACM, 2012. 712-723.[doi:10.1145/2382196.2382271]
    [11] Blanchet B. Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Foundations and Trends® in Privacy and Security, 2016,1(1-2):1-135.
    [12] Milner R. Communicating and Mobile Systems:The Pi Calculus. London:Cambridge University Press, 1999.
    [13] Kiyomoto S, Ota H, Tanaka T. A security protocol compiler generating C source codes. In:Proc. of the 2008 Int'l Conf. on Information Security and Assurance (ISA 2008). Piscataway:IEEE, 2008. 20-25.
    [14] Backes M, Maffei M, Unruh D. Computationally sound verification of source code. In:Al-Shaer E, ed. Proc. of the 17th ACM Conf. on Computer and Communications Security. New York:ACM, 2010. 387-398.[doi:10.1145/1866307.1866351]
    [15] Jürjens J. Automated security verification for crypto protocol implementations:Verifying the Jessie project. Electronic Notes in Theoretical Computer Science, 2009,250(1):123-136.[doi:10.1016/j.entcs.2009.08.009]
    [16] Bhargavan K, Fournet C, Gordon AD, Tse S. Verified interoperable implementations of security protocols. ACM Trans. on Programming Languages and Systems (TOPLAS), 2008,31(1):1-61.[doi:10.1145/1452044.1452049]
    [17] Tang WS, Gou ZL, Ahmadon MAB, Yamaguchi S. On verification of implementation of security specification with Petri nets' protocol inheritance. In:Proc. of the IEEE 5th Global Conf. on Consumer Electronics. Piscataway:IEEE, 2016. 1-4.[doi:10.1109/GCCE.2016.7800491]
    [18] Ahmadon MAB, Yamaguchi S, Gupta BB. Petri net-based verification of security protocol implementation in software evolution. Int'l Journal of Embedded Systems, 2018,10(6):503-517.[doi:10.1504/IJES.2016.10011276]
    附中文参考文献:
    [3] 孟博,鲁金钿,王德军,何旭东.安全协议实施安全性分析综述.山东大学学报(理学版),2018,53(1):1-18.[doi:10.6040/j.issn.1671-9352.2.2017.067]
    [4] 张焕国,吴福生,王后珍,王张宜.密码协议代码执行的安全验证分析综述.计算机学报,2018,41(2):288-308.[doi:10.11897/SP.J. 1016.2018.00288]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

张协力,祝跃飞,顾纯祥,陈熹. C2P:基于Pi演算的协议C代码形式化抽象方法和工具.软件学报,2021,32(6):1581-1596

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

京公网安备 11040202500063号