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

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

通过转换后的分析表明:代码中存在一条攻击路径,在认证性证明时,单射一致性被打破,参见图 10.代码实
现逻辑中,在第 5 步消息接收时,并未对 IV5 与 IV4 进行比较,即验证 IV5 值的新鲜性,导致攻击者可以在不拥有
任何密钥的情况下,仅利用截获消息来构造攻击路径,从而导致 B 对 A 认证并不满足单射一致性,协议的认证性
被破坏.若可信第三方 S 在局部时间内为 A 和 B 生成的密钥 Kab 不变,攻击者便可以成功构造攻击路径.
表 4 列出了 C2P 方法与相关文献工作的对比情况.文献[9,10]在函数调用语法处理上均需要人工将所有函
数调用改写为 inline 模式,再利用预编译程序处理 inline.本文 C2P 方法可以直接支持函数调用语法的自动化处
理.此外,文献[9,10]仅支持单一执行路径,不支持条件分支语法;而 C2P 方法给出了条件分支的抽象方法.在支持
安全属性验证方面,C2P 与文献[9]都采用了 Pi 演算模型,可以支持符号模型的安全属性验证;而文献[10]采用
Blanchet 演算,支持计算模型的安全属性验证.符号模型基于完美密码假设理论,即认为密码学相关设计完美,攻
击者不具备特殊密码学能力;计算模型则在概率条件下考虑攻击者的破密能力.一般认为:计算模型复杂度高,
但更符合实际安全.因此,把本文方案迁移到计算模型,也是待拓展工作之一.
Table 4 Comparison of related work
表 4 相关工作对比
支持的 C 语法
文献 抽象模型 安全模型
函数调用 条件分支 指针
文献[9] Pi 演算 人工改写 inline 不支持 部分支持 符号模型
文献[10] Blanchet 演算 人工改写 inline 不支持 部分支持 计算模型
C2P Pi 演算 支持 支持 部分支持 符号模型
5 结 语

本文基于 Pi 演算模型给出了一种对 C 语言开发的安全协议源码进行形式化验证的方法,继承了以往工作
先抽象再验证的工作思路以及密码学原语相关函数黑盒化的技巧,并将之拓展到通信模块和可信标准库或第
三方库;通过定义 FCSG 及函数调用静态执行序列获取算法得到函数静态执行序列,并在此基础上,依照函数调
用、函数体语句、表达式约简的顺序逐级对代码进行抽象转换成 Pi 演算模型,借助 ProVerif 自动化验证协议安
全属性;最后,利用 ProVerif 给出了相关抽象的逻辑正确性证明,并通过 Kerberos 协议代码案例分析说明了方法
的有效性;依据方案实现了 C2P 工具并将之开源,以弥补这一领域工作延续性不足的问题.

References:
[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]