漏洞挖掘与Semmle QL实战：第二部分

本系列的第一部分介绍了Semmle QL以及Microsoft安全响应中心（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
 7
 8
 9
10
11
12


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
13
14
15


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)`	node1的数据也会污染node2
`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 $@", mhf, m

使用Semmle QL进行漏洞挖掘实战：Azure固件安全审计

本文详细介绍了Microsoft安全响应中心使用Semmle QL对Azure固件组件进行安全审计的过程，包括攻击面定义、数据流分析、内存安全漏洞检测和路径遍历漏洞发现等技术内容。