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

鲁班七号 技术 2018年8月21日发布

导语:在这篇文章之前,我们曾讨论过MSRC是如何自动化的对发现的漏洞进行原因分析并形成报告的。而在完成此操作后,我们的下一步是变体分析:查找和调查漏洞的任何变体。事实上这也是最为重要的一点,即找到所有这些变体并同时修补它们,否则我

在这篇文章之前,我们曾讨论过MSRC是如何自动化的对发现的漏洞进行原因分析并形成报告的。而在完成此操作后,我们的下一步是变体分析:查找和调查漏洞的任何变体。事实上这也是最为重要的一点,即找到所有这些变体并同时修补它们,否则我们就要承担其在野外被利用的风险。在这篇文章中,我想阐述的其实就是如何自动化的发现这些漏洞的变体。

在过去一年左右的时间里,我们一直在使用第三方静态分析环境Semmle来扩充我们的手动代码审查流程。它将代码编译到关系数据库(快照数据库 – 数据库和源代码的组合),使用Semmle QL查询,Semmle QL是一种用于程序分析的声明式的面向对象的查询语言。

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

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

整数溢出检查不正确

第一种情况是一个直接定义的错误,但在大型代码库中找到变体会很繁琐。

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

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

不幸的是,当整数类型的宽度足够小需要进行整体提升时,它就不能正常工作了。例如,如果x和y都是无符号short,则在编译时,上面的代码最终将等同于(unsigned int)x + y <x,这使得溢出检查无效。

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

importcpp
fromAddExpr a, Variable v, RelationalOperation r
wherea.getAnOperand() = v.getAnAccess()
  andr.getAnOperand() = v.getAnAccess()
  andr.getAnOperand() = a
   and forall(Expr op | op = a.getAnOperand() | op.getType().getSize() < 4)
  and nota.getExplicitlyConverted().getType().getSize() < 4
selectr, "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位就不重要了:

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

(这样的检查就像(无符号short)(x + y)<x不会被查询标记。)

最后,select子句就会定义结果集。

此漏洞最初在Chakra(Edge的JavaScript引擎)中被报告,其中特定无效溢出检查的结果是内存损坏。该查询与原始漏洞匹配,但在Chakra中没有其他变体。但是,我们在将此确切查询应用于其他Windows组件时发现了几个变体。

不安全地使用SafeInt

滚动自己的整数溢出检查的另一种方法是使用内置此类检查的库.SafeInt是一个C ++模板类,它覆盖算术运算符以抛出检测到溢出的异常。

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

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

 1.png

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

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

 2.png

如何编写查询来检测这个?在前面的示例中,我们的查询仅使用了内置的QL类。那么对于这个,让我们重新来定义我们的开始。为此,我们从(使用extends)中选择一个或多个QL类进行子类化,并定义一个特征谓词,该谓词指定快照数据库中与该类匹配的那些实体:

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不是。

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的重新使用到免费使用

下一个示例是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期间,可以执行任意JavaScript代码。上面的函数可以通过传递一个覆盖valueOf的JavaScript对象来释放缓冲区来利用,所以当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);

因此,我们在QL中寻找的特定模式是:从GetTypedArrayBuffer获取指针,然后调用可能执行JavaScript的Chakra函数,然后使用指针。

对于数组缓冲区指针,我们匹配对GetTypedArrayBuffer的调用,其中第二个参数(Call的getArgument为零索引)是表达式(&)的地址,并取其操作数:

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

这里使用存在的逻辑量词来将新变量(c)引入范围。

有几个Chakra API函数可用于JavaScript重入。我们可以识别执行此任务的内部Chakra函数,而不是通过名称定义它们,并使用QL从调用图中计算出来:

// 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将跟随调用的控制流图,直到有匹配使用。下图说明了这一点:

 3.png

 

除了最初报告的漏洞之外,此查询还发现了四个变体,所有这些变体都被评估为严重程度。好了,本篇就到此为止了。下一部分将介绍使用QL进行数据流分析和污点跟踪,以及我们对Azure固件组件的安全性审查中的示例。

本文翻译自: https://blogs.technet.microsoft.com/srd/2018/08/16/vulnerability-hunting-with-semmle-ql-part-1/如若转载,请注明原文地址: http://www.4hou.com/technology/13154.html
点赞 0
  • 分享至
取消

感谢您的支持,我会继续努力的!

扫码支持

打开微信扫一扫后点击右上角即可分享哟

发表评论