在上文中，我们为读者介绍了污点源的定义等静态污点分析方面的知识，在本文中，我们将继续为读者演示如何处理来自多个污染源的SSA变量的约束等技巧。

（接上文）

对来自多个污染源的SSA变量的约束

在进行污染传播时，如果有任何源变量被污染，包括PHI函数，我们就将目标变量标记为污染变量。在第二阶段的过滤过程中，如果一个变量受到约束，我们会将约束应用于所有相关变量。但是，当派生变量（子变量）来自一个以上的独立污点源（父变量），并且只有一个父变量被验证，那么，子变量也被认为被验证过了。但这种做法是不可取的。考虑一下下面的例子：

假设x和y来自两个独立的污点源，而index是两者之和，因此，它是一个派生变量。当x被验证后，由于y没有被验证，所以，index仍然可能被污损——但是，之前的算法没有考虑到这一点。

为了解决这个问题，我考虑将每个派生的污点变量与实际的源变量联系起来，称为根变量，并维护每个根变量的def-use链副本。例如，变量index#3有两个根变量：x#0和y#0变量。对于每个根变量，都利用与变量index#3相关的污点信息来维护一份可达块的副本。当x#1变量被验证时，只有变量index#3的副本x#0被标记为不可达，而副本y#0仍被视为污染变量。我们可以通过变量的依赖图来表示这些关系。

使用依赖图确定SSA变量之间的关系

在变量依赖关系图中，函数中的任何污点变量都被表示为一个节点。当一个变量来自另一个变量时，就形成了一条从父变量（节点）到子变量（节点）的有向边。

为了建立变量之间的关系，使用get_ssa_var_definition()访问所有污点变量的定义位置（definition site）。当MLIL表达式中的任何一个源变量被污染时，在图中创建一个边连接。由于在MLIL_LOAD_SSA操作中被污染的变量没有父节点或传入的边，因此，它们就成为了根节点。

这样的依赖关系图通常存在许多弱连接的组件，因为加载自受污染的内存区的每一段内存都将被分配给一个新的变量，对应于图中一个新节点。简单地说，每个内存加载都会和它的派生变量一起创建一个子图。当变量派生自多个根节点时，相应的子图可能会与另一个子图连接。下面是一个来自函数Dbtux::execTUX_ADD_ATTRREQ()的示例依赖关系图：

另一个需要注意的属性是，依赖关系图不一定是有向无环图（DAG）。这是因为循环可能是通过PHI函数中变量的循环依赖关系引入的。请考虑以下循环操作的SSA表示形式：

此处，counter#2的值取决于counter#1或counter#4，这是一个PHI函数，前置块决定函数的结果。在循环的下方，counter#4依赖于counter#2。这种关系将在依赖关系图中表示为一个循环。

生成依赖关系图后，很容易获得与任何受污染变量关联的根变量。此外，还可以获取任何给定变量的子变量和父变量来处理传递关系。现在唯一缺少的部分是没有表示出受污染的信息是如何向前传播到其他函数的。

静态函数钩子与过程间污点传播

一旦完成对当前函数的分析，所有带有污染参数的MLIL_CALL_SSA和MLIL_TAILCALL_SSA指令都将被处理。对于具有已知目的地（例如，MLIL_CONST_PTR)的任何调用指令，都会提取符号以检查静态钩子，具体见下面的示例代码：

for expr, callee_vars in self.callee.items():
 
        if expr.dest.operation == MediumLevelILOperation.MLIL_CONST_PTR:
            symbol = self.bv.get_symbol_at(expr.dest.constant)
 
            for func in config.function_hooks:
                if symbol and func in symbol.name:
                    self.visit_function_hooks(expr, func, callee_vars)
                    break
            else:
                dest = expr.dest.constant
                args = self.get_args_to_pass(expr, callee_vars)
 
                callee_trace = MLILTracer(self.bv, dest)
                callee_trace.set_function_args(args)
                callee_trace.trace()

静态钩子是处理函数的程序——与其他函数相比，我们打算以不同的方式处理这些函数。对libc函数memcpy的调用来说，无需进行污染传播，相反，我们只对检查受污染的大小、源或目标参数感兴趣。为了向分析器提供这些信息并进行相应的配置，我们将使用具有函数名称和参数的JSON配置，具体如下所示：

{
    "memset":["arg0", "arg1", "arg2"],
    "bzero": ["arg0", "arg1"],
    "bcopy": ["arg1", "arg2"],
    "memcpy":["arg0", "arg1", "arg2"],
    "memmove":["arg0", "arg1", "arg2"],
    "strncpy":["arg0", "arg1", "arg2"],
    "strlcpy":["arg0", "arg1", "arg2"]
}

