深入学习CodeQL by security_lab

一、简介

github SecurityLab 上有多个CodeQL的使用例子

通过学习这些例子,我们可以加深对CodeQL的了解,以便于更好的使用它。

二、ChakraCore-bad-overflow-check

1. 漏洞模式

  • 这个例子主要是学习如何查找出错误的整数相加溢出判断逻辑。

  • 以一个例子为例

    1
    2
    3
    4
    bool checkOverflow(unsigned short x, unsigned short y) {
    // BAD: comparison is always false due to type promotion
    return (x + y < x);
    }

    这里相加后的结果由于会自动隐式转换至int类型,因此该加法操作的结果将始终不会溢出。这会使得程序无法正常判断是否存在溢出操作,而这就是漏洞所在。

  • 但在以下这个例子中

    1
    2
    3
    bool checkOverflow(unsigned short x, unsigned short y) {
    return ((unsigned short)(x + y) < x); // GOOD: explicit cast
    }

    由于相加后的结果会进行强制类型转换,因此该加法操作的结果可以产生溢出,溢出判断逻辑工作正常。

2. QL的编写

  • 首先明确目的,我们要查找出错误的检测溢出的代码,即上述中的第一个例子。

  • 因此,我们先列一下这个模式的必要条件,即通过什么条件来查找出这个漏洞

    • 需要获取符合var1 + var2 <compare> var1的语句

    • 比较操作符RelationalOperation左右两边各有一个AddExprLocalScopeVariable var1

    • 加法操作AddExpr内部所含有的一个LocalScopeVariable va1,与上面的var1是同一个。

    • 操作数 var1 的位数必须小于32位

    • 加法运算的结果不执行强制类型转换,或者强转后的大小大于32位

      这个条件会使得溢出检测算法无效,而这就是我们的目标所在。

  • 故最终的QL代码如下

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

    /** Matches `var < var + ???`. */
    predicate overflowCheck(LocalScopeVariable var, AddExpr add, RelationalOperation compare){
    /* 当前的relationalOperation,其左右两边分别是一个变量以及一个加法语句 */
    compare.getAnOperand() = var.getAnAccess() and
    compare.getAnOperand() = add and
    /* 同时这个变量还是加法语句中的一个操作数 */
    add.getAnOperand() = var.getAnAccess()
    }

    from LocalScopeVariable var, AddExpr add
    where overflowCheck(var, add, _) /* 获取可能存在溢出的点 */
    and var.getType().getSize() < 4 /* 当前的操作数大小要小于4字节 */
    and not add.getConversion+().getType().getSize() < 4 /* 限制加法的位数 >= 32 */
    select add, "Overflow check on variable of type " + var.getUnderlyingType()

    注意where语句中使用的一个通配符_,该通配符用于表示任何数据集

三、Facebook_Fizz_CVE-2019-3560

1. 漏洞模式

  • 该漏洞是一个由+=符所引起的整型溢出漏洞 - src

    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
    30
    31
    32
    33
    34
    35
    folly::Optional<TLSMessage> PlaintextReadRecordLayer::read(
    folly::IOBufQueue& buf) {
    while (true) {
    // 获取当前buf所读取到的指针位置
    folly::io::Cursor cursor(buf.front());
    // ...
    if (/* ... */) {
    if (/* ... */) {
    // ...
    // 从当前cursor指向的位置中,读取一个uint16_t
    auto length = cursor.readBE<uint16_t>();
    // 检查是否接收到足够多的数据以继续解析
    if (buf.chainLength() < (cursor - buf.front()) + length) {
    return folly::none;
    }
    // !!! 将 length执行加法操作
    length +=
    sizeof(ContentType) + sizeof(ProtocolVersion) + sizeof(uint16_t);
    // 修改buf的指针,使得下一次获取cursor时的位置移至后面
    // 详细函数见最下方
    buf.trimStart(length);
    continue;
    }
    // ...
    }
    // ...
    }
    // ...
    }

    void IOBuf::trimStart(std::size_t amount) {
    DCHECK_LE(amount, length_);
    data_ += amount;
    length_ -= amount;
    }
  • 这段代码中将会从传入的网络数据包中读取一个uint16_t,并将其传给lengthlength是攻击者可控的。同时,代码中的if语句只是用于检测是否接收到足够多的数据,并不会检测可能存在的溢出操作

  • 因此,倘若length在执行+=操作时溢出至0,那么在执行buf.trimStart函数时,buf中指向当前正在处理数据的指针将不会被修改。也就是说,在循环的下一次执行中,cursor会被设置为与当前循环相同的cursor,然后读取与当前循环相同的length,之后length继续溢出至0,buf的指针仍然没有被修改。如此循环往复,程序将陷入循环中无法跳出,这样便造成了拒绝服务攻击(DoS)。

