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

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

[1]
为了发现协议实现中的语义逻辑错误,研究人员提出了对协议实现代码同样进行形式化验证的思路 .程
序设计语言本身在语法语义上复杂表达能力丰富,难以直接在其上进行形式化的验证推演,因而对协议代码的
形式化分析都是遵循先抽象再验证的工作思路开展.通常做法是:将协议源码抽象为某种形式化语言模型,再基
于该抽象模型进行协议安全属性的形式化验证.不同语言实现的协议在分析时存在较大差异性,多数文献都是
针对协议的某种具体的编程语言实现提出相应的形式化方法 [2−4] .近些年,协议代码形式化验证方面的研究工
[7]
[6]
作目前以对 JavaScript [5,6] ,Python 和 Java 这类高级语言编写的协议代码分析为主,而针对较偏底层的 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 抽象模型相对较复杂,研究人员得熟练掌握