漏洞挖掘与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


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


// 检查调用图以匹配任何可能最终调用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将从调用跟踪控制流图直到匹配使用。下图说明了这一点：

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

暂时就这些。下一部分将涵盖使用QL进行数据流分析和污点跟踪，以及我们对Azure固件组件安全审查的示例。

Steven Hunter，MSRC漏洞与缓解团队

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

本文介绍了微软安全响应中心如何使用Semmle QL进行漏洞变体分析，包括整数溢出检查错误、SafeInt不安全使用和JavaScript重入导致的使用后释放漏洞的检测方法和实际案例。

漏洞挖掘与Semmle QL，第一部分

不正确的整数溢出检查

不安全使用SafeInt

JavaScript重入导致使用后释放