基于信息流的整数漏洞插装和验证

为降低整数漏洞插装验证的运行开销,提出基于信息流的整数漏洞插装方法.从限定分析对象范围的角度出发,将分析对象约减为污染信息流路径上的所有危险整数操作,以降低静态插装密度.在GCC平台上,实现了原型系统DRIVER(detect and run-time check integer-based vulnerabilities with information flow).实验结果表明,该方法具有精度高、开销低、定位精确等优点.

整数漏洞研究:安全模型、检测方法和实例

C/C++语言中整型的有限表示范围、不同符号或长度间的类型转换导致了整数漏洞的发生,包括整数上溢、整数下溢、符号错误和截断错误.攻击者常常间接利用整数漏洞实施诸如恶意代码执行、拒绝服务等攻击行为.综述了整数漏洞的研究进展,从缺陷发生后行为的角度提出了新的整数漏洞安全模型,总结了判定整数漏洞的充分条件.从漏洞判定规则对充分条件覆盖的角度对现有检测方法进行比较和分析.通过实例分析,讨论了整数漏洞在现实中的特征分布.最后指出了整数漏洞研究中存在的挑战和有待进一步研究的问题.

基于静态插装和约束求解的整数漏洞检测

以C源码为研究对象,提出了一种基于静态插装和约束求解的整数漏洞检测方法.首先在C源码中可能的整数漏洞点前面插装检测代码,同时定位可能导致整数漏洞的输入源,并将其标记为符号变量.之后将静态插装后的源码编译成可执行代码,并进行(符号和具体执行的)混合执行.在动态执行的过程中,通过对插装代码对应的符号约束进行求解,可以检测整数漏洞是否存在,以及获得当整数漏洞存在时符号变量相应的具体取值.进一步地,通过对从程序入口点到整数漏洞点所经过路径上的所有条件跳转约束进行求解,获得引导程序到达整数漏洞点时符号变量相应的具体取值.结合两者可以辅助生成触发漏洞的输入用例.基于CVE(通用漏洞披露)通告的实验表明本系统能够成功检测到相应漏洞.

二进制代码中整数型漏洞挖掘和利用技术

通过对以往二进制挖掘模型的研究,提出了一种新的二进制代码整数型漏洞挖掘方法模型,该模型综合运用了Fuzzing、逆向工程和符号执行等相关技术。首先利用逆向分析锁定与整数漏洞相关的代码部分,获得数据相关类型操作,检测敏感函数,构建函数结构流图,确定整数漏洞相关的代码部分;其次通过对汇编代码的符号执行,获得代码的输入输出关系和路径约束条件,调整Fuzzing的输入,这些可以大大提高Fuzzing的路径覆盖和效率。本模型使得二进制整数型漏洞的挖掘准确性得到了一定程度的提高。

基于标志位差异分析的整数溢出漏洞溢出点定位方法

近几年,整数溢出漏洞数量居高不下,危害性较大。目前,漏洞分析定位的方法仅在补丁自动生成或漏洞触发样本文件自动生成中有所涉及,且这些方法大多利用缓冲区溢出会覆盖其邻接内存数据的特点来进行定位分析,而整数溢出漏洞不具有直接覆盖重要数据的特点,所以现有的方法不能对其进行有效的定位分析。现阶段对整数溢出漏洞的分析大多依靠人工完成,效率较低。为了提高分析人员的工作效率,提出了一种结合动态污点分析技术进行EFLAGS标志位信息比对的方法,来将溢出点锁定在少量的地址中。在此基础上实现了一套整数溢出漏洞溢出点定位系统,并对提出的方法进行了验证。

IFuzz:对整数类型漏洞的灰盒模糊测试

现有的基于覆盖率反馈的灰盒模糊测试技术在漏洞挖掘实践当中获得了巨大的成功。然而,以AFL为代表的灰盒模糊测试器在发现整数类型漏洞方面仍有不足。这类模糊测试器使用简单的整数替换方法,没有解决在哪里变异和如何变异的问题。为了解决这些问题,本文提出了解决方案IFuzz。该方案采用自主设计的通用模糊测试hook框架来获取额外的轻量级运行时信息,进而进行逐字节扰动变异并运用这些信息以推断整数位置,最后通过给字节分配不同的能量来进行整数变异。实验评估结果表明,该方法能有效提高整数类型漏洞的模糊测试效率。

一种代币智能合约的形式化建模与验证方法

针对代币智能合约的安全问题,提出一种基于代币智能合约整数溢出漏洞的形式化建模与验证方法。分析现有The DAO和BEC等漏洞攻击事件,定义代币智能合约的安全属性,通过引入全局变量和数值比较等约束条件对代币智能合约的建模语言进行扩展,使其支持智能合约各类语句的形式化表示。借鉴数学归纳法的思想,优化SmartVerif模型验证过程,避免状态空间的无限遍历。实验结果表明,该方法能成功找出代币智能合约的整数溢出漏洞,并且具有较强的通用性。