使用Semmle QL进行漏洞挖掘，第二部分

本系列的第一部分介绍了Semmle QL，以及微软安全响应中心（MSRC）如何使用它来调查报告给我们的漏洞变体。本文讨论了我们如何主动使用它的一个例子，涵盖了对Azure固件组件的安全审计。

这是对Azure服务进行更广泛的深度防御安全审查的一部分，从一个假设的对手的角度探索攻击向量，该对手已经渗透了至少一个安全边界，现在位于服务后端的操作环境中（在下图中用*标记）。

审查的目标之一是一个基于Linux的嵌入式设备，它与服务后端和管理后端接口，在两者之间传递操作数据。该设备的主要攻击面是在两个接口上使用的管理协议。

对其固件的初步手动审查表明，该管理协议是基于消息的，有超过四百种不同的消息类型，每种都有自己的处理函数。手动审核每个函数将是繁琐且容易出错的，因此使用Semmle来扩展我们的代码审查能力是一个容易的选择。我们总共发现了33个易受攻击的消息处理函数，使用了本文讨论的静态分析技术。

定义攻击面

我们的第一步是编写一些QL来建模来自攻击者的数据。管理协议基于请求-响应工作，每个消息请求类型由类别号和命令号标识。这在源代码中使用结构数组定义，例如：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


MessageCategoryTable g_MessageCategoryTable[] = 
{
  { CMD_CATEGORY_BASE, g_CommandHandlers_Base },
  { CMD_CATEGORY_APP0, g_CommandHandlers_App0 },
  …
  { NULL, NULL }
};

CommandHandlerTable g_CommandHandlers_Base [] = 
{
  { CMD_GET_COMPONENT_VER, sizeof(ComponentVerReq), GetComponentVer, … },
  { CMD_GET_GLOBAL_CONFIG, -1, GetGlobalConfig, … },
  …
  { NULL, NULL, NULL, … }
};

在上面的例子中，具有类别类型CMD_CATEGORY_BASE和命令类型CMD_GET_COMPONENT_VER的消息将被路由到GetComponentVer函数。命令处理程序表还有关于预期请求消息大小的信息，该信息在调用处理函数之前在消息分发例程中进行验证。

我们使用以下QL定义了消息处理程序表：

1
2
3
4
5
6
7
8


class CommandHandlerTable extends Variable {
  CommandHandlerTable() {
    exists(Variable v | 
      v.hasName("g_MessageCategoryTable") and
      this.getAnAccess() = v.getInitializer().getExpr().getAChild().getChild(1)
    )
  }
}

这需要一个名为g_MessageCategoryTable的变量，找到其初始化表达式，并匹配此表达式的所有子项——每个子表达式对应于消息类别表的一行。对于每一行，它取第二列（这是getChild(1)，因为getChild谓词的参数是从零开始的），每个都是对命令处理程序表的引用，并匹配引用的变量。在上面的例子中，这些将是g_CommandHandlers_Base和g_CommandHandlers_App0。

我们使用类似的方法定义了消息处理函数集：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


class MessageHandlerFunction extends Function {
  Expr tableEntry;

  MessageHandlerFunction() {
    exists(CommandHandlerTable table |
      tableEntry = table.getInitializer().getExpr().getAChild()
    )
    and this = tableEntry.getChild(2).(FunctionAccess).getTarget()
  }

  int getExpectedRequestLength() {
    result = tableEntry.getChild(1).getValue().toInt()
  }
  …
}

这个QL类使用成员变量tableEntry来保存所有命令处理程序表中的所有行。这样它可以在特征谓词（MessageHandlerFunction() { … }）和getExpectedRequestLength()中引用，而无需重复定义。

所有这些映射到上面的代码结构如下：

每个消息处理函数具有相同的签名：

1
2


typedef unsigned char UINT8;
int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse);

并遵循一个通用模式，其中请求数据被转换为表示消息布局的结构类型，并通过其字段访问：

1
2
3
4
5
6
7


int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse)
{
  ExampleMessageRequest *pMsgReq = (ExampleMessageRequest *)pRequest;
  …
  someFunction(pMsgReq->aaa.bbb)
  …
}

