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

在本博客之前，我们讨论过MSRC如何自动化分析报告和发现的漏洞的根本原因。完成这一步后，我们的下一步是变体分析：查找并调查该漏洞的任何变体。找到所有此类变体并同时修补它们非常重要，否则我们将承担这些变体在野外被利用的风险。在这篇文章中，我想解释我们在变体查找中使用的自动化方法。

过去一年左右，我们一直在使用Semmle（一个第三方静态分析环境）来增强我们的手动代码审查流程。它将代码编译为关系数据库（快照数据库——数据库和源代码的组合），并使用Semmle QL（一种为程序分析设计的声明式、面向对象的查询语言）进行查询。

基本工作流程是，在根本原因分析之后，我们编写查询来查找与原始漏洞语义相似的代码模式。任何结果都会像往常一样进行分类，并提供给我们的工程团队以开发修复程序。此外，查询被放置在一个中央存储库中，供MSRC和其他安全团队定期重新运行。这样，我们可以随着时间的推移和跨多个代码库扩展我们的变体查找。

除了变体分析，我们还在源代码的安全审查中主动使用QL。这将是未来博客文章的主题。现在，让我们看一些受MSRC案例启发的真实示例。

不正确的整数溢出检查

第一个案例是一个定义简单但在大代码库中查找变体会很繁琐的错误。

以下代码显示了检测无符号整数加法溢出的常见习惯用法：

1

