2021, Vol. 32
2. 网络密码技术河南省重点实验室, 河南 郑州 450002
2. Henan Key Laboratory of Network Cryptography Technology, Zhengzhou 450002, China
形式化方法在对安全协议的分析中取得了显著成果, 并促进了很多协议草案的设计完善.但理论上的安全并不能保证实际部署中协议的安全属性满足, 经过形式化验证安全的协议, 在转换成具体实现时可能依然存在安全问题.协议实现中的安全问题既有一般性的低级别错误如缓冲区溢出, 也包含了语义实现中的逻辑错误: 第1类安全问题可以借助通用的代码审计技术等来弥补; 第2类语义逻辑错误问题更为隐蔽, 难以借助现有的软件测试技术如Fuzzing来发掘.
为了发现协议实现中的语义逻辑错误, 研究人员提出了对协议实现代码同样进行形式化验证的思路[1].程序设计语言本身在语法语义上复杂表达能力丰富, 难以直接在其上进行形式化的验证推演, 因而对协议代码的形式化分析都是遵循先抽象再验证的工作思路开展.通常做法是: 将协议源码抽象为某种形式化语言模型, 再基于该抽象模型进行协议安全属性的形式化验证.不同语言实现的协议在分析时存在较大差异性, 多数文献都是针对协议的某种具体的编程语言实现提出相应的形式化方法[2-4].近些年, 协议代码形式化验证方面的研究工作目前以对JavaScript[5, 6], Python[6]和Java[7]这类高级语言编写的协议代码分析为主, 而针对较偏底层的C语言协议实现形式化工作相对较少, 且在实用性上存在一定限制, 例如不支持C的指针语法[1, 8]、对条件分支和函数调用无法自动化抽象[9, 10]等.而安全协议开发中C语言的所占比重, 对协议C代码的形式化验证工作更具现实安全需求.
本文的研究对象是C语言实现的协议代码的逻辑语义检测, 忽略一般的代码级问题如内存类bug, 旨在设计并实现对协议C源码自动地形式化验证方法.根据C语言面向过程的编程特点, 按照函数调用-函数体语句-表达式的顺序将协议C程序逐步抽象为Pi演算模型, 利用成熟的协议自动验证工具ProVerif[11]对代码的抽象模型进行验证.ProVerif是一个在Dolev-Yao敌手模型下自动化分析协议安全属性的工具, 能够自动化证明可达性属性和观察等价性.这些能力允许对机密性和认证属性进行分析, 此外, 还可以用于刻画诸如匿名性、可追溯性等, 并且可以在无限数量的会话和无限的消息空间下进行推理.该工具还能够进行攻击路径重构.这些针对协议的成熟的解决方案是一般的代码验证工作所不具备的.根据抽象方案实现了自动化抽象工具C2P(https://github.com/85lx/C2P), 并将其开源.在对协议实现代码中的密码与通信原语及相关标准库函数处理时, 采用当前这一方向的通用处理方式, 将其视为黑盒, 不探索这些库函数的细节; 提出了获取静态函数调用关系序列的算法, 并在静态执行下函数调用关系序列基础上, 给出了函数调用关系在Pi演算逻辑语言中的表达方法; 提出了基于函数上下文的表达式归约算法, 对C语言中涉及到的基本代数和逻辑运算进行规约, 降低了抽象模型的逻辑复杂度.
本文的主要贡献如下:
(1) 提出一种对协议实现的C源码形式化验证的方法.该方法可以将协议C代码转换为Pi演算抽象模型, 进一步在Dolve-Yao敌手模型下验证相关的安全属性是否满足;
(2) 提出了函数调用时序图(function call sequence graph, 简称FCSG)结构和静态执行下函数调用序列获取算法, 并基于静态执行下的函数调用序列, 给出了C程序中函数调用在Pi演算模型中的抽象方法, 给出了其合理性证明;
(3) 依据方案实现了协议C代码的自动化抽象工具C2P并将其开源, 通过Kerberos协议代码, 验证分析说明了方法和工具的有效性.
本文第1节介绍相关工作.第2节简介协议源码验证及Pi演算基础知识.第3节阐述协议C源码到Pi演算模型的抽象方法.第4节介绍C2P工具实现和方法合理性证明以及代码实例上的实验.最后, 第5节总结全文.
1 相关工作对于协议代码的形式化验证, 与之前的协议标准的形式化分析工作有着很大区别.程序设计语言本身在语法语义上复杂表达能力丰富, 难以直接在其上进行形式化的验证推演, 因而对现有协议代码的形式化分析都是遵循的先抽象再验证的逻辑思路开展.文献[11]是对协议实现安全性分析最早的工作之一, 通过程序开发人员在代码中的注释建立信任断言模型, 将协议的C语言程序抽象成霍恩子句, 基于霍恩子句的逻辑理论, 在信任断言模型中进行协议机密性验证.文献[8]是第1个将软件模型检测与标准协议安全模型相结合、自动分析C语言中实现协议中的认证性和机密性的框架.文章中用谓词抽象技术将具体的协议程序翻译成更为抽象的ASPIER模型, 并采用ASPIER分析并发现了SSL握手协议的OpenSSL0.9.6c源代码中存在的“版本回滚”漏洞.不足之处在于: 该项工作没有很好地处理C语言的主要特性是指针和内存操作这两大特性, 因而需要大量人工参与, 实用性受限; 另一方面的不足是, 文中采用自定义的ASPIER抽象模型相对较复杂, 研究人员得熟练掌握ASPIER抽象模型才可以在此基础上开展分析工作, 因而通用性也有一定损失.类似的工作有文献[13-15], 都是将现有的协议代码抽象成自定义的模型再进行逻辑推演.
文献[9]的工作弥补了这一不足, 将安全协议的C语言代码转换成为Pi演算模型.Pi演算是一种通用而语法简洁的协议模型描述语言, 且可以直接作为协议自动验证工具ProVerif的输入语言模型, 从而在符号模型下对协议C代码进行自动化的形式化验证分析.相关团队在文献[10]中将该项工作拓展到计算模型, 利用CryptoVerif工具进行计算模型下的协议形式化验证.这一工作的不足之处在于: 仅支持单一执行路径, 不支持函数调用和条件分支、循环迭代等, 在一定程度上削弱了验证框架的适用范畴.但该工作所体现的将协议的C语言代码抽象成已经存在且较成熟的Pi演算逻辑模型的研究思路, 既方便后续工作拓展, 也有利于基于已有形式化自动化验证工具进行协议代码的安全属性分析.与之类似的工作还有文献[16], 其采用类似的思路将程序设计语言F#所编写的协议代码转换为Pi演算和Blanchet演算, 然后借助ProVerif工具进行自动化的形式化验证.还有一部分工作将这种思路应用到Java语言编写的协议代码形式化验证中, 如文献[7], 通过将安全协议的Java代码抽象成Blanchet演算, 从而利用CryptoVerif工具对抽象后的模型进行自动化的形式化验证分析.文献[17, 18]也是采用先抽象再验证的思路, 与其他工作的不同之处在于, 这些工作应用了Petri网理论模型: 首先将安全协议程序转换成对应的Petri网模型, 然后借助Petri网理论来分析协议的通信行为是否满足相关的安全属性.此项工作的意义在于为协议实现的形式化分析研究引进了新的工具Petri网理论, 但同时仍然有很多待研究解决的问题.
本文沿用了先模型抽象再验证的研究思路.与现有工作相比, 直接在源码层面做抽象, 支持更多的C语法抽象如函数调用, 适用于代码规模较大的协议实现分析.另一方面, 现有工作的共性不足之处在于工作缺乏延续性, 或仅限于团队内部延续, 这很大程度上源于该领域在复现他人工作方面并不平凡.为此, 本文将C2P工具的代码开源, 希望对这一现状有所改善.
2 相关基础 2.1 协议源码验证为理解协议协议源码验证和传统的源码安全测试工作的不同, 在此给出协议源码的验证的定义.
定义2.1(协议源码验证). 给定一个协议Pro的规范S(Pro)和由程序设计语言L编码的协议实现P(Pro)[L], 验证S(Pro)中可满足的安全属性φ在P(Pro)[L]中也是可满足的过程:
| $ S\left( {Pro} \right)╞\varphi \Rightarrow P\left( {Pro} \right)\left[ L \right]╞\varphi $ |
称为对协议Pro的L源码的安全属性验证, 简称为协议源码验证.
根据定义2.1, 协议源码验证工作的对象是某种具体编程语言实现的安全协议源码, 如本文的研究对象即C语言实现的协议源码, 即P(Pro)[C-Language].研究的目标是安全属性是否满足, 而非一般的代码级问题.
2.2 Pi演算语法Pi演算(Pi calculus)[12]是一个用于并行系统之间通信行为建模的理论, 其模型简洁且具有强大的表达能力.著名的安全协议验证工具ProVerif的输入语言便是扩展的Pi演算.本节对这种扩展的Pi演算语言进行简单介绍, 为便于描述, 后文提到的Pi演算特指ProVerif的输入模型.
Pi演算语法中的项(term)是由名(names)、变量(variables)和构造/析构函数(constructor/destructor)组成的.形式化定义如下:
| $ M, N∷ = a, b, c, \ldots \left| {x, y, z, \ldots } \right|h\left( {{M_1}, \ldots , {M_k}} \right)\left| {M = N} \right|M < > N\left| {M\& \& N} \right|not\left( M \right), $ |
其中, a, b, c∈C; x, y, z∈V; h∈∑为names的集合, V为变量集合, ∑为函数符号集合; =和 < > 表示等式和不等式关系, & & , ‖和not对应与或非逻辑关系; 项可以用于描述安全协议通信中的消息, 函数可以用于对加密原语的描述.
在Pi演算中, 进程(process)是用于描述一系列协议行为.Pi演算中, 进程的定义见表 1.其中: 空进程表示无实义操作; 并发进程为两个进程同时运行; 创建新名是为进程P创建私有名; 条件语句为比较项M和N, 相等则执行进程P, 否则执行进程Q; 赋值语句为变量x赋值为项M, 赋值成功执行进程P, 失败执行进程Q; 接收消息和发送消息操作模拟协议通信中的发送和接收消息行为.
|
Table 1 Process grammar in Pi calculus 表 1 Pi演算进程语法 |
一个协议实体的通信行为可以用这些语法进行描述.例如对称加解密操作的表示中, 加密过程看作不解义的构造函数(constructor): enc(x, y)解密操作视为析构函数(destructor), 加解密之间的联系用等式理论代替:
| $ dec\left( {enc\left( {x, y} \right), y} \right) = x. $ |
类似地, 公钥加密算法的表示分别对应如下:
| $ enc\left( {x, pk\left( y \right)} \right); $ |
| $ dec\left( {enc\left( {x, pk\left( y \right)} \right), y} \right) = x, $ |
其中, pk(y)表示私钥y对应的公钥, 同样为不解译函数.采用类似的等式理论可以表示私钥签名等操作.
ProVerif所支持的Pi演算的主要语法描述如上, 更多细节可参考相关文档[11].
3 从协议C代码提取Pi演算模型对安全协议代码进行形式化分析的基本思路是: 将协议C源代码转换成为Pi演算模型, 之后借助协议自动化分析工具ProVerif对抽象后的Pi模型进行形式化验证分析.我们依据C语言面向过程的这种以函数调用组织起来的结构特点, 依次从C程序中的函数调用、函数体语句、语句中的表达式这3个不同的层次来对安全协议C程序代码来实施形式化抽象.图 1给出了协议C源码验证的整体框架.
|
Fig. 1 Overall security verification framework of C protocol code 图 1 协议C源码的安全验证架构 |
整个验证框架分为4个步骤.
(1) 对待分析的目标协议源码进行预处理, 预处理任务主要包括基本的预编译处理, 如消除宏相关指令、头文件处理以及对密码原语操作相关函数、通信模块相关函数以及标准库相关函数的重写;
(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 常见编译预处理指令 |
对一个函数的黑盒化处理是指不进入该函数的函数体中去解析该函数的执行逻辑是否正确, 而是默认该函数的实现逻辑和它所声明的执行功能一样.密码学是安全协议实现安全属性的重要基石, 在安全协议对应的代码中也存在很多密码原语相关的操作函数.密码学上一般通过多轮混淆(confusion)、扩散(diffusion)和移位(shift)等操作来抵抗敌手的分析.密码原语函数的相关代码中同样存在这些逻辑, 对这些逻辑的分析会增加协议源码的分析难度.在基于Dolve-Yao模型的协议规范形式化分析通常采用完美密码假设来处理这一问题, 在对代码的形式化分析中同样可以采用这一思路.将协议代码中密码原语操作函数按照Pi演算逻辑中的项重写和等式规则直接替换.同样的, 对于协议代码中的通信模块相关函数如socket编程接口, 也不去探索这些函数实现细节, 用逻辑语言中的消息发送和接收逻辑替代.这一处理可以扩大到标准库或者第三方库中的函数, 甚至是协议源码中任意可信任的函数实现.协议代码的预处理交由用户手工标识配合程序半自动化完成, 因为C2P工具的使用对象定位为协议代码开发者或者对代码熟悉的专业人员, 而非一般用户.
3.2 获取函数静态执行序列函数是对程序代码逻辑模块化的编程方式, 采用函数组织程序有助于将复杂的程序代码结构分割成代码块集合.一个C语言程序的结构可以表示为一个函数执行序列.
考虑到C程序的面向过程的函数结构, 我们从程序的函数静态执行序列入手, 对程序从结构上进行解析.为了得到函数静态执行序列, 我们设计了能全面反映协议C程序代码的函数调用关系的数据结构函数调用时序图, 用缩写FCSG表示.
FCSG是一个四元组结构G=(F, R, S, f0), 其中,
● F是一个符号集合;
● R是定义在F上的二元关系: R={〈fi, fj〉k|fi∈F, fj∈F, k∈Z+}, 下标k表示对集合中相同的fi和fj构成的关系的区分.且∀k≥2, 若〈fi, fj〉k∈R, 则〈fi, fj〉k-1∈R.当k=1时, 简记为r=〈fi, fj〉;
● S是集合R到正整数集Z+的映射, 满足:
➢ ∀〈fi, fj〉k∈R, 有S(〈fi, fj〉k)=s, s≥k;
➢ ∀〈fi, fj〉k∈R, ∀〈fi, fj'〉k'∈R, 若〈fi, fj'〉k'≠〈fi, fj〉k, 则S(〈fi, fj'〉k')≠S(〈fi, fj〉k);
➢ ∀S(〈fi, fj〉k)=s, 若s > 1, 则Ǝ〈fi, fj'〉k'∈R, S(〈fi, fj'〉k')=s-1;
● f0∈F, 且
符号集合F对应一个C程序P中的所有函数集合.考虑C语言中不支持函数重载, 故可用函数名表示程序中的函数.集合R用来刻画程序P中的函数调用关系, ∀fi∈F, fj∈F, 若程序P中的函数fi的定义中存在函数fj的调用语句, 且在函数中的调用是第k次出现, 则有〈fi, fj〉k∈R; 若该次调用是fi函数体中出现的第s个函数调用语句, 则有S(〈fi, fj〉k)=s.程序P的入口函数记为f0, 显然, 一个良好程序的入口函数不会在其他函数中被调用.在关系集合R中, k是对相同的函数调用关系的编号, 用以区分这些相同函数调用.
在协议代码FCSG结构的基础上, 定义获取函数调用静态执行序列(static execution of call sequence, 简称SECS)算法, 将其命名为FCSG-SECS算法, 算法描述如下:
算法1. 函数调用静态执行序列获取算法FCSG-SECS(G).
输入: G=(F, R, S, f0);
输出: 函数调用静态执行序列SECS.
1. SECS=[·];
2. If G.F=Ø then
3. Return [·];
4. EndIf
5. R0={〈G.f0, f'〉k|〈G.f0, f'〉k∈G.R};
6. 将R0按照G.S的映射值升序排序;
7. Foreach 〈f0, f'〉k∈R0 do
8. SECS.append(〈f0, f'〉k);
9. G'=(F/f0, R/〈f0, f'〉k, S/(〈f0, f'〉k→s'), f');
10. SECS.append(FCSG-SECS(G'));
11. EndFor
12. Return SECS
函数调用时序图中蕴含了静态模拟执行代码的函数调用顺序.从入口函数出发, 对协议代码对应的FCSG按出边的标号属性顺序(升序), 遍历所有函数调用关系, 便可以得到程序代码的函数调用执行序列.我们用图 2中的示例代码来具体说明.图 2是一段示例代码和其对应的FCSG图.
|
Fig. 2 Example for function calls and FCSG 图 2 函数调用及FCSG示例 |
示例代码对应的FCSG表示为G=(F, R, S, f0), 其中,
● 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};
● f0=main.
通过FCSG-SECS算法可得到程序代码在静态执行下的函数访问序列:
| $ \left[ {\left\langle {main, bar} \right\rangle , \left\langle {bar, foo} \right\rangle , \left\langle {main, foo} \right\rangle , \left\langle {main, bar} \right\rangle , \left\langle {bar, foo} \right\rangle } \right]. $ |
这与代码在静态执行过程中的函数调用顺序是一致的(实际执行中的函数调用序列可能会因为条件判断语句等因素产生偏差).为了简化分析, 还可以根据人工经验, 将一些无用的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所示.
|
Fig. 3 Function call simulation 图 3 函数调用模拟 |
(1) 第CALL_ID=n次函数调用关系〈A, B〉看作相应的A进程和B进程并行执行;
(2) 调用者A在信道C_n上发送空消息, 并在相应的S_n信道上等待接收返回值信息, 然后继续执行剩余代码逻辑;
(3) 被调用者B在信道C_n上监听, 有空消息到来时执行B函数体逻辑, 最后将返回值在信道S_n上发出, 然后执行结束.
第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语言函数体中的代码块, 暂不考虑匿名函数等语法现象, 因为它们的处理方式和正常函数的处理类似.在对语句进行抽象处理时, 将表达式Expr视为原子项, 对于表达式的处理将在第3.3.3节阐述.首先介绍C中的变量类型处理, 再介绍各种类型语句的抽象方法.
A. 变量类型转换
方案将C语言中的变量基本类型简化为两种基本类型: 数字型num和字符串类型bitstring.其中, num类型包含了C语言中常见的int, float, long, double等.对于字符及数组等抽象为bitstring类型.为了支持条件分支语句逻辑, 还应该引入对bool类型的抽象.Pi演算模型中, 内建类型中支持bool类型以及与之相伴随的true和false两个bool型常量, 这里直接将C语言中的bool类型及true, false与之对应抽象即可.
在此基础上增加指针类型ptr, 并通过引入PTR构建操作和对应的析构操作VAR来实现对C语言中基本类型指针的支持.
● PTR_num(a: num): ptr获取num类型变量a的内存地址;
● PTR_bitstring(s: bitstring): ptr获取bitstring类型变量s的内存地址;
● VAR_num(p: ptr): num获取地址p处的值, 返回类型为num;
● VAR_bitstring(p: ptr): bitstring获取地址p处的值, 返回类型为bitstring.
用Pi演算中的重写规则来将这两种操作进行关联.
type num.
type bitstring.
type ptr.
fun PTR_num(num): ptr.
reduc forall a: num, p: ptr; VAR_num(PTR_(ptr))=a.
fun PTR_bitstring(bitstring): ptr.
reduc forall s: bitstring, p: ptr; VAR_bitstring(PTR_bitstring(ptr))=p.
本方案暂不支持函数指针以及指针的运算操作, 当协议代码中涉及到这些语法时, 自动化抽象程序仅将这些语法部分标注出来, 留作人工处理.
B. 语句抽象
对代码块的处理, 我们以C语言中的语句(statement)作为基本的翻译单元.考虑协议的C代码中常见的语句类型, 主要有变量声明/定义语句、表达式语句、条件分支语句、函数调用语句、返回语句、循环结构语句等.其中, 函数调用语句和返回语句在上一小节中已经进行了抽象处理, 本方案暂不支持C程序中的循环结构语句, 涉及到循环结构的部分需要依赖人工经验进行手工转换(见表 3).
|
|
Table 3 Common statements type in C language 表 3 C中常见语句类型 |
下面逐一给出这些语句到Pi演算逻辑的转换方法.
● VarDeclStatement
变量声明和定义语句在抽象转换时并无特殊区别, 因为C2P并不关注协议C代码的语法正确性.这是编译工具所做的事情.
全局变量与局部变量定义语句在具体的抽象细节上稍有不同, 具体抽象规则描述如下:
| $ VarDeclstatement:: = \left\langle {Ctype} \right\rangle \left\langle {varname} \right\rangle \left[ {Initial} \right], $ |
其中,
| $ Ctype:: = int|float|char| \ldots . $ |
全局变量的抽象方式:
| $ free\left\langle {varname} \right\rangle :\left\langle {type} \right\rangle . $ |
局部变量的抽象方式:
| $ new\left\langle {varname} \right\rangle :\left\langle {type} \right\rangle , $ |
其中, type是依照前文所述的变量类型转换方法进行替换:
| $ \left\langle {type} \right\rangle = abs(\left\langle {Ctype} \right\rangle ). $ |
对于含有初始化部分〈Initial〉的变量定义语句, 采用和ExprStatement中的赋值表达式相同抽象方法处理.
● ExprStatement
一个表达式作为独立的C语言语句, 表达式语句是C语言中最基础的语句类型.严格意义上, 函数调用语句也属于表达式语句的一种, 但这里的ExprStatement不包含函数调用的表达式语句, 因为函数调用表达式语句的抽象过程中已被处理过.在C语言中的表达式语句的作用是对表达式进行求值, 然后丢弃求值结果, 像a+3.这种表达式作为单独语句是没有意义的, 有用的是执行表达式之后会对参与的变量(一个或多个)的值进行修改的表达式语句, 最常见是赋值语句和自增减语句.自增减其本质也是一种赋值操作, 若作为单独语句, 是可以和赋值语句等价转换.
赋值语句的语法如下:
| $ \left\langle {Lvarname} \right\rangle = \left\langle {subExpr} \right\rangle . $ |
对应的Pi演算抽象:
| $ {\rm{let}}\left\langle {Lvarname} \right\rangle = abs(\left\langle {subExpr} \right\rangle )\;{\rm{in}} $ |
对于〈subExpr〉抽象abs(〈subExpr〉), 我们会进行基于表达式上下文化简, 具体参考第3.3.3节.
● IfStatement/SwitchStatement
C语言语法中存在两类条件分支语句: If-Else和Switch-Case.Switch case结构可以转化为If-Else结构, 所以我们重点讨论IfStatement.SwitchStatement的抽象可以先将其转换为IfStatement, 再对其进行抽象转换为Pi演算模型.Pi演算中支持if-else条件判断, 因此仅需要将相应的部分条件表达式condition, if分支代码块If_block, else分支代码块Else_block等, 利用本方案中的对应类型进行抽象即可.对于没有else的分支, 自动补充else部分抽象: else 0.具体的抽象规则描述如图 5所示, abs(〈c_code〉)表示对〈c_code〉进行抽象后的结果.
|
Fig. 5 IfStatement abstraction 图 5 条件语句抽象 |
● ForStatement/WhileStatement
考虑到循环控制结构在Pi演算抽象模型中无合适的模型对应, 因此和现有的一些方案类似, 本文方案对循环结构无确定的自动化抽象转换规则.在自动化分析阶段采用保留循环, 仅对其中代码块中的子表达式和子语句进行抽象, 最后采用人工分析进行抽象转换, 这其中或引入执行语义的损失.
● NullStatement
空语句不执行任何操作但也符合C语言的语法规范, 我们将其等价转换为Pi演算中的空过程0.
3.3.3 表达式约简表达式是C语言语句中的核心组件, 对表达式的抽象逻辑处于整个抽象方案的最底层环节.变量和常量是最基本的表达式: 对于变量, 我们直接在抽象逻辑中将其作为相应抽象类型的变量; 常量将其视为不解义符号.对于由变量和代数运算符等构成的表达式, 先按照代数运算规则对其进行相应的计算约简, 再将约简后的表达式中的代数运算符抽象为Pi演算中的构建操作(constructor).
所谓约简, 即在当前函数中, 对表达式根据表达式的求值运算规则进行求值运算.
基于函数上下文关系的表达式约简算法见算法2.
算法2. 基于函数上下文关系的表达式约简算法.
输入: 单个函数定义中的表达式序列E;
输出: 约简后的表达式序列E'.
1. Context=[·];
2. E'=[·];
3. Foreach e in E then
4. Context.append{e};
5. e'=Simplify(Context, e); //据表达式上下文Context对表达式e进行化简
6. E'.append(e');
7. EndFor
8. Return E'
在一个函数的上下文中, 维护一个表达式的上下文内容, 根据表达式的上下文内容逐行对当前的表达式进行约简.最后, 函数中出现的局部变量都会被函数的参数变量、全局变量以及常量的代数表达式所替代.经过约简后的表达式, 基本的代数运算和逻辑运算已经完成, 无法根据当前信息进一步对表达式进行运算.无法进一步运算的表达式中的代数运算符视为透明操作, 用Pi演算中的Constructor来表示.以最基本的二元运算符+为例进行说明.对于二元操作符+, 抽象为constructor add: fun add(num, num): num.其他操作符类似, n元操作符抽象为n元函数即可.
基于函数表达式上下文关系代码约简示例如图 6.
|
Fig. 6 Sample code for expression reduction 图 6 表达式约简示例 |
4 C2P实现与评估 4.1 实现
本节介绍关于依照上文方案开发的C2P工具的实现.
C2P工具以人工预处理后的源码为输入, 将其依照上文所述的抽象方法转换为对应的Pi演算模型.在实现时, 我们利用C编译器前端开源项目clang及llvm库, 采用C++编程语言开发了C2P工具代码, 约1.5KLoC.
从协议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中转换模型求证以下两个命题成立.
|
Fig. 7 Case of call abstract 图 7 函数调用抽象逻辑正确性案例 |
命题4.1. 事件before_call, in_call, after_call严格依序发生:
| $ {{\rm{query}}\;inj - event\left( {in\_call} \right) = = > inj - event\left( {before\_call} \right);} $ |
| $ {{\rm{query}}\;inj - event\left( {after\_call} \right) = = > inj - event\left( {in\_call} \right).} $ |
命题4.2. 消息m的隐私性不因在临时信道s_id上传递而发生改变.若消息m是私有的, 则攻击者知识集中无法推导出消息m, 即query attacker(m)不成立.
这里采用ProVerif工具自动化证明命题4.1和命题4.2, 如图 8所示.
|
Fig. 8 Proof of correctness 图 8 正确性证明结果 |
由ProVerif对命题4.1和命题4.2的证明结果可知, 两个命题均成立.事实上, 借助ProVerif工具可以进一步证明: 在多个函数调用存在情况下, 命题依然成立.据此, 本文关于函数调用关系抽象的正确性得到证明, 即根据此方法得到的Pi演算抽象模型在执行逻辑上与协议C代码时一致的.
4.3 Kerberos协议代码分析本节以一份Kerberos协议的示例代码作为分析对象, 进一步说明本文方案对协议代码验证的有效性.该分析对象为github上下载的一份Kerberos协议的Demo代码.该份代码实现的协议流程如下.
(1) A→B: A, B, N1;
(2) S→A: IV2, E(N1, B, Kab, IV_ticket, ticket)Ka, IV2;
(3) A→B: A, B, IV_ticket, ticket, IV3, E(N2)Kab, IV3;
(4) B→A: IV4, E(N2, N3)Kab, IV4;
(5) A→B: IV5, E(N2, N3)Kab, IV5;
(6) B→A: IV6, E(data)Kab, IV6;
(7) A→B: IV7, E(data*)Kab, IV7.
其中, ticket=E(timestamp, A, Kab)Kb, Ka和Kb分别为实体A, B与可信第三方S共享的密钥, E为对称加密算法, IV为加密算法中用的初始向量.协议主要通信目标为实体A通过可信第三方S授权访问B上的资源data.
代码抽象的部分结果如图 9所示.
|
Fig. 9 Partial results of code abstraction 图 9 代码转换部分结果 |
抽象完成后, 通过人工添加协议安全属性及部分语法修正, 利用ProVerif工具自动化验证结果, 如图 10所示.
|
Fig. 10 An attack path of Kerberos code 图 10 Kerberos代码认证性攻击路径 |
通过转换后的分析表明: 代码中存在一条攻击路径, 在认证性证明时, 单射一致性被打破, 参见图 10.代码实现逻辑中, 在第5步消息接收时, 并未对IV5与IV4进行比较, 即验证IV5值的新鲜性, 导致攻击者可以在不拥有任何密钥的情况下, 仅利用截获消息来构造攻击路径, 从而导致B对A认证并不满足单射一致性, 协议的认证性被破坏.若可信第三方S在局部时间内为A和B生成的密钥Kab不变, 攻击者便可以成功构造攻击路径.
表 4列出了C2P方法与相关文献工作的对比情况.文献[9, 10]在函数调用语法处理上均需要人工将所有函数调用改写为inline模式, 再利用预编译程序处理inline.本文C2P方法可以直接支持函数调用语法的自动化处理.此外, 文献[9, 10]仅支持单一执行路径, 不支持条件分支语法; 而C2P方法给出了条件分支的抽象方法.在支持安全属性验证方面, C2P与文献[9]都采用了Pi演算模型, 可以支持符号模型的安全属性验证; 而文献[10]采用Blanchet演算, 支持计算模型的安全属性验证.符号模型基于完美密码假设理论, 即认为密码学相关设计完美, 攻击者不具备特殊密码学能力; 计算模型则在概率条件下考虑攻击者的破密能力.一般认为: 计算模型复杂度高, 但更符合实际安全.因此, 把本文方案迁移到计算模型, 也是待拓展工作之一.
|
|
Table 4 Comparison of related work 表 4 相关工作对比 |
5 结语
本文基于Pi演算模型给出了一种对C语言开发的安全协议源码进行形式化验证的方法, 继承了以往工作先抽象再验证的工作思路以及密码学原语相关函数黑盒化的技巧, 并将之拓展到通信模块和可信标准库或第三方库; 通过定义FCSG及函数调用静态执行序列获取算法得到函数静态执行序列, 并在此基础上, 依照函数调用、函数体语句、表达式约简的顺序逐级对代码进行抽象转换成Pi演算模型, 借助ProVerif自动化验证协议安全属性; 最后, 利用ProVerif给出了相关抽象的逻辑正确性证明, 并通过Kerberos协议代码案例分析说明了方法的有效性; 依据方案实现了C2P工具并将之开源, 以弥补这一领域工作延续性不足的问题.
| [1] |
Goubault-Larrecq J, Parrennes F. Cryptographic protocol analysis on real C code. In: Cousot R, ed. Proc. of the Int'l Workshop on Verification, Model Checking, and Abstract Interpretation. Berlin: Springer-Verlag, 2005. 363-379.[doi: 10.1007/978-3-540-30579-8_24]
|
| [2] |
Avalle M, Pironti A, Sisto R. Formal verification of security protocol implementations: A survey. Formal Aspects of Computing, 2014, 26(1): 99-123.
[doi:10.1007/s00165-012-0269-9] |
| [3] |
Meng B, Lu JT, Wang DJ, He XD. Survey of security analysis of security protocol implementations. Journal of Shandong University (Natural Science), 2018, 53(1): 1-18(in Chinese with English abstract).
[doi:10.6040/j.issn.1671-9352.2.2017.067] |
| [4] |
Zhang HG, Wu FS, Wang HZ, Wang ZY. A survey: Security verification analysis of cryptographic protocols implementations on real code. Chinese Journal of Computers, 2018, 41(2): 288-308(in Chinese with English abstract).
[doi:10.11897/SP.J.1016.2018.00288] |
| [5] |
Kobeissi N. Formal verification for real-world cryptographic protocols and implementations[Ph.D. Thesis]. Paris: Ecole Normale Supérieure de Paris, 2018.
|
| [6] |
He X, Liu Q, Chen S, Huang C, Wang DJ, Meng B. Analyzing security protocol Web implementations based on model extraction with applied PI calculus. IEEE Access, 2020, 8: 26623-26636.
[doi:10.1109/ACCESS.2020.2971615] |
| [7] |
Li ZM, Meng B, Wang DJ, et al. Mechanized verification of cryptographic security of cryptographic security protocol implementation in JAVA through model extraction in the computational model. Journal of Software Engineering, 2015, 9(1): 1-32.
[doi:10.3923/jse.2015.1.32] |
| [8] |
Chaki S, Datta A. ASPIER: An automated framework for verifying security protocol implementations. In: Proc. of the 22nd IEEE Computer Security Foundations Symp. New York: IEEE, 2009. 172-185.[ doi:10.1109/CSF.2009.20]
|
| [9] |
Aizatulin M, Gordon AD, Jürjens J. Extracting and verifying cryptographic models from C protocol code by symbolic execution. In: Chen Y, ed. Proc. of the 18th ACM Conf. on Computer and Communications Security. New York: ACM, 2011. 331-340.[ doi:10.1145/2046707.2046745]
|
| [10] |
Aizatulin M, Gordon AD, Jürjens J. Computational verification of C protocol implementations by symbolic execution. In: Yu T, ed. Proc. of the 2012 ACM Conf. on Computer and Communications Security. New York: ACM, 2012. 712-723.[doi:10.1145/2382196.2382271]
|
| [11] |
Blanchet B. Modeling and verifying security protocols with the applied Pi calculus and ProVerif. Foundations and Trends® in Privacy and Security, 2016, 1(1-2): 1-135.
|
| [12] |
Milner R. Communicating and Mobile Systems: The Pi Calculus. London: Cambridge University Press, 1999.
http://www.ams.org/mathscinet-getitem?mr=1695885 |
| [13] |
Kiyomoto S, Ota H, Tanaka T. A security protocol compiler generating C source codes. In: Proc. of the 2008 Int'l Conf. on Information Security and Assurance (ISA 2008). Piscataway: IEEE, 2008. 20-25.
|
| [14] |
Backes M, Maffei M, Unruh D. Computationally sound verification of source code. In: Al-Shaer E, ed. Proc. of the 17th ACM Conf. on Computer and Communications Security. New York: ACM, 2010. 387-398.[ doi:10.1145/1866307.1866351]
|
| [15] |
Jürjens J. Automated security verification for crypto protocol implementations: Verifying the Jessie project. Electronic Notes in Theoretical Computer Science, 2009, 250(1): 123-136.
[doi:10.1016/j.entcs.2009.08.009] |
| [16] |
Bhargavan K, Fournet C, Gordon AD, Tse S. Verified interoperable implementations of security protocols. ACM Trans. on Programming Languages and Systems (TOPLAS), 2008, 31(1): 1-61.
[doi:10.1145/1452044.1452049] |
| [17] |
Tang WS, Gou ZL, Ahmadon MAB, Yamaguchi S. On verification of implementation of security specification with Petri nets' protocol inheritance. In: Proc. of the IEEE 5th Global Conf. on Consumer Electronics. Piscataway: IEEE, 2016. 1-4.[doi: 10.1109/GCCE.2016.7800491]
|
| [18] |
Ahmadon MAB, Yamaguchi S, Gupta BB. Petri net-based verification of security protocol implementation in software evolution. Int'l Journal of Embedded Systems, 2018, 10(6): 503-517.
[doi:10.1504/IJES.2016.10011276] |
| [3] |
孟博, 鲁金钿, 王德军, 何旭东. 安全协议实施安全性分析综述. 山东大学学报(理学版), 2018, 53(1): 1-18.
[doi:10.6040/j.issn.1671-9352.2.2017.067] |
| [4] |
张焕国, 吴福生, 王后珍, 王张宜. 密码协议代码执行的安全验证分析综述. 计算机学报, 2018, 41(2): 288-308.
[doi:10.11897/SP.J.1016.2018.00288] |