在此分析中，我们只对请求数据感兴趣。我们在MessageHandlerFunction QL类中定义了两个额外的谓词来建模请求数据及其长度：

1
2
3
4
5
6


class MessageHandlerFunction extends Function {
  Expr tableEntry;
  …
  Parameter getRequestDataPointer() { result = this.getParameter(0) }
  Parameter getRequestLength() { result = this.getParameter(1) }
}

抽象出消息处理函数的定义后，它可以像任何其他QL类一样使用。例如，此查询按圈复杂度的降序列出所有消息处理函数：

1
2
3


from MessageHandlerFunction mhf
select mhf, mhf.getADeclarationEntry().getCyclomaticComplexity() as cc
order by cc desc

分析数据流

现在我们已经定义了一组不可信数据的入口点，下一步是找到它可能以不安全的方式使用的地方。为此，我们需要跟踪此类数据在代码库中的流动。QL提供了一个强大的全局数据流库，抽象了其中涉及的大多数棘手的语言特定细节。

数据流库通过以下方式引入查询范围：

1

import semmle.code.cpp.dataflow.DataFlow

它通过子类化DataFlow::Configuration并覆盖其谓词来使用，以定义数据流，因为它适用于DataFlow::Node，一个表示数据可以流经的任何程序工件的QL类：

配置谓词	描述
`isSource(source)`	数据必须从源流动
`isSink(sink)`	数据必须流向接收器
`isAdditionalFlowStep(node1, node2)`	数据也可以在node1和node2之间流动
`isBarrier(node)`	数据不能流过节点

大多数数据流查询看起来像这样：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12


class RequestDataFlowConfiguration extends DataFlow::Configuration {
  RequestDataFlowConfiguration() { this = "RequestDataFlowConfiguration" }

  override predicate isSource(DataFlow::Node source) { … }
  override predicate isSink(DataFlow::Node sink) { … }
  override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { … }
  override predicate isBarrier(DataFlow::Node node) { … }
}

from DataFlow::Node source, DataFlow::Node sink
where any(RequestDataFlowConfiguration c).hasFlow(source, sink)
select "Data flow from $@ to $@", source, sink

请注意，QL数据流库执行过程间分析——除了检查函数本地的数据流外，它还包括通过函数调用参数流动的数据。这对我们的安全审查是一个基本特性，因为尽管下面讨论的易受攻击的代码模式在简单的示例函数中显示以便于演示，但在我们目标的实际源代码中，大多数结果都有跨越多个复杂函数的数据流。

查找内存安全漏洞

由于此固件组件是纯C代码库，我们首先决定搜索与内存安全相关的代码模式。

此类错误的一个常见来源是在没有执行边界检查的情况下进行数组索引。单独搜索此模式将提供很大一部分结果，这些结果很可能不是安全漏洞，因为我们真正感兴趣的是攻击者对索引值有一定控制的地方。因此，在这种情况下，我们正在寻找数据流，其中接收器是数组索引表达式，源是消息处理函数的请求数据，并且在由相关边界检查保护的任何数据流节点上存在屏障。

例如，我们想找到匹配如下代码的数据流：

1
2
3
4
5
6


int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
  ExampleMessageRequest *pMsgReq(3) = (ExampleMessageRequest *)pRequest(2);
  int index1(6) = pMsgReq(4)->index1(5);
  pTable1[index1(7:sink)].field1 = pMsgReq->value1;
}

但我们也想排除匹配如下代码的数据流：

1
2
3
4
5
6
7
8
9


int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
  ExampleMessageRequest *pMsgReq(3) = (ExampleMessageRequest *)pRequest(2);
  int index2(6) = pMsgReq(4)->index2(5);
  if (index2 >= 0 && index2 < PTABLE_SIZE)
  {
    pTable2[index2].field1 = pMsgReq->value2;
  }
}

源使用前面讨论的MessageHandlerFunction类定义，我们可以使用ArrayExpr的getArrayOffset谓词来定义合适的接收器：

1
2
3
4
5
6
7


override predicate isSource(DataFlow::Node source) {
  any(MessageHandlerFunction mhf).getRequestDataPointer() = source.asParameter()
}

override predicate isSink(DataFlow::Node sink) {
  exists(ArrayExpr ae | ae.getArrayOffset() = sink.asExpr())
}