要检查的参数从0开始索引。对于memcpy函数来说，所有3个参数都被标记为需要进行分析。与JSON配置中提供的参数索引相关的SSA变量，都需要进行污染检验。例如，配置文件中的arg2将映射到一个与memcpy函数的size参数相关的SSA参数变量：

def get_var_for_arg(self, expr, arg):
 
        params = expr.params
        argno = lambda _arg: int(_arg.split("arg").pop())
 
        if argno(arg) < len(params):
            param = params[argno(arg)]
            if param.operation in operations.MLIL_GET_VARS:
                return param.vars_read[0]
 
    def visit_function_hooks(self, expr, func, tainted_vars):
 
        args = config.function_hooks[func]
 
        for arg in args:
            ssa_var = self.get_var_for_arg(expr, arg)
            if ssa_var in tainted_vars: 
                logging.info("Potential controlled args in call to %s @ 0x%lx %s %s", func, expr.address, expr, self.get_stack_trace())

静态钩子也可用于标记要被污染和进一步传播的函数的输出变量或返回值。但是，由于未考虑特定于函数的相关细节，因此，目前尚未实现该功能。必要时，可以重用MLIL_SET_VAR_SSA操作的visitor处理程序，以在CALL操作期间实现反向污染传播。对于没有钩子的任何其他函数，可以通过将目标函数的变量标记为已污染来传播污染信息。

def set_function_args(self, funcargs):
 
        for arg, value in funcargs.items():
            # BN function.parameter_vars is buggy #2463
            for var in self.function.vars:
 
                if var.name == arg:
                    ssa_var = SSAVariable(var, 0)
 
                    if self.is_pointer(value):
                        self.source_vars[ssa_var] = value
 
                    elif self.is_tainted(value):
                        self.tainted_vars[ssa_var] = value

通过可达块跟踪漏洞

一旦污点传播和过滤阶段结束，分析的最后一个阶段就是遍历所有污点变量，并检查潜在泄漏点（sink）的可达块。根据已经报告的漏洞，我将查找目标定为涉及越界(OOB)内存访问、函数调用API（如memcpy）期间的缓冲区溢出、不可信的指针输入以及受污染的循环计数器的漏洞。本节的其余部分将详细介绍其他检测策略。

OOB读写

MySQL Cluster中的大多数漏洞都是OOB读写相关的内存访问漏洞，这些是由于缺少对不可信数组索引的验证所致。为了检测这些漏洞，我们可以将任何MLIL_LOAD_SSA或MLIL_STORE_SSA视为泄漏点。以下是来自DBDIH::execget_latest_gci_req()的示例代码：

