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

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

头文件处理以及对密码原语操作相关函数、通信模块相关函数以及标准库相关函数的重写;
(2) 对简化后的代码,通过构建函数调用时序图和运行 FCSG-SECS 算法,得到源码对应的函数静态执行
序列;
(3) 在函数调用静态执行序列基础上,对函数调用关系抽象得到协议源码的 Pi 演算模型框架,再逐步函数
体语句抽象、表达式约简得到协议源码的 Pi 演算抽象模型;
(4) 对得到的抽象模型,借助 ProVerif 自动化验证协议规范中规定的安全属性.
第(4)步验证工作借助了现成的支持 Pi 演算模型验证的 ProVerif 工具,只需添加相应的待验证安全属性,此
工作不再赘述.
下面对前 3 步内容涉及的细节进一步阐述.
3.1 对协议代码的预处理

直接在程序设计语言尤其是 C 这样偏底层的语言编写的协议代码上进行形式化分析工作比较困难,需要
对协议源码进行预处理,转换为适合模型抽取的简化代码.
本方案对源码的预处理包含两方面工作.第 1 部分工作是常规的编译预处理,消除宏定义、条件编译宏以
及头文件包含等.这部分处理借助通用的 C 编译器前端预处理选项即可.有所区分的是:“头文件包含”仅处理协
议源码中自定义头文件,对于标准库头文件以及源码项目第三方头文件采用直接注释.这样是为了配合预处理
的第 2 部分工作:函数黑盒化处理.具体需要识别并处理的预处理指令见表 2.
Table 2 Common compilation preprocessing instructions
表 2 常见编译预处理指令
编译预处理指令 说明
#define 宏定义
#undef 撤销宏
#if 条件宏
#ifdef 宏已定义,则编译
#ifndef 宏未定义,则编译
#elif 和#if 配合使用
#endif 结束条件编译
#include 头文件包含
对一个函数的黑盒化处理是指不进入该函数的函数体中去解析该函数的执行逻辑是否正确,而是默认该
函数的实现逻辑和它所声明的执行功能一样.密码学是安全协议实现安全属性的重要基石,在安全协议对应的
代码中也存在很多密码原语相关的操作函数.密码学上一般通过多轮混淆(confusion)、扩散(diffusion)和移位
(shift)等操作来抵抗敌手的分析.密码原语函数的相关代码中同样存在这些逻辑,对这些逻辑的分析会增加协议
源码的分析难度.在基于 Dolve-Yao 模型的协议规范形式化分析通常采用完美密码假设来处理这一问题,在对
代码的形式化分析中同样可以采用这一思路.将协议代码中密码原语操作函数按照 Pi 演算逻辑中的项重写和
等式规则直接替换.同样的,对于协议代码中的通信模块相关函数如 socket 编程接口,也不去探索这些函数实现
细节,用逻辑语言中的消息发送和接收逻辑替代.这一处理可以扩大到标准库或者第三方库中的函数,甚至是协
议源码中任意可信任的函数实现.协议代码的预处理交由用户手工标识配合程序半自动化完成,因为 C2P 工具
的使用对象定位为协议代码开发者或者对代码熟悉的专业人员,而非一般用户.

3.2 获取函数静态执行序列
函数是对程序代码逻辑模块化的编程方式,采用函数组织程序有助于将复杂的程序代码结构分割成代码
块集合.一个 C 语言程序的结构可以表示为一个函数执行序列.
考虑到 C 程序的面向过程的函数结构,我们从程序的函数静态执行序列入手,对程序从结构上进行解析.为
了得到函数静态执行序列,我们设计了能全面反映协议 C 程序代码的函数调用关系的数据结构函数调用时序
图,用缩写 FCSG 表示.