使用 Semmle QL 进行漏洞搜索 Part 1

翻译自：https://blogs.technet.microsoft.com/srd/2018/08/16/vulnerability-hunting-with-semmle-ql-part-1/
作者：swiat

前言

在这篇博客之前，我们聊过MSRC是怎么自动对报告和发现的漏洞进行根本原因分析的。完成这个之后，我们的下一步是变体分析：寻找和调查漏洞的任何变体。重要的是我们要找到所有的变体并同时修补它们，否则我们将承担它们在别的地方被利用的风险。在这篇文章中，我想说明一下我们在变体发现中所使用到的自动化操作。

在过去一年左右的时间里，我们一直在使用第三方静态分析环境Semmle扩充我们的手动代码审查流程。它把代码编译到一个关系型数据库（快照数据库——一个数据库和源代码的结合），使用Semmle QL查询，Semmle QL是一种用于程序分析的陈述性的、面向对象的查询语言。

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

除了变体分析以外，我们还前瞻性的在源代码的安全性评估中使用QL。这将会是未来的一个博客主题。现在，让我们看一些受MSRC案例启发的现实案例。

不正确的整数溢出检查

第一种情况是这种直接定义的错误，在大型代码库中找到变体会是一个十分繁琐的过程。

下面的代码展示了在添加无符号整数时检测溢出的常用习惯用法：

if (x + y < x) {
    // handle integer overflow
}

不幸的是，当整数类型的宽度足够小以进行整型提升时，这个方法不起作用。例如，如果x和y都是unsigned short，在编译时，上述代码讲等同于(unsigned int)x + y < x，使溢出检查失效。

这是一个匹配这种代码模式的QL查询语句：

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, "Useless overflow check due to integral promotion"

在from子语句中，我们定义了要在其余的查询语句中要用到的变量，以及它们的类型。AddExpr，Variable和RelationalOperation是表示快照数据库中各种实体集的QL类，例如，RelationalOperation包含所有具有关系操作的表达式（小于，大于等）。

where子语句是查询的一个元组成，使用逻辑连接词和量词来定义如何与变量建立联系。把它拆分开来看，这意味着加法表达式和关系运算需要一个与其中一个操作数相同的变量（上面代码示例中的x）：

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

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

r.getAnOperand() = a

添加的两个操作数的宽度必须都小于32位（4比特）

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

但如果加法表达式里有一个显示的强制类型转换，我们就对它是否小于32位不感兴趣了。

（这样的检查就类似于 (unsigned short)(x + y) < x，不会被查询语句标记）

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

此漏洞最初在Chakra（Edge的JavaScript引擎）中报告，无效的溢出检查导致的结果是内存崩溃。该查询与原始漏洞匹配，但在Chakra中没有其他变体。但是，我们在将此查询应用于其他Windows组件时，却发现了几个变体。

SafeInt的不安全使用

另一种检查整数溢出的方法是使用内置此类检查的库。SafeInt是一个C ++模板类，它在检测到溢出的地方覆盖掉算术操作以抛出一个异常。

下面是一个正确使用它的例子：

int x, y, z;

// ...

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

但这有一个无意中被误用的例子——传递给构造函数的表达式可能已经溢出了：

int x, y, z;

// ...

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

如何写一个查询语句来检测这个？在前面的实例中，我们的查询语句只是用了内置QL类。对于这一个，让我们从自定义自己的类开始。我们选择一个或多个QL类进行子类化（使用extends），并定义一个特征谓词，该谓词指定快照数据库中与该类匹配的那些实体：

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

QL类type表示快照数据库中所有类型的集合，对于QL类SafeInt，我们将其子集化为以“SafeInt<”开头的类型，从而表明它们是SafeInt模板类的实例化。getUnspecifiedType()谓词用于忽略类定义和诸如const的类型标识符。

