CodeQL學習——CodeQl數據流分析


數據流程圖

CodeQL數據流庫通過對程序或功能的數據流圖進行建模來實現對程序或功能的數據流分析。抽象語法樹不同,數據流圖不反映程序的語法結構,而是在運行時對數據流過程序的方式進行建模。抽象語法樹中的節點代表語法元素,例如語句或表達式。另一方面,數據流圖中的節點表示在運行時帶有值的語義元素。

一些AST節點(例如表達式)具有相應的數據流節點,而其他AST節點(例如if語句)則沒有。這是因為表達式在運行時被評估為一個值,而 if語句純粹是一個控制流構造,並且不攜帶值。還有一些數據流節點根本不與AST節點相對應。

數據流圖中的邊緣表示程序元素之間數據流的方式。例如,在表達式中,存在與子表達式相對應的數據流節點,以及與整個表達式相對應的數據流節點從對應於的節點到對應於的節點之間存在一條邊,表示數據可能從流動(因為表達式可以求值為)。同樣,從對應的節點到對應於的節點都有一條邊|| yxy|| yx|| yx|| y|| yxy|| y

本地數據流和全局數據流在考慮的邊緣方面有所不同:本地數據流僅考慮屬於同一功能的數據流節點之間的邊緣,而忽略功能之間以及通過對象屬性的數據流。但是,全局數據流也要考慮后者。污染跟蹤將其他邊沿引入數據流圖中,這些邊並不精確地對應於值流,而是模擬運行時某個值是否可以從另一個值中導出,例如通過字符串操作。

使用計算數據流圖,以對表示圖節點的程序元素進行建模。節點之間的數據流使用謂詞建模以計算圖的邊緣。

計算准確而完整的數據流圖提出了若干挑戰:

  • 無法通過源代碼不可用的標准庫函數來計算數據流。
  • 直到運行時才能確定某些行為,這意味着數據流庫必須采取額外的步驟來找到潛在的調用目標。
  • 變量之間的混淆會導致一次寫入更改多個指針指向的值。
  • 數據流圖可能很大,計算起來很慢。

為了克服這些潛在的問題,庫中對兩種數據流進行了建模:

  • 本地數據流,涉及單個功能內的數據流。在推理本地數據流時,僅考慮屬於同一功能的數據流節點之間的邊。通常,它對於許多查詢而言足夠快速,高效且精確,並且通常可以為CodeQL數據庫中的所有功能計算本地數據流。
  • 全局數據流通過計算函數之間以及對象屬性之間的數據流,有效地考慮了整個程序中的數據流。與本地數據流相比,計算全局數據流通常需要更多的時間和精力,因此應優化查詢以查找更具體的源和匯。

許多CodeQL查詢都包含本地和全局數據流分析的示例。有關詳細信息,請參見內置查詢

正常數據流與污點跟蹤

在標准庫中,我們對“正常”數據流和污點跟蹤進行了區分。常規數據流庫用於分析每個步驟中數據值都被保留的信息流。

例如,如果您要跟蹤不安全的對象x(可能是一些不受信任的或潛在的惡意數據),則程序中的某個步驟可能會“更改”其值。因此,在諸如y=x+1這樣的簡單過程中,正常的數據流分析將突出顯示x,但不突出顯示y但是,由於y是從x派生的,因此受不受信任或“污染”的信息的影響,因此也會被污染。分析污點從x到y的流動稱為污點跟蹤。

在QL中,污點跟蹤通過包括以下步驟來擴展數據流分析,在這些步驟中不必保留數據值,但仍會傳播潛在的不安全對象。這些流程步驟在污點跟蹤庫中使用謂詞進行建模,這些謂詞用於確定污點是否在節點之間傳播。

在Java中分析數據流

我們可以使用CodeQL跟蹤Java程序數據流。

本地數據流

本地數據流是指單個方法或者可調用方法內的數據流,通常比全局數據流有着更容易、更快和更准確的優點,對於許多查詢來說是足夠的了。

使用本地數據流

本地數據流庫位於DataFlow模塊中,該模塊定義了Node類表示數據可以流經的任何元素Node分為表達式節點(ExprNode)和參數節點(ParameterNode)。我們可以使用成員謂詞asExprasParameter在數據流節點和表達式/參數之間進行映射

class Node {
  /** Gets the expression corresponding to this node, if any. */
  Expr asExpr() { ... }

  /** Gets the parameter corresponding to this node, if any. */
  Parameter asParameter() { ... }

  ...
}

或使用謂詞exprNodeparameterNode

/**
 * Gets the node corresponding to expression `e`.
 */
ExprNode exprNode(Expr e) { ... }

/**
 * Gets the node corresponding to the value of parameter `p` at function entry.
 */
