论文部分内容阅读
混合布尔算术(Mixed Boolean-Arithmetic,MBA)混淆技术是一种语义保留的变换方法,它将一个简单的表达式转变为一个难于理解和分析的形式。更具体一点,这种混淆技术产生的表达式包含混合使用的算术运算操作符(如,加法和乘法操作)和布尔运算操作符(如,与、或、非等操作)的表达式。MBA混淆技术即使在面对静态或动态反混淆方法时,包括先进的SMT求解器分析技术,依然能够有效隐藏程序中的数据和算法流程。然而,专用的MBA反混淆技术依然处于不断发展中。目前先进的MBA化简方案,如模式匹配,bit-blasting,程序综合,和深度学习等方法,依然存在着各种不足,如面临着严重的性能问题,为特定MBA模式所设计,或产生过多的错误化简结果。与现有的线性MBA化简方法相比,本文深入线性MBA混淆机制的设计中,抽象出其核心机制为:基于真值表的线性方程组求解系统。之后,本文提出signature-vector的概念,signature-vector能够表示线性MBA表达式的完整语义。基于signature-vector,本文发展出一种高效的线性MBA表达式化简办法。首先,基于线性MBA表达式的真值表来计算signature-vector。对于任意给定的signature-vector,通过计算位运算表达式的线性组合来重新构建一个简单的表达式。通过这种方式,针对任意的线性MBA表达式,该方法可以将其化简为一个等价的简单形式。我们已经实现该化简方法为一个开源工具MBA-Blast,并且在一个具有10,000条线性MBA表达式的数据集上进行测试。本研究也在真实的二进制反混淆场景下测试MBA-Blast,实验结果表明MBA-Blast能够帮助软件分析人员理解被混淆后的恶意软件的行为。与已有的工作相比,MBA-Blast是最高效和通用的线性MBA表达式反混淆技术;MBA-Blast具有坚实的理论基础,化简线性MBA表达式成功率高且代价可以忽略。MBA表达式的反混淆研究对MBA混淆技术提出潜在的挑战,因此现有的MBA混淆技术必须被加强以克服这些出现的挑战。本文首先回顾已有的MBA混淆技术,并且阐明现有的MBA混淆技术主要基于线性MBA表达式—MBA表达式的一个简单子集。这种现况留下一个未被探索的研究方向,也就是更复杂的非线性MBA表达式。因此,本文提出一种新的混淆方法来展示非线性MBA混淆技术的潜力。非线性MBA表达式是通过组合或变换具有坚实理论基础的线性MBA表达式而得到。与现有的MBA混淆技术相比,本研究能够产生更复杂的非线性MBA表达式。我们已经实现该方法为一个开源工具,命名为MBA-Obfuscator,并利用该工具产生一个大规模的数据集。相关实验结果表明,MBA-Obfuscator是一个具有坚实理论基础的实用混淆技术。非线性MBA表达式的出现,提出一个全新的挑战:如何化简MBA表达式。本文首先探索SMT求解器处理不同种类MBA表达式的能力:线性,多项式,和非多项式MBA表达式。我们观察到SMT求解器只能处理简单的线性MBA表达式,在面对复杂线性MBA表达式和非线性MBA表达式时面临严重的性能瓶颈问题。为了提高SMT求解器的处理能力,本文提出一种语义保留的方法来化简MBA表达式。首先,我们将任意一个位运算表达式转换为一种统一的形式—一个简单的MBA表达式。之后,我们应用基本的数学规则来合并同类项,并产生一个具体的化简结果。实验结果表明,本研究提出的化简方法能够极大提高SMT求解器处理MBA表达式的效率。本文提出的方法已经能够成功化简多项式MBA表达式,最后一个挑战便是如何化简非多项式MBA表达式。本文提出一种基于神经网络的化简方法,神经网络模型的输入为非多项式MBA表达式,输出为一个简单的表达式。首先,本文构建相应的神经网络模型,并用它们来学习非多项式MBA表达式的语法和语义。之后,本文生成一个大型数据集,它包含一百万个非多项式MBA恒等式,并用该数据集训练神经网络模型。最后,利用训练好的神经网络模型来化简非多项式MBA表达式。实验结果表明,同已有的化简方法相比,本研究提出的方法在大幅提高化简正确率的同时也能大幅降低化简时间。本文以MBA表达式为研究对象,提出不同的方法来产生非线性MBA表达式,并且提出一系列方法来化简不同种类的MBA表达式。希望本文工作能够对MBA表达式的混淆和化简提供新的思路和见解。