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

1584 Journal of Software 软件学报 Vol.32, No.6, June 2021

进程 P,否则执行进程 Q;赋值语句为变量 x 赋值为项 M,赋值成功执行进程 P,失败执行进程 Q;接收消息和发送
消息操作模拟协议通信中的发送和接收消息行为.
Table 1 Process grammar in Pi calculus
表 1 Pi 演算进程语法
P|Q|R::= 进程(process)
0 空进程
P|Q 并发进程
!P 重复进程
new n:t; P 创建新名
if M=N then P else Q 条件
let x=M in P else Q 赋值
in(M,x:t); P 接收消息
out(M,N); P 发送消息

一个协议实体的通信行为可以用这些语法进行描述.例如对称加解密操作的表示中,加密过程看作不解义
的构造函数(constructor):enc(x,y)解密操作视为析构函数(destructor),加解密之间的联系用等式理论代替:
dec(enc(x,y),y)=x.
类似地,公钥加密算法的表示分别对应如下:
enc(x,pk(y));
dec(enc(x,pk(y)),y)=x,
其中,pk(y)表示私钥 y 对应的公钥,同样为不解译函数.采用类似的等式理论可以表示私钥签名等操作.
ProVerif 所支持的 Pi 演算的主要语法描述如上,更多细节可参考相关文档 [11] .

3 从协议 C 代码提取 Pi 演算模型

对安全协议代码进行形式化分析的基本思路是:将协议 C 源代码转换成为 Pi 演算模型,之后借助协议自动
化分析工具 ProVerif 对抽象后的 Pi 模型进行形式化验证分析.我们依据 C 语言面向过程的这种以函数调用组
织起来的结构特点,依次从 C 程序中的函数调用、函数体语句、语句中的表达式这 3 个不同的层次来对安全协
议 C 程序代码来实施形式化抽象.图 1 给出了协议 C 源码验证的整体框架.

2. 静态执行
序列获取 3. 逐级代码抽象
简化代码 构建FCSG 函数调用抽象

函数静态 函数体
1. 预处理 FCSG 执行序列 语句抽象

3. FCSG- 协议Pi演算
协议C源代码 SECS算法 抽象模型 表达式约简

4. ProVerif
安全属性 自动化验证 安全属性违例

Fig.1 Overall security verification framework of C protocol code
图 1 协议 C 源码的安全验证架构
整个验证框架分为 4 个步骤.
(1) 对待分析的目标协议源码进行预处理,预处理任务主要包括基本的预编译处理,如消除宏相关指令、