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

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

从协议 C 代码到 Pi 演算的转换工作本质是实现协议 C 代码的翻译,需要对目标代码的 C 语言进行语法分
析、词法分析、语义分析等传统编译前端工作,这些可以借助 lex 和 yacc 接口实现.C2P 工具采用了 clang 编译
器的 AST 访问接口,因而其对协议 C 代码的解析,直接建立在目标协议 C 代码的抽象语法树基础上.Clang AST
为开发者提供了强大的抽象语法树解析访问接口.简而言之,C2P 借助 Clang AST 接口对 C 代码的抽象语法树
进行前序遍历,并采用 Clang AST 的 Rewriter 类对源码进行抽象重写.
在处理协议代码之前,除采用编译器前端处理预编译宏指令外,需要手工标记协议代码中的密码学函数和
通信函数,C2P 工具在遍历 AST 的时候会自动跳过被标记的函数.当前,我们采用为这些函数的函数名添加固定
前缀来标记.这一步处理还可以改进为配置文件的形式,从预置文件中读取相应的函数名,并在遍历时跳过这些
函数.C2P 需要对预处理后的代码进行两次遍历:第 1 次遍历识别出目标协议代码中的所有的函数定义和函数
调用关系(除标记函数外),将其以链表结构存储,在第 1 次遍历之后,便得到了代码的 FCSG 图;第 2 次遍时在
FCSG 图上运行算法 1,获取函数静态执行序列,同时根据函数调用静态执行序列的顺序,完成函数调用关系抽
象、函数体语句抽象.具体地,对所有 FCSG 图中的函数体语句进行抽象重写,函数调用关系抽象需要处理函数
体定义、函数调用语句、函数返回语句等的抽象翻译;非函数调用的一般语句按照第 3.3.2 节中的抽象方案进
行抽象转换即可;在处理每个函数定义时,维护一个表达式上下文结构,按照算法 2 进行约简.
实现中的要点如下.
• 基于 Clang AST,在抽象语法树层面对 C 代码语法解析,而非从词法和语法分析做起.Clang AST 提供了
方便的操作接口,采用 Clang::Rewriter 类对源码进行转换,对该类作了少许修改,以满足需求;
• 在 Clang 的 CallGraph 抽取代码基础上,添加了函数调用关系图的时序属性,构成了函数调用时序图
FCSG 抽取逻辑.在此基础上添加了 FCSG-SECS 算法,获取函数调用静态执行序列,在执行 FCSG-
SECS 算法的同时,完成函数调用关系的抽象;
• 函数体语句抽象是继承了 Clang::VisitStmt 类,为不同类型语句转换重写方法;表达式约简中,在基于函
数上下文关系的表达式约简算法中借助了著名数学工具库 pari,对基础的代数运算和逻辑表达式进行
约简.
更具体的实现细节详见 C2P 项目源码.
4.2 合理性证明
在本节给出本文方法中关于函数调用关系抽象的合理性证明.
抽象正确性指在抽象后的执行逻辑与原 C 代码执行逻辑上是一致的,包含两个方面.
(1) 抽象后的模型执行顺序与原协议 C 代码执行顺序一致;
(2) 抽象后的模型不改变攻击者(attacker)的知识集.
第 1 点,为了说明抽象方案不改变原有的代码执行顺序;第 2 点旨在证明抽象方案不改变任何消息原有的
机密性,即抽象后的模型不改变攻击者(attacker)的知识集.即证明:对于任意消息 m,其隐私性不因抽象方案而改
变(任意消息 m 若是私有的,则转换后的 Pi 演算模型下无法推出攻击者的知识集中包含 m).在 Pi 演算逻辑中,
信息机密性的改变是由直接或间接的信道传递而导致的,抽象方案引入了新的信道 s_id 和 c_id.进一步将问题
简化为验证在 s_id 信道直接传递 m 的情况下,消息 m 的机密性不因在新添信道 s_id 中的传递而发生变化.即,
转换后的 Pi 演算模型中 query attacker(m)不成立.query attacker(m)是 Pi 演算中关于消息 m 机密性的求解表达
式,表示在 Dolev-Yao 敌手模型假设下,求解攻击者的知识集中是否能包含消息 m.
不失一般性,将问题简化为对图 7 中转换模型求证以下两个命题成立.
命题 4.1. 事件 before_call,in_call,after_call 严格依序发生:
query inj-event(in_call)==>inj-event(before_call);
query inj-event(after_call)==>inj-event(in_call).
命题 4.2. 消息 m 的隐私性不因在临时信道 s_id 上传递而发生改变.若消息 m 是私有的,则攻击者知识集中
无法推导出消息 m,即 query attacker(m)不成立.