Page 7 - 《软件学报》2021年第6期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(6):1581−1596 [doi: 10.13328/j.cnki.jos.006238] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
C2P:基于 Pi 演算的协议 C 代码形式化抽象方法和工具

1,2
1,2
1,2
张协力 , 祝跃飞 , 顾纯祥 , 陈 熹 1,2
1
(数学工程与先进计算国家重点实验室,河南 郑州 450001)
2 (网络密码技术河南省重点实验室,河南 郑州 450002)
通讯作者: 顾纯祥, E-mail: gcxiang5209@163.com

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

中文引用格式: 张协力,祝跃飞,顾纯祥,陈熹.C2P:基于 Pi 演算的协议 C 代码形式化抽象方法和工具.软件学报,2021,32(6):
1581−1596. http://www.jos.org.cn/1000-9825/6238.htm
英文引用格式: Zhang XL, Zhu YF, Gu CX, Chen X. C2P: Formal abstraction method and tool for c protocol code based on Pi
caculus. Ruan Jian Xue Bao/Journal of Software, 2021,32(6):1581−1596 (in Chinese). http://www.jos.org.cn/1000-9825/6238.htm
C2P: Formal Abstraction Method and Tool for C Protocol Code Based on Pi Caculus

1,2
1,2
1,2
ZHANG Xie-Li , ZHU Yue-Fei , GU Chun-Xiang , CHEN Xi 1,2
1 (State Key Laboratory of Mathematical Engineering and Advanced Computing, Zhengzhou 450001, China)
2 (Henan Key Laboratory of Network Cryptography Technology, Zhengzhou 450002, China)
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.
Key words: protocol implementation; formal verification; Pi calculus; model extraction; ProVerif

形式化方法在对安全协议的分析中取得了显著成果,并促进了很多协议草案的设计完善.但理论上的安全
并不能保证实际部署中协议的安全属性满足,经过形式化验证安全的协议,在转换成具体实现时可能依然存在
安全问题.协议实现中的安全问题既有一般性的低级别错误如缓冲区溢出,也包含了语义实现中的逻辑错误:第
1 类安全问题可以借助通用的代码审计技术等来弥补;第 2 类语义逻辑错误问题更为隐蔽,难以借助现有的软件
测试技术如 Fuzzing 来发掘.

∗ 基金项目: 国家重点研发计划(2019QY1302)
Foundation item: National Key Research and Development Program of China (2019QY1302)
本文由“形式化方法与应用”专题特约编辑田聪教授推荐.
收稿时间: 2020-07-29; 修改时间: 2020-10-26, 2020-12-19; 采用时间: 2021-01-18; jos 在线出版时间: 2021-02-07