接下来，我们定义可能会导致溢出的表达式子集，大多数算术操作都会导致溢出，但不是全部；这里使用QL的instanceof操作符来定义哪些是。我们使用递归定义，因为我们需要包含诸如(x+1)/y之类的表达式，即使x/y不需要包含在内。

class PotentialOverflow extends Expr {
  PotentialOverflow() {
    (this instanceof BinaryArithmeticOperation    // match   x+y x-y x*y
       and not this instanceof DivExpr            // but not x/y
       and not this instanceof RemExpr)           //      or x%y

    or (this instanceof UnaryArithmeticOperation  // match   x++ x-- ++x --x -x
          and not this instanceof UnaryPlusExpr)  // but not +x

    // recursive definitions to capture potential overflow in
    // operands of the operations excluded above
    or this.(BinaryArithmeticOperation).getAnOperand() instanceof PotentialOverflow
    or this.(UnaryPlusExpr).getOperand() instanceof PotentialOverflow
  }
}

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

from PotentialOverflow po, SafeInt si
where po.getParent().(Call).getTarget().(Constructor).getDeclaringType() = si
select 
    po, 
    po + " may overflow before being converted to " + si

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

就像之前的示例一样，这是一个跨多个代码库的，提供了多种可操作结果的查询语句。

JavaScript重入到UAF

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

Edge定义了许多能被JavaScript调用的函数。这个模型函数阐明了漏洞的本质：

HRESULT SomeClass::vulnerableFunction(Var* args, UINT argCount, Var* retVal)
{
    // get first argument -
    // from Chakra, acquire pointer to array
    BYTE* pBuffer;
    UINT bufferSize;
    hr = Jscript::GetTypedArrayBuffer(args[1], &pBuffer, &bufferSize);

    // get second argument – 
    // from Chakra, obtain an integer value
    int someValue;
    hr = Jscript::VarToInt(args[2], &someValue);

    // perform some operation on the array acquired previously
    doSomething(pBuffer, bufferSize);

…

问题出现在Edge回调Chakra的时候，在VarToInt的过程中可以造成RCE。下面的函数可用于传递一个JavaScript对象以覆盖valueOf，以达到释放缓冲区的目的，所以当VarToInt返回值的时候，pBuffer就成了迷途指针。

var buf = new ArrayBuffer(length);
var arr = new Uint8Array(buf);

var param = {}
param.valueOf = function() {
    /* free `buf`
       (code to actually do this would be defined elsewhere) */
    neuter(buf);  // neuter `buf` by e.g. posting it to a web worker
    gc();         // trigger garbage collection
    return 0;
};

vulnerableFunction(arr, param);

因此我们在查询中寻找的具体模式应该是：从GetTypedArrayBuffer获得一个指针，然后调用一些可以执行JS的chakra函数，之后就可以使用指针了。

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

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内部用于实现这个功能的函数，并使用查询以从调用表中将其挖掘出来。

// examine call graph to match any function that may eventually call MethodCallToPrimitive
predicate mayExecJsFunction(Function f) {
    exists(Function g | f.calls+(g) and g.hasName("MethodCallToPrimitive")
    }

// this defines a call to any of the above functions
class MayExecJsCall extends FunctionCall {
    MayExecJsCall() {
        mayExecJsFunction(this)
    }
}

调用谓语后面的"+"指定了一个传递闭包 - 它将谓词应用于自身，直到匹配到为止。这可以允许对函数调用表进行一个简明的探查。

最后，查询语句和这些QL类的定义在控制流中联系到一起。

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,
    "Call to " + call + " between definition " + def + " and use " + use

getASuccessor()的谓语指定了在控制流中的下一个声明或者表达式。因此，使用例如call.getASuccessor+() = use将跟随调用的控制流图，直到匹配到use为止。如下图：

这个查询发现了原始漏洞的四个变体，都是紧急漏洞。

以上就是全部内容。下一篇文章将介绍使用QL进行数据流分析和污点追踪，以及我们对Azure固件组件的安全性审查中的示例。

源链接

Hacking more

...