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

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

ASPIER 抽象模型才可以在此基础上开展分析工作,因而通用性也有一定损失.类似的工作有文献[13−15],都是
将现有的协议代码抽象成自定义的模型再进行逻辑推演.
文献[9]的工作弥补了这一不足,将安全协议的 C 语言代码转换成为 Pi 演算模型.Pi 演算是一种通用而语法
简洁的协议模型描述语言,且可以直接作为协议自动验证工具 ProVerif 的输入语言模型,从而在符号模型下对
协议 C 代码进行自动化的形式化验证分析.相关团队在文献[10]中将该项工作拓展到计算模型,利用
CryptoVerif 工具进行计算模型下的协议形式化验证.这一工作的不足之处在于:仅支持单一执行路径,不支持函
数调用和条件分支、循环迭代等,在一定程度上削弱了验证框架的适用范畴.但该工作所体现的将协议的 C 语
言代码抽象成已经存在且较成熟的 Pi 演算逻辑模型的研究思路,既方便后续工作拓展,也有利于基于已有形式
化自动化验证工具进行协议代码的安全属性分析.与之类似的工作还有文献[16],其采用类似的思路将程序设
计语言 F#所编写的协议代码转换为 Pi 演算和 Blanchet 演算,然后借助 ProVerif 工具进行自动化的形式化验证.
还有一部分工作将这种思路应用到 Java 语言编写的协议代码形式化验证中,如文献[7],通过将安全协议的 Java
代码抽象成 Blanchet 演算,从而利用 CryptoVerif 工具对抽象后的模型进行自动化的形式化验证分析.文献
[17,18]也是采用先抽象再验证的思路,与其他工作的不同之处在于,这些工作应用了 Petri 网理论模型:首先将安
全协议程序转换成对应的 Petri 网模型,然后借助 Petri 网理论来分析协议的通信行为是否满足相关的安全属性.
此项工作的意义在于为协议实现的形式化分析研究引进了新的工具 Petri 网理论,但同时仍然有很多待研究解
决的问题.
本文沿用了先模型抽象再验证的研究思路.与现有工作相比,直接在源码层面做抽象,支持更多的 C 语法抽
象如函数调用,适用于代码规模较大的协议实现分析.另一方面,现有工作的共性不足之处在于工作缺乏延续
性,或仅限于团队内部延续,这很大程度上源于该领域在复现他人工作方面并不平凡.为此,本文将 C2P 工具的代
码开源,希望对这一现状有所改善.
2 相关基础

2.1 协议源码验证
为理解协议协议源码验证和传统的源码安全测试工作的不同,在此给出协议源码的验证的定义.
定义 2.1(协议源码验证). 给定一个协议 Pro 的规范 S(Pro)和由程序设计语言 L 编码的协议实现 P(Pro)[L],
验证 S(Pro)中可满足的安全属性ϕ在 P(Pro)[L]中也是可满足的过程:
S(Pro)Bϕ⇒P(Pro)[L]Bϕ
称为对协议 Pro 的 L 源码的安全属性验证,简称为协议源码验证.
根据定义 2.1,协议源码验证工作的对象是某种具体编程语言实现的安全协议源码,如本文的研究对象即 C
语言实现的协议源码,即 P(Pro)[C-Language].研究的目标是安全属性是否满足,而非一般的代码级问题.
2.2 Pi演算语法
Pi 演算(Pi calculus) [12] 是一个用于并行系统之间通信行为建模的理论,其模型简洁且具有强大的表达能力.
著名的安全协议验证工具 ProVerif 的输入语言便是扩展的 Pi 演算.本节对这种扩展的 Pi 演算语言进行简单介
绍,为便于描述,后文提到的 Pi 演算特指 ProVerif 的输入模型.
Pi 演算语法中的项(term)是由名(names)、变量(variables)和构造/析构函数(constructor/destructor)组成的.
形式化定义如下:
M,N::=a,b,c,…|x,y,z,…|h(M 1 ,…,M k )|M=N|M<>N|M&&N|not(M),
其中,a,b,c∈C;x,y,z∈V;h∈Σ为 names 的集合,V 为变量集合,Σ为函数符号集合;=和<>表示等式和不等式关系,&&,
||和 not 对应与或非逻辑关系;项可以用于描述安全协议通信中的消息,函数可以用于对加密原语的描述.
在 Pi 演算中,进程(process)是用于描述一系列协议行为.Pi 演算中,进程的定义见表 1.其中:空进程表示无实
义操作;并发进程为两个进程同时运行;创建新名是为进程 P 创建私有名;条件语句为比较项 M 和 N,相等则执行