默认情况下，数据流库只包括在每个节点保留值的流，例如函数调用参数、赋值表达式等。但我们还需要数据从请求数据指针流向它被转换到的结构的字段。我们将这样做：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) {
  // 请求包上的任何终端字段访问
  // 例如，在表达式a->b.c中，数据从a流向c
  exists(Expr e, FieldAccess fa |
    node1.asExpr() = e and
    node2.asExpr() = fa |
    fa.getQualifier*() = e and
    not (fa.getParent() instanceof FieldAccess)
  )
}

为了排除有边界检查的流，我们在任何节点上放置一个屏障，该节点具有在控制流图中较早的某些条件语句中使用的变量或字段（目前，我们假设任何此类边界检查都是正确完成的）：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


override predicate isBarrier(DataFlow::Node node) {
  exists(ConditionalStmt condstmt |
    // 数据流节点变量用于条件语句的表达式中
    // 这包括字段（因为FieldAccess扩展了VariableAccess）
    node.asExpr().(VariableAccess).getTarget().getAnAccess() = condstmt.getControllingExpr().getAChild*()
    // 并且该语句在控制流图中先于数据流节点
    and condstmt.getASuccessor+() = node.asExpr()
    // 并且数据流节点本身不是条件语句表达式的一部分
    and not (node.asExpr() = cs.getControllingExpr().getAChild*())
  )
}

将此应用于上面的两个例子，每个节点的数据流将是：

在我们的固件代码库中，此查询在15个消息处理函数中总共定位了18个漏洞，混合了攻击者控制的越界读取和写入。

我们应用了类似的分析来查找函数调用的参数来自消息请求数据而未经首先验证的地方。首先，我们定义了一个QL类来定义感兴趣的函数调用和参数，包括对memcpy和类似函数_fmemcpy的大小参数，以及CalculateChecksum的长度参数。CalculateChecksum是此代码库特定的函数，将返回缓冲区的CRC32，并可能被用作信息泄露原语，其中消息处理函数将此值复制到其响应缓冲区中。

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


class ArgumentMustBeCheckedFunctionCall extends FunctionCall {
  int argToCheck;

  ArgumentMustBeCheckedFunctionCall() {
    ( this.getTarget().hasName("memcpy") and argToCheck = 2 ) or
    ( this.getTarget().hasName("_fmemcpy") and argToCheck = 2 ) or
    ( this.getTarget().hasName("CalculateChecksum") and argToCheck = 1 )
  }

  Expr getArgumentToCheck() { result = this.getArgument(argToCheck) }
}

接下来，我们修改了先前查询的接收器，以匹配ArgumentMustBeCheckedFunctionCall而不是数组索引：

1
2
3
4


override predicate isSink(DataFlow::Node sink) {
  // 接收器节点是必须首先检查的函数调用的参数
  exists (ArgumentMustBeCheckedFunctionCall fc | fc.getArgumentToCheck() = sink.asExpr())
}

此查询在13个消息处理程序中揭示了另外17个漏洞，主要是攻击者控制的越界读取（我们后来确认在响应消息中披露），其中一个是越界写入。

污点跟踪

在上面的查询中，我们覆盖了数据流库的isAdditionalFlowStep谓词，以确保在数据流向结构指针的地方，该结构的字段将被添加为数据流图中的节点。我们这样做是因为默认情况下，数据流分析只包括数据值保持未修改的路径，但我们还想跟踪它可能影响的一组特定表达式。也就是说，我们定义了一组由不可信数据污染的特定表达式。

QL包含一个内置库，以应用更通用的方法进行污点跟踪。它在数据流库的基础上开发，用一组更丰富的值修改表达式规则覆盖了isAdditionalFlowStep。这是TaintTracking库，它以类似于DataFlow的方式导入：

1

import semmle.code.cpp.dataflow.TaintTracking

它的使用方式与数据流库几乎相同，除了要扩展的QL类是TaintTracking::Configuration，具有这些配置谓词：

配置谓词	描述
`isSource(source)`	数据必须从源流动
`isSink(sink)`	数据必须流向接收器
`isAdditionalTaintStep(node1, node2)`	节点1的数据也会污染节点2
`isSanitizer(node)`	数据不能流过节点