Signal* arg2  {Register rsi}
int64_t arg1  {Register rdi}
Dbdih::execGET_LATEST_GCI_REQ:
   0 @ 005b4b24  rax#1 = zx.q([arg2#0 + 0x28].d @ mem#0)
   1 @ 005b4b27  rax_1#2 = zx.q([arg1#0 + (rax#1 << 2) + 0x9b784].d @ mem#0)
   2 @ 005b4b2e  [arg2#0 + 0x28].d = rax_1#2.eax @ mem#0 -> mem#1
   3 @ 005b4b32  return rax_1#2 
 
>>> current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.src<il: [arg1#0 + (rax#1 << 2) + 0x9b784].d @ mem#0>>>> current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.src.operation
>>> current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.src.vars_read
[<ssa

在这里，rax#1是已污染的，因此，使用MLIL_LOAD_SSA的读操作可以被认为是一个OOB读条件。类似地，考虑一下来自Thrman::execOVERLOAD_STATUS_REP()的另一个案例：

Signal* arg2  {Register rsi}
void* arg1  {Register rdi}
 
Thrman::execOVERLOAD_STATUS_REP:
   0 @ 0078415f  r14#1 = arg2#0
   1 @ 00784162  r15#1 = arg1#0
   2 @ 00784165  rax#1 = zx.q([arg2#0 + 0x28].d @ mem#0)
   3 @ 00784168  rcx#1 = [arg2#0 + 0x2c].d @ mem#0
   4 @ 0078416b  [arg1#0 + (rax#1 << 3) + 0x3ca0].d = rcx#1 @ mem#0 -> mem#1
 
>>> current_function.get_low_level_il_at(0x78416b).mlil.ssa_form<il: [arg1#0 + (rax#1 << 3) + 0x3ca0].d = rcx#1 @ mem#0 ->mem#1> 
>>> current_function.get_low_level_il_at(0x78416b).mlil.ssa_form.operation
>>> current_function.get_low_level_il_at(0x78416b).mlil.ssa_form.dest.vars_read
[<ssa

在这里，rax#1再次受到污染，因此，使用MLIL_STORE_SSA的写入操作可以被视为OOB写入条件。

API缓冲区溢出

静态函数钩子可用于检测由于传递给memcpy、memmove等函数的参数缺乏验证而导致的缓冲区溢出漏洞。有关此问题的详细信息已经在上面的“静态函数钩子与过程间污染传播”一节中进行了详细的说明。简单来说，只要挂钩函数的任何我们感兴趣的参数受到了污染，我们就会将其记录为潜在漏洞。

不可信的指针解引用

在某些情况下，我注意到MySQL Cluster会将不可信的输入转换为指针，然后进行指针解引用。为了识别这种漏洞，我们可以借助于Binary Ninja的类型信息。MLIL变量对象有一个Type属性，用于返回与变量相关的Type对象。一个Type对象的类型可以用type_class属性来访问。这里的模型是，污点源指向Signal结构中的一个污点内存区域，而目标变量是PointerTypeClass类型的。Type对象还有一个confidence属性，具体如下图所示：

>>> current_function.get_low_level_il_at(here).mlil.ssa_form
>>> current_function.get_low_level_il_at(here).mlil.ssa_form.dest>> current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var
>>> current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type
>>> current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type.type_class
>>> current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type.confidence
255

对于变量类型来说，confidence的最大值为255。为减少误报，分析器仅考虑具有最大置信度的类型信息。

if (dest.var.type.type_class == TypeClass.PointerTypeClass
        and dest.var.type.confidence == 255 and expr.src.operation == MediumLevelILOperation.MLIL_LOAD_SSA):
        
        instr = self.function_mlilssa[expr.instr_index]
        logging.info("Potential untrusted pointer load @ 0x%lx %s %s", expr.address, instr, self.get_stack_trace())

循环中的污点控制流操作

我们知道，依赖于受污染变量的某些循环终止条件会导致我们感兴趣的漏洞。然而Binary Ninja的MLIL并没有提供关于循环的信息，因此，替代方案是通过HLIL来检测受污染的循环条件。比如，Cmvmi::execEVENT_SUBSCRIBE_REQ()中循环语句的HLIL如下所示：

/* 0050516b */              do
/* 0050516b */                  uint64_t rsi_7 = zx.q(*(r12 + (rcx_3 << 2) + 0x30))
/* 00505170 */                  if (rsi_7 u> 0x10] = rsi_7.b
/* 00505184 */                      rdx_5 = *(r12 + 0x2c)
/* 00505160 */                  rcx_3 = rcx_3 + 1
/* 00505160 */              while (rcx_3 u< zx.q(rdx_5))

这里的问题是，我们已经使用MLIL实现了整个污点传播，而Binary Ninja却无法提供MLIL和HLIL之间的映射。因此，即使可以检测到循环，也需要知道受污染的MLIL变量是否映射到循环条件中使用的HLIL变量。

不过，倒是存在一个变通方法，即HLIL指令具有一个条件属性，该属性可以用来获取与循环关联的条件语句，而这个条件语句的地址可以映射到相应的MLIL_IF指令。

>>> expr<HLIL_DO_WHILE: do while (rcx_3 u< zx.q(rdx_5))>>>> expr.condition<HLIL_CMP_ULT: rcx_3 u< zx.q(rdx_5)>>>> expr.operation
>>> hex(expr.condition.address)
'0x505169'
 
>>> current_function.get_low_level_il_at(here).mlil.ssa_form
>>> hex(current_function.get_low_level_il_at(here).mlil.ssa_form.address)
'0x505169'

因此，如果任何一条MLIL_IF指令被污染，并且是HLIL循环条件的一部分，那么分析器就会将其记录为一个潜在的漏洞。

关于支配关系的实验

支配关系提供了关于基本块执行顺序的相关信息。如果所有通向Y的路径都要经过X，那么，我们就可以说基本块X支配着另一个基本块Y。

在所提供的图中，节点B支配着节点C、D、E和F，因为通往这些节点的所有路径必须经过节点B。因此，被节点B支配的全部节点集包括B、C、D、E和F节点。此外，还有一个相关的概念叫做严格支配方，它并不考虑可疑的节点。因此，被节点B严格支配的所有节点的集合包括节点C、D、E和F。

Binary Ninja的BasicBlock对象具有dominators和strict_dominators属性，提供关于函数中支配关系的相关信息。

>>> current_function.mlil.ssa_form.basic_blocks
[
>>> current_function.mlil.ssa_form.basic_blocks[2].dominators
[
>>> current_function.mlil.ssa_form.basic_blocks[2].strict_dominators
[

那么，我们该如何利用Binary Ninja中可用的dominance属性来处理污染约束，而不是通过networkx包中的图可达性算法来处理这个问题呢？

将约束映射到支配块

为了检查一个SSA变量的def-use链中的所有基本块是否可达，我们可以遵循以下步骤：

查找与该变量关联的所有约束块。

使用def-use链获取所有引用该变量的基本块。

对于每个基本块，检查它是否被约束块严格支配。如果是，则该变量被认为是该基本块的有效变量，并且被认为是不可达的。

回到同一个示例，索引在中得到验证，而它又是的支配方。因此，通过检查支配方的约束块，就可以确定可达性。

支配关系引发的误报

虽然支配关系是有希望的方法，并给出了良好的结果，但它确实会引起某些误报。考虑以下CFG，其中验证是在两个不同的程序路径中完成的：

>>> current_function.mlil.ssa_form.basic_blocks
[
>>> current_function.mlil.ssa_form.basic_blocks[7]
>>> current_function.mlil.ssa_form.basic_blocks[7].strict_dominators
[

这里，在访问潜在的泄露块之前，就已经在两个不同的程序路径中对索引进行了相应的检查。但是，执行检查的约束块和都不是支配方。在这种情况下，由于约束块不能映射到任何支配方，潜在的泄露块在地址0x11BA处进行读访问时，将被视为易受攻击的。实际上，这是一个假阳性结果。

另外，branch_dependence属性也是这种情况：它返回由分支指令索引和是否抵达指令的分支判断所组成的字典。当真分支和假分支都支配指令基本块时，我们将无法获得可达性的信息。

>>> current_function.get_llil_at(here).mlil.ssa_form
>>> current_function.get_llil_at(here).mlil.ssa_form.instr_index
9
>>> current_function.get_llil_at(here).mlil.ssa_form.branch_dependence
{2:
>>> current_function.get_llil_at(here).mlil.ssa_form
>>> current_function.get_llil_at(here).mlil.ssa_form.instr_index
13
>>> current_function.get_llil_at(here).mlil.ssa_form.branch_dependence
{}

从扫描结果中可以看出，大多数约束都是支配块的一部分。在通过多个代码路径进行验证的情况下，是很少出现误报的。由于借助变量的定义和使用的路径搜索算法可以消除这些假阳性结果，因此，我更倾向于采用这种方法，而不是支配者。然而，为了进行相关的实验，存储库仍然提供了相关的代码。

注意事项

使用Binary Ninja加载目标ndbd可执行文件后，将生成BNDB分析数据库。然后，我们就通过分析器对ndbd.bndb执行分析，以提高分析速度：

python3 mysql_bugs.py--function_hooks functions_to_hook.json ndbd.bndb

虽然没有对速度进行优化，但是分析器只运行了约4-5分钟，并返回195个结果。其中，有些结果是重复的，因为helper函数中的单个漏洞可能会被多个处理程序使用。并且，分析器能够找出大部分已经知道的安全问题，以及一些以前不知道的安全问题：ZDI-CAN-15120、ZDI-CAN-15121和ZDI-CAN-15122漏洞。然而，与静态分析结果相关的分类成本是很高的，尤其是当目标不太熟悉时。幸运的是，我的同事Lucas已经在代码库上花了相当多的时间，这使得对结果进行分类变得更加容易。

该项目的源代码可以在这里找到。

鸣谢与参考资料

感谢Lucas Leong的所有讨论和分类，他的文章MindShare：When MySQL Cluster Encounters Taint Analysis是对MySQL Cluster进行静态污点分析的绝佳参考资料。

关于图的可达性问题的污染分析，可以参考Tainted Flow Analysis on e-SSA-form Programs一文。

这里也提供了许多关于Binary Ninja的优秀文章。

Josh Watson创建了许多基于Binary Ninja的项目。我们的visitor类是在emILator的基础上实现的。

本文中的所有代码片段均由Jordan提供，同时，还要感谢Binary Ninja slack社区热心回答我们的各种问题。

小结

我希望您喜欢这篇通过Binary Ninja软件，使用污点分析技术挖掘安全漏洞的文章。几天后，我将返回头来讨论如何使用Clang Static Analyzer(CSA)来检测不受信任的指针解引用和受污染的循环条件。在此之前，您可以在Twitter @renorobertr上找到我，并一起探讨最新的exploit技术和安全补丁。

本文翻译自：https://www.zerodayinitiative.com/blog/2022/2/14/static-taint-analysis-using-binary-ninja-a-case-study-of-mysql-cluster-vulnerabilities如若转载，请注明原文地址