2. QL的编写

  • 先列出这个漏洞的必要条件

    • 不受信任的输入
    • 向下的类型转换
  • 首先,我们需要确定一个不受信任的输入。在Fizz中,数据通常按照网络字节顺序来通过套接字发送,因此网络字节顺序通常需要转换为主机字节顺序,这就意味着ntohsntohl通常是不受信任输入的来源之一。但是,Fizz使用Endian类来处理字节顺序转换。因此在查询时就必须设置数据流源头为Endian类变量。

    以下是一个用于查找所有Endian::big函数声明的QL代码

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    import cpp
    import semmle.code.cpp.ir.IR

    /**
    * The endianness conversion function `Endian::big()`.
    * It is Folly's replacement for `ntohs` and `ntohl`.
    */
    class EndianConvert extends Function {
    EndianConvert() {
    this.getName() = "big" and
    this.getDeclaringType().getName().matches("Endian")
    }
    }

    from EndianConvert ec
    select ec

    因此我们可以查找出调用Endian::big函数的FunctionCall,不受信任的数据将从这个FunctionCall中流出。

    1
    2
    3
    4
    5
    6
    7
    8
    /**
    * Holds if `i` is an endianness conversion.
    * (A telltale sign of network data.)
    */
    predicate isNetworkData(Instruction i) {
    i.(CallInstruction).getCallTarget().(FunctionInstruction).getFunctionSymbol()
    instanceof EndianConvert
    }
  • 之后,我们查找从较大类型到较小类型的所有转换,这些类型转换可能会产生溢出,而我们的目标就是为了让不受信任的数据流动至此处

    ConvertInstruction类型来自于semmle.code.cpp.ir.IR,这个类型将会查找所有的类型转换。

    这里的类型转换不局限于强制类型转换和隐式类型转换,还包括if条件框中的intbool类型等等。

    所包含的数据量及其之多,因此需要进行二次过滤。

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    import cpp
    import semmle.code.cpp.ir.IR

    from
    ConvertInstruction conv,
    Type inputType,
    Type outputType
    where
    /* 转换后的类型位数必须小于原始类型 */
    conv.getResultSize() < conv.getUnary().getResultSize() and
    /* 获取初始类型 */
    inputType = conv.getUnary().getResultType() and
    /* 获取转换后类型 */
    outputType = conv.getResultType()
    select
    conv,
    "Narrowing conversion from " + inputType + " to " + outputType + "."
  • 接下来,我们便可以编写全局污点追踪查询

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    class Cfg extends TaintTracking::Configuration {
    Cfg() { this = "FizzOverflowIR" }
    /**
    * Holds if `source` is network data.
    */
    override predicate isSource(DataFlow::Node source) {
    isNetworkData(source.asInstruction())
    }

    /** Holds if `sink` is a narrowing conversion. */
    override predicate isSink(DataFlow::Node sink) {
    isNarrowingConversion(sink.asInstruction())
    }
    }
  • 将上面的代码组装起来,便是以下的完整代码

    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
    30
    31
    32
    33
    34
    35
    36
    37
    38
    39
    40
    41
    42
    43
    44
    45
    46
    47
    48
    49
    50
    51
    52
    53
    54
    55
    56
    57
    58
    59
    60
    61
    62
    63
    64
    /**
    * @name Fizz Overflow
    * @description Narrowing conversions on untrusted data could enable
    * an attacker to trigger an integer overflow.
    * @kind path-problem
    * @problem.severity warning
    */

    import cpp
    import semmle.code.cpp.ir.dataflow.TaintTracking
    import semmle.code.cpp.ir.IR
    import DataFlow::PathGraph

    /**
    * The endianness conversion function `Endian::big()`.
    * It is Folly's replacement for `ntohs` and `ntohl`.
    */
    class EndianConvert extends Function {
    EndianConvert() {
    this.getName() = "big" and
    this.getDeclaringType().getName().matches("Endian")
    }
    }

    /** Holds if `i` is a narrowing conversion. */
    predicate isNarrowingConversion(ConvertInstruction i) {
    i.getResultSize() < i.getUnary().getResultSize()
    }

    /**
    * Holds if `i` is an endianness conversion.
    * (A telltale sign of network data.)
    */
    predicate isNetworkData(Instruction i) {
    i.(CallInstruction).getCallTarget().(FunctionInstruction).getFunctionSymbol()
    instanceof EndianConvert
    }

    class Cfg extends TaintTracking::Configuration {
    Cfg() { this = "FizzOverflowIR" }

    /**
    * Holds if `source` is network data.
    */
    override predicate isSource(DataFlow::Node source) {
    isNetworkData(source.asInstruction())
    }

    /** Holds if `sink` is a narrowing conversion. */
    override predicate isSink(DataFlow::Node sink) {
    isNarrowingConversion(sink.asInstruction())
    }
    }

    from
    Cfg cfg, DataFlow::PathNode source, DataFlow::PathNode sink, ConvertInstruction conv,
    Type inputType, Type outputType
    where
    cfg.hasFlowPath(source, sink) and
    conv = sink.getNode().asInstruction() and
    inputType = conv.getUnary().getResultType() and
    outputType = conv.getResultType()
    select sink, source, sink,
    "Conversion of untrusted data from " + inputType + " to " + outputType + "."