if (x + y < x) { // 处理整数溢出 }

不幸的是，当整数类型的宽度足够小以至于受到整数提升的影响时，这种方法无法正常工作。例如，如果x和y都是unsigned short，在编译时，上述代码最终将等同于(unsigned int)x + y < x，使得此溢出检查无效。

这是一个匹配此代码模式的QL查询：

1
2
3
4
5
6
7
8


import cpp
from AddExpr a, Variable v, RelationalOperation r
where a.getAnOperand() = v.getAnAccess()
and r.getAnOperand() = v.getAnAccess()
and r.getAnOperand() = a
and forall(Expr op | op = a.getAnOperand() | op.getType().getSize() < 4)
and not a.getExplicitlyConverted().getType().getSize() < 4
select r, "由于整数提升导致的无效溢出检查"

在from子句中，我们定义了变量及其类型，用于查询的其余部分。AddExpr、Variable和RelationalOperation是QL类，表示快照数据库中的各种实体集，例如RelationalOperation涵盖每个具有关系操作（小于、大于等）的表达式。

where子句是查询的核心，使用逻辑连接词和量词来定义如何关联变量。分解来看，这意味着加法表达式和关系操作需要相同的变量作为它们的操作数之一（上面示例代码中的x）：

1

a.getAnOperand() = v.getAnAccess() and r.getAnOperand() = v.getAnAccess()

关系操作的另一个操作数必须是加法：

1

r.getAnOperand() = a

加法的两个操作数的宽度必须小于32位（4字节）：

1

forall(Expr op | op = a.getAnOperand() | op.getType().getSize() < 4)

但是，如果加法表达式上有显式转换，我们不关心它是否小于32位：

1

not a.getExplicitlyConverted().getType().getSize() < 4

（这样像(unsigned short)(x + y) < x这样的检查就不会被查询标记。）

最后，select子句定义了结果集。

这个漏洞最初在Chakra（Edge的JavaScript引擎）中报告，该特定无效溢出检查的后果是内存损坏。查询匹配了原始漏洞，但在Chakra中没有找到其他变体。然而，当将此确切查询应用于其他Windows组件时，我们发现了几个变体。

不安全使用SafeInt

另一种自己编写整数溢出检查的方法是使用内置此类检查的库。SafeInt是一个C++模板类，它重写算术运算符以在检测到溢出时抛出异常。

以下是如何正确使用它的示例：

1

int x, y, z; // ... z = SafeInt<int>(x) + y;

但这里是一个如何无意中误用的示例——传递给构造函数的表达式可能已经溢出：

1

int x, y, z; // ... z = SafeInt<int>(x + y);

如何编写查询来检测这种情况？在前一个示例中，我们的查询仅使用内置的QL类。对于这个，让我们从定义我们自己的类开始。为此，我们选择一个或多个QL类来子类化（使用extends），并定义一个特征谓词，指定快照数据库中与该类匹配的实体：

1
2
3
4
5


class SafeInt extends Type { 
    SafeInt() { 
        this.getUnspecifiedType().getName().matches("SafeInt<%") 
    } 
}

QL类Type表示快照数据库中所有类型的集合。对于QL类SafeInt，我们将其子集化为仅名称以“SafeInt<”开头的类型，从而表明它们是SafeInt模板类的实例化。getUnspecifiedType()谓词用于忽略typedef和类型说明符（如const）。

接下来，我们定义可能溢出的表达式子集。大多数算术操作可能溢出，但并非所有；这使用QL的instanceof运算符来定义哪些操作。我们使用递归定义，因为我们需要包含像(x+1)/y这样的表达式，即使x/y不被包含。

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


class PotentialOverflow extends Expr {
    PotentialOverflow() {
        (this instanceof BinaryArithmeticOperation // 匹配 x+y x-y x*y
        and not this instanceof DivExpr // 但不包括 x/y
        and not this instanceof RemExpr) // 或 x%y
        or (this instanceof UnaryArithmeticOperation // 匹配 x++ x-- ++x --x -x
        and not this instanceof UnaryPlusExpr) // 但不包括 +x
        // 递归定义以捕获上述排除操作的操作数中的潜在溢出
        or this.(BinaryArithmeticOperation).getAnOperand() instanceof PotentialOverflow
        or this.(UnaryPlusExpr).getOperand() instanceof PotentialOverflow
    }
}

最后，我们在查询中关联这两个类：

1
2
3


from PotentialOverflow po, SafeInt si 
where po.getParent().(Call).getTarget().(Constructor).getDeclaringType() = si 
select po, po + " 可能在转换为 " + si + " 之前溢出"

.(Call)和.(Constructor)是内联转换的示例，类似于instanceof，是限制匹配哪些QL类的另一种方式。在这种情况下，我们说的是，给定一个可能溢出的表达式，我们只关心它的父表达式是某种调用。此外，我们只想知道该调用的目标是否是构造函数，以及它是否是某个SafeInt的构造函数。

像前一个示例一样，这是一个在多个代码库中提供了许多可操作结果的查询。

JavaScript重入导致使用后释放

下一个示例是Edge中的一个漏洞，由重入JavaScript代码引起。

Edge定义了许多可以从JavaScript调用的函数。这个模型函数说明了漏洞的本质：

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


HRESULT SomeClass::vulnerableFunction(Var args, UINT argCount, Var retVal)
{
    // 获取第一个参数 - 从Chakra获取数组指针
    BYTE* pBuffer;
    UINT bufferSize;
    hr = Jscript::GetTypedArrayBuffer(args[1], &pBuffer, &bufferSize);
    
    // 获取第二个参数 - 从Chakra获取整数值
    int someValue;
    hr = Jscript::VarToInt(args[2], &someValue);
    
    // 对先前获取的数组执行某些操作
    doSomething(pBuffer, bufferSize);
    ...
}

问题是当Edge回调到Chakra时，例如在VarToInt期间，可能会执行任意JavaScript代码。通过传递一个重写valueOf以释放缓冲区的JavaScript对象，可以利用上述函数，因此当VarToInt返回时，pBuffer是一个悬空指针：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10


var buf = new ArrayBuffer(length);
var arr = new Uint8Array(buf);
var param = {} 
param.valueOf = function() {
    // 释放buf（实际执行此操作的代码将在别处定义）
    neuter(buf); // 通过例如将其发布到web worker来使buf失效
    gc(); // 触发垃圾收集
    return 0;
};
vulnerableFunction(arr, param);

因此，我们使用QL查找的特定模式是：从GetTypedArrayBuffer获取指针，随后调用某些可能执行JavaScript的Chakra函数，然后使用该指针。

对于数组缓冲区指针，我们匹配对GetTypedArrayBuffer的调用，其中第二个参数（Call的getArgument是零索引的）是一个取地址表达式（&），并取其操作数：

1
2
3
4
5
6
7
8


class TypedArrayBufferPointer extends Expr { 
    TypedArrayBufferPointer() { 
        exists(Call c | 
            c.getTarget().getName() = "GetTypedArrayBuffer"
            and this = c.getArgument(1).(AddressOfExpr).getOperand()
        ) 
    } 
}

这里使用exists逻辑量词将新变量（c）引入作用域。

有几个Chakra API函数可能用于JavaScript重入。我们可以通过名称定义它们，但也可以识别执行此任务的内部Chakra函数，并使用QL从调用图中找出：

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11


// 检查调用图以匹配任何可能最终调用MethodCallToPrimitive的函数
predicate mayExecJsFunction(Function f) {
    exists(Function g | f.calls+(g) and g.hasName("MethodCallToPrimitive"))
}

// 这定义了对任何上述函数的调用
class MayExecJsCall extends FunctionCall {
    MayExecJsCall() {
        mayExecJsFunction(this)
    }
}

calls谓词的“+”后缀指定了传递闭包——它将谓词应用于自身，直到有匹配为止。这允许简洁地探索函数调用图。

最后，这个查询将这些QL类定义结合在一起，通过控制流关联它们：

1
2
3
4
5
6


from TypedArrayBufferPointer def, MayExecJsCall call, VariableAccess use, Variable v 
where v.getAnAccess() = def 
and v.getAnAccess() = use 
and def.getASuccessor+() = call 
and call.getASuccessor+() = use 
select use, "在定义 " + def + " 和使用 " + use + " 之间调用 " + call

谓词getASuccessor()指定控制流中的下一个语句或表达式。因此，使用例如call.getASuccessor+() = use将从调用开始跟随控制流图，直到有与use匹配的项。下图说明了这一点：

[控制流图示意图]

此查询除了最初报告的漏洞外，还发现了四个变体，所有这些都被评估为严重严重性。

以上就是本次的内容。下一部分将涵盖使用QL进行数据流分析和污点跟踪，以及我们在Azure固件组件安全审查中的示例。

Steven Hunter，MSRC漏洞与缓解团队