ParameterNode parameterNode(Parameter p) { ... }

如果從節點nodeFrom到節點nodeTo之間存在直連的數據流邊線,則謂詞localFlowStep(Node nodeFrom, Node nodeTo)成立我們可以使用+*運算符,也可以使用預定義的遞歸謂詞localFlow(等效於localFlowStep*)來遞歸地應用謂詞

例如,我們可以在0個或多個本地數據流步驟中找到從參數source到表達式sink的流

DataFlow::localFlow(DataFlow::parameterNode(source), DataFlow::exprNode(sink))

使用本地污點跟蹤

本地污點跟蹤通過包含非保留值的流程步驟來擴展本地數據流。例如:

String temp = x; String y = temp + ", " + temp; 

如果x是受污染的字符串,則y也受污染。

本地污染跟蹤庫位於TaintTracking模塊中像本地數據流一樣,如果從nodeFrom 節點到nodeTo節點之間存在直接的污點傳播邊線,則謂詞localTaintStep(DataFlow::Node nodeFrom, DataFlow::Node nodeTo)成立您可以使用+和*運算符,也可以使用預定義的遞歸謂詞localTaint(等效於localTaintStep*)來遞歸地應用謂詞

例如,我們可以在0個或多個本地數據流步驟中查找從參數source到表達式sink污染流

TaintTracking::localTaint(DataFlow::parameterNode(source), DataFlow::exprNode(sink))

例子

這個查詢查找傳遞給new FileReader(..)的文件名

import java

from Constructor fileReader, Call call
where
  fileReader.getDeclaringType().hasQualifiedName("java.io", "FileReader") and
  call.getCallee() = fileReader
select call.getArgument(0)

但是,這只是給出參數的表達式,而不是可能傳遞給它的值。因此,我們需要使用本地數據流查找流入該參數的所有表達式:

import java
import semmle.code.java.dataflow.DataFlow

from Constructor fileReader, Call call, Expr src
where
  fileReader.getDeclaringType().hasQualifiedName("java.io", "FileReader") and
  call.getCallee() = fileReader and
  DataFlow::localFlow(DataFlow::exprNode(src), DataFlow::exprNode(call.getArgument(0)))
select src

然后,我們可以使source 更加具體,例如對公共參數的訪問。以下查詢查找將公共參數傳遞到new FileReader(..)的位置:

import java
import semmle.code.java.dataflow.DataFlow

from Constructor fileReader, Call call, Parameter p
where
  fileReader.getDeclaringType().hasQualifiedName("java.io", "FileReader") and
  call.getCallee() = fileReader and
  DataFlow::localFlow(DataFlow::parameterNode(p), DataFlow::exprNode(call.getArgument(0)))
select p

下述查詢用於查找對格式化字符串未進行硬編碼的格式化函數的調用。

import java
import semmle.code.java.dataflow.DataFlow
import semmle.code.java.StringFormat

from StringFormatMethod format, MethodAccess call, Expr formatString
where
  call.getMethod() = format and
  call.getArgument(format.getFormatStringIndex()) = formatString and
  not exists(DataFlow::Node source, DataFlow::Node sink |
    DataFlow::localFlow(source, sink) and
    source.asExpr() instanceof StringLiteral and
    sink.asExpr() = formatString
  )
select call, "Argument to String format method isn't hard-coded."

練習

練習1:編寫一個查詢,該查詢使用本地數據流查找用於創建java.net.URL的所有硬編碼字符串回答

全局數據流

全局數據流跟蹤整個程序中的數據流,因此比本地數據流更強大。但是,全局數據流不如本地數據流精確,並且分析通常需要大量時間和內存才能執行。

使用全局數據流

您可以通過擴展類DataFlow::Configuration來使用全局數據流庫

import semmle.code.java.dataflow.DataFlow

class MyDataFlowConfiguration extends DataFlow::Configuration {
  MyDataFlowConfiguration() { this = "MyDataFlowConfiguration" }

  override predicate isSource(DataFlow::Node source) {
    ...
  }

  override predicate isSink(DataFlow::Node sink) {
    ...
  }
}

這些謂詞在配置中定義:

  • isSource-定義數據可能來源
  • isSink-定義數據可能流向的位置
  • isBarrier—可選,限制數據流
  • isAdditionalFlowStep—可選,添加額外的數據流步驟

特征謂詞MyDataFlowConfiguration()定義了配置的名稱,因此"MyDataFlowConfiguration"應該是個唯一的名稱,例如類的名稱。

使用謂詞hasFlow(DataFlow::Node source, DataFlow::Node sink)執行數據流分析