四、libssh2_eating_error_codes

1. 漏洞模式

  • 这种漏洞模式主要是由类似于以下的代码组成

    1
    2
    3
    4
    5
    int _libssh2_get_c_string(...){ /* ... */}

    unsigned int p_len;
    if((p_len = _libssh2_get_c_string(&buf, &p)) < 0)
    //...

    其中,_libssh2_get_c_string函数返回的是一个带符号的整型,但接收返回值的变量是无符号的。因此该漏洞将会使函数内部产生的error code(-1)被忽略

2. QL的编写

  • 首先,我们不使用污点分析技术来尝试查询到这些错误。

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    import cpp

    from FunctionCall call, ReturnStmt ret
    where
    /* 返回语句的返回值限定在负数 */
    ret.getExpr().getValue().toInt() < 0 and
    /* 查找一个函数调用,这个函数调用将会调用 那些可能会返回-1的函数 */
    call.getTarget() = ret.getEnclosingFunction() and
    /* 限定函数调用的返回值被类型转换为无符号整数 */
    call.getFullyConverted().getType().getUnderlyingType().(IntegralType).isUnsigned()
    select call, ret

    可以查询出一部分错误点。

  • 但上面的查询代码并不能很好的找到下面这种类型的错误

    1
    2
    int r = f();
    unsigned int x = r;

    因此我们要试着使用一下数据流分析技术,查询从FunctionCall流出的数据(即返回值)到最近一个无符号类型转换的路径。

    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    import cpp
    import semmle.code.cpp.dataflow.DataFlow

    from FunctionCall call, ReturnStmt ret, DataFlow::Node source, DataFlow::Node sink
    where
    ret.getExpr().getValue().toInt() < 0 and
    call.getTarget() = ret.getEnclosingFunction() and
    /* 数据流源头被设置为FunctionCall位置 */
    source.asExpr() = call and
    /* 数据流终点被设置为存在类型转换的位置 */
    sink.asExpr().getFullyConverted().getType().getUnderlyingType().(IntegralType).isUnsigned() and
    DataFlow::localFlow(source, sink)
    select source, sink
  • 版权声明: 本博客所有文章除特别声明外,著作权归作者所有。转载请注明出处!
  • Copyrights © 2020-2021 Kiprey
  • 访问人数: | 浏览次数:

请我喝杯奶茶吧~