深入学习CodeQL by security_lab

天问之路
字数统计: 2.2k   |   阅读时长≈ 9 分钟

一、简介

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左右两边各有一个AddExpr和LocalScopeVariable 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，并将其传给length。即length是攻击者可控的。同时，代码中的if语句只是用于检测是否接收到足够多的数据，并不会检测可能存在的溢出操作。

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

2. QL的编写

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

    • 不受信任的输入
    • 向下的类型转换

  • 首先，我们需要确定一个不受信任的输入。在Fizz中，数据通常按照网络字节顺序来通过套接字发送，因此网络字节顺序通常需要转换为主机字节顺序，这就意味着ntohs和ntohl通常是不受信任输入的来源之一。但是，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条件框中的int转bool类型等等。

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

    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-2024 Kiprey
  • 访问人数: | 浏览次数:

请我喝杯咖啡吧~