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

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

(3) 被调用者 B 在信道 C_n 上监听,有空消息到来时执行 B 函数体逻辑,最后将返回值在信道 S_n
上发出,然后执行结束.
空消息
创建 信道C_n
1 2
调用者A 被调用者
副本B_n
4 3
创建 信道S_n
返回值
Fig.3 Function call simulation
图 3 函数调用模拟

第 4)步骤中,将每次函数调用都看作调用者和被调用者在专有信道上的并行通信行为.双方采用在临时信
道来模拟调用者与被调用者之间的执行同步.两个进程在形式上是并行的,通过通信同步执行顺序,同时也解决
了函数返回值传递问题.图 4 给出了函数抽象更具体的转换细节:左边为示例的 C 代码,描述了 A 中调用了函数
B;中间为转换后 A 函数的 Pi 演算抽象;右边为 B 函数的 Pi 演算抽象.在 Pi 演算中,A 和 B_n 进程并行,A 中新建
了两个信道 C_n 和 S_n,并通过 out(C_n,(⋅))发送空消息触发 B_n 中的 in(C_n,(⋅));同样,B 进程中的 out(S_n,value)
将 B 函数返回值发送回 A,并触发其函数调用后的执行逻辑.C_n,S_n 与 B 函数原有参数一起传送给 B_n 进程.

Fig.4 Function call abstraction
图 4 函数调用关系抽象
需要强调的是,为了符合 Pi 演算的语法规范和满足正确的逻辑,在实际转换时,
• 两个临时信道由调用者以创建新名的方式创建,以过程宏参数的形式传给被调用函数,其作用范围仅
局限于调用者的函数调用点与整个被调用函数体中;
• 每个函数的每次调用都会被翻译,被调用函数的函数体部分的翻译会被复制一份副本,函数名也以添
加后缀_〈CALL_ID〉的形式加以区分;
• 同一函数再次被调用时,仅需对其中涉及调用的临时信道名进行替换.
转换时,对于函数调用逻辑之外的其他函数体语句保持不变.通过对程序静态执行下的函数调用序列中的
所有函数调用关系进行转换之后,便得到了一个协议 C 程序对应的 Pi 演算的形式化描述框架,主要剩余函数体
语句部分未进行抽象.在实验章节,我们通过 ProVerif 自动化证明了此函数抽象方案的正确性.
3.3.2 函数体语句抽象
对函数调用关系的抽象,实现了协议代码到 Pi 演算模型框架的转换,还需对模型中未转换的函数体语句部
分进行抽象后才能作为 ProVerif 工具的输入.这里分析的 C 语言函数体中的代码块,暂不考虑匿名函数等语法