from MyDataFlowConfiguration dataflow, DataFlow::Node source, DataFlow::Node sink
where dataflow.hasFlow(source, sink)
select source, "Data flow to $@.", sink, sink.toString()

使用全局污點跟蹤

全局污點跟蹤是針對全局數據流而言,就像本地污點跟蹤是針對本地數據流一樣。也就是說,全局污點跟蹤通過額外的non-value-preserving步驟擴展了全局數據流。我們可以通過擴展類TaintTracking::Configuration來使用全局污點跟蹤庫

import semmle.code.java.dataflow.TaintTracking

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

  override predicate isSource(DataFlow::Node source) {
    ...
  }

  override predicate isSink(DataFlow::Node sink) {
    ...
  }
}

這些謂詞在配置中定義:

  • isSource-定義污點的可能來源
  • isSink-定義污點可能流向的位置  
  • isSanitizer—可選,限制污點流
  • isAdditionalTaintStep—可選,添加額外污點步驟

與全局數據流相似,特征謂詞MyTaintTrackingConfiguration()定義配置的唯一名稱。

污點跟蹤分析是使用謂詞hasFlow(DataFlow::Node source, DataFlow::Node sink)執行的

流sources

數據流庫包含一些預定義的流sources。RemoteFlowSource(在semmle.code.java.dataflow.FlowSources中定義)表示可由遠程用戶控制的數據流source ,這對於發現安全性問題很有用。

例子

下述查詢展示了使用遠程用戶輸入作為數據源的污點跟蹤配置。

import java
import semmle.code.java.dataflow.FlowSources

class MyTaintTrackingConfiguration extends TaintTracking::Configuration {
  MyTaintTrackingConfiguration() {
    this = "..."
  }

  override predicate isSource(DataFlow::Node source) {
    source instanceof RemoteFlowSource
  }

  ...
}

 

練習

練習2:編寫使用全局數據流查找用於創建java.net.URL的所有硬編碼字符串的查詢回答

練習3:編寫一個代表數據流源來自】java.lang.System.getenv(..)的類回答

練習4:使用2和3的答案,編寫查詢以查找從getenvjava.net.URL所有全局數據流回答

答案

練習

import semmle.code.java.dataflow.DataFlow

from Constructor url, Call call, StringLiteral src
where
  url.getDeclaringType().hasQualifiedName("java.net", "URL") and
  call.getCallee() = url and
  DataFlow::localFlow(DataFlow::exprNode(src), DataFlow::exprNode(call.getArgument(0)))
select src

練習

import semmle.code.java.dataflow.DataFlow

class Configuration extends DataFlow::Configuration {
  Configuration() {
    this = "LiteralToURL Configuration"
  }

  override predicate isSource(DataFlow::Node source) {
    source.asExpr() instanceof StringLiteral
  }

  override predicate isSink(DataFlow::Node sink) {
    exists(Call call |
      sink.asExpr() = call.getArgument(0) and
      call.getCallee().(Constructor).getDeclaringType().hasQualifiedName("java.net", "URL")
    )
  }
}

from DataFlow::Node src, DataFlow::Node sink, Configuration config
where config.hasFlow(src, sink)
select src, "This string constructs a URL $@.", sink, "here"

練習

import java

class GetenvSource extends MethodAccess {
  GetenvSource() {
    exists(Method m | m = this.getMethod() |
      m.hasName("getenv") and
      m.getDeclaringType() instanceof TypeSystem
    )
  }
}

練習

import semmle.code.java.dataflow.DataFlow

class GetenvSource extends DataFlow::ExprNode {
  GetenvSource() {
    exists(Method m | m = this.asExpr().(MethodAccess).getMethod() |
      m.hasName("getenv") and
      m.getDeclaringType() instanceof TypeSystem
    )
  }
}

class GetenvToURLConfiguration extends DataFlow::Configuration {
  GetenvToURLConfiguration() {
    this = "GetenvToURLConfiguration"
  }

  override predicate isSource(DataFlow::Node source) {
    source instanceof GetenvSource
  }

  override predicate isSink(DataFlow::Node sink) {
    exists(Call call |
      sink.asExpr() = call.getArgument(0) and
      call.getCallee().(Constructor).getDeclaringType().hasQualifiedName("java.net", "URL")
    )
  }
}

from DataFlow::Node src, DataFlow::Node sink, GetenvToURLConfiguration config
where config.hasFlow(src, sink)
select src, "This environment variable constructs a URL $@.", sink, "here"

 


免責聲明!

本站轉載的文章為個人學習借鑒使用,本站對版權不負任何法律責任。如果侵犯了您的隱私權益,請聯系本站郵箱yoyou2525@163.com刪除。



 
粵ICP備18138465號   © 2018-2025 CODEPRJ.COM