我们重新运行了先前的查询，删除了isAdditionalFlowStep（因为我们不再需要定义它）并将isBarrier重命名为isSanitizer。正如预期的那样，它返回了上面提到的所有结果，但还发现了一些数组索引中的整数下溢缺陷。例如：

1
2
3
4
5
6


int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
  ExampleMessageRequest *pMsgReq(3) = (ExampleMessageRequest *)pRequest(2);
  int index1(6) = pMsgReq(4)->index1(5);
  pTable1[(index1(7) - 2)(8:sink)].field1 = pMsgReq->value1;
}

对于我们内部对每种漏洞类型的报告，我们感兴趣的是将这些与先前的查询结果分开分类。这涉及对接收器的简单修改，使用SubExpr QL类：

1
2
3
4
5
6
7
8


override predicate isSink(DataFlow::Node sink) {
  // 此接收器是减法表达式的左操作数，
  // 它是数组偏移表达式的一部分，例如a[x - 1]中的x
  exists(ArrayExpr ae, SubExpr s |
    sink.asExpr() instanceof FieldAccess and
    ae.getArrayOffset().getAChild*() = s and
    s.getLeftOperand().getAChild*() = sink.asExpr())
}

这为我们提供了另外3个漏洞，分布在2个消息处理函数中。

查找路径遍历漏洞

为了查找潜在的路径遍历漏洞，我们使用QL尝试识别消息处理函数，这些函数在文件打开函数中使用攻击者控制的文件名。

这次我们使用了稍微不同的污点跟踪方法，定义了一些额外的污点步骤，这些步骤将通过各种字符串处理C库函数流动：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29


predicate isTaintedString(Expr expSrc, Expr expDest) {
  exists(FunctionCall fc, Function f |
    expSrc = fc.getArgument(1) and
    expDest = fc.getArgument(0) and
    f = fc.getTarget() and (
      f.hasName("memcpy") or
      f.hasName("_fmemcpy") or
      f.hasName("memmove") or
      f.hasName("strcpy") or
      f.hasName("strncpy") or
      f.hasName("strcat") or
      f.hasName("strncat")
    )
  )
  or exists(FunctionCall fc, Function f, int n |
    expSrc = fc.getArgument(n) and
    expDest = fc.getArgument(0) and
    f = fc.getTarget() and (
      (f.hasName("sprintf") and n >= 1) or
      (f.hasName("snprintf") and n >= 2)
    )
  )
}

…

override predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) {
  isTaintedString(node1.asExpr(), node2.asExpr())
}

并将接收器定义为文件打开函数的路径参数：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15


class FileOpenFunction extends Function {
  FileOpenFunction() {
    this.hasName("fopen") or this.hasName("open")
  }

  int getPathParameter() { result = 0 } // 文件名参数索引
}

…

override predicate isSink(DataFlow::Node sink) {
  exists(FunctionCall fc, FileOpenFunction fof |
    fc.getTarget() = fof and
    fc.getArgument(fof.getPathParameter()) = sink.asExpr())
}

根据我们从初步审查中观察到的关于目标设备如何工作的一些先验知识，我们期望在解决下一个问题（即排除数据经过验证的流，如先前的查询）之前至少有一些结果。然而，查询没有返回任何结果。

由于没有数据流路径可检查，我们退而求其次，查询函数调用图以搜索消息处理函数与文件打开函数调用之间的任何路径，排除路径参数为常量的调用：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


// 此递归谓词定义了函数调用图
predicate mayCallFunction(Function caller, FunctionCall fc) {
  fc.getEnclosingFunction() = caller or
  mayCallFunction(fc.getTarget(), fc)
}

from MessageHandlerFunction mhf, FunctionCall fc, FileOpenFunction fof
where mayCallFunction(mhf, fc)
  and fc.getTarget() = fof
  and not fc.getArgument(fof.getPathParameter()).isConstant()
select mhf, "$@ may have a path to $@",

使用Semmle QL进行漏洞挖掘实战：第二部分

本文详细介绍了微软安全响应中心如何使用Semmle QL对Azure固件组件进行安全审计，通过定义攻击面、分析数据流和污点跟踪技术，发现了33个存在内存安全和路径遍历漏洞的消息处理函数。