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

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

示例代码对应的 FCSG 表示为 G=(F,R,S,f 0 ),其中,
• F={main,bar,foo};
• R={〈main,bar〉,〈bar,foo〉〈main,foo〉,〈main,bar〉 2 };
• S={〈main,bar〉→1,〈main,foo〉→2,〈main,bar〉 2 →3,〈bar,foo〉→1};
• f 0 =main.
通过 FCSG-SECS 算法可得到程序代码在静态执行下的函数访问序列:
[〈main,bar〉,〈bar,foo〉,〈main,foo〉,〈main,bar〉,〈bar,foo〉].
这与代码在静态执行过程中的函数调用顺序是一致的(实际执行中的函数调用序列可能会因为条件判断
语句等因素产生偏差).为了简化分析,还可以根据人工经验,将一些无用的 FCSG 分支修剪.
从程序 P 的 C 语言程序源码构建程序对应的 FCSG,根据程序源码的抽象语法树识别定位所有函数声明、
函数定义、函数调用点位置,进一步构建协议代码实现的函数调用时序图.有很多现成的开源工具可以从程序
源码中抽取函数调用关系图,FCSG 的构建只需要在这些逻辑上添加函数调用的时序信息即可.

3.3 逐级代码抽象
函数调用执行序列构成了协议 C 源码的程序框架结构.通过对源码中函数调用关系的抽象,构建协议 C 源
码对应的 Pi 演算抽象模型框架,本文对函数调用关系的抽象依赖于函数调用静态执行序列;再通过函数体语句
抽象过程将一般的代码语句转换为形式化逻辑;最后,基于函数上下文关系将表达式约简得到协议源码的 Pi 演
算抽象模型.
3.3.1 函数调用关系抽象
将 C 语言程序中的函数调用关系转换为 Pi 演算的形式化逻辑描述这一工作并不是平凡的.函数调用关系
在 Pi 演算逻辑中表示的难点如下.
• Pi 演算逻辑中的进程宏仅支持并行进程语法,不能在逻辑上直接表达函数调用者与被调用者之间的
关系;
• Pi 演算中的构造和析构函数对整个函数过程进行了黑盒抽象,不适用于一般函数的逻辑抽象.
Pi 演算的形式化逻辑中虽然有过程宏、函数等概念,但这二者与程序设计语言中的函数并不等同.如前文
所述:Pi 演算中的函数可以用于代码中抽象密码原语操作、基础通信操作以及 C 标准库中的函数;Pi 演算中的
进程宏(process macros)与 C 语言程序中的函数相近,可以用于定义子进程(sub-processes);缺乏处理结果返回机
制,且在语法上仅支持子进程的并行,不能直接表达多个子进程之间的顺序执行结构的语义.
为了在 Pi 演算逻辑中模拟 C 程序中的普通函数调用语义,本文在函数静态执行序列的基础上,综合运用了
Pi 演算逻辑中的进程宏、并行进程、私有通信这 3 种机制,实现了对 C 程序中的函数调用关系进行等价逻辑
转换(证明见第 4.2 节).
对函数调用抽象的步骤如下.
1) 基于 FCSG-SECS 算法获取函数调用静态执行序列;
2) 根据函数调用静态执行序列,为每一次函数调用关系都分配了全局唯一的正整数调用编号,简记为
CALL_ID.如:对于在哈数调用静态执行序列中出现的第 n 个函数调用关系〈A,B〉,其对应的编号
CALL_ID〈A,B〉为 n;
3) 以 CALL_ID 为编号,为每次调用关系创建两个临时信道 C_〈CALL_ID〉和 S_〈CALL_ID〉,对 CALL_ID=n,
对应的临时信道为 C_n,S_n;
4) 对所有的函数调用关系执行转换,如图 3 所示.
(1) 第 CALL_ID=n 次函数调用关系〈A,B〉看作相应的 A 进程和 B 进程并行执行;
(2) 调用者 A 在信道 C_n 上发送空消息,并在相应的 S_n 信道上等待接收返回值信息,然后继续执行
剩余代码逻辑;