使用Semmle QL進行漏洞探索 Part2

安全漏洞 · 發表 2019-03-27 14:32:26

摘要：前言本系列的第一部分介紹了 Semmle QL ，以及Microsoft安全響應中心（MSRC）如何使用它來稽核向我們報告的漏洞。這篇文章討論了一個我們如何主動使用它的例子，包括Azure韌體元件的安全審計。這是Azure服務深度安全審查的更廣泛防禦的一部分，從假...

前言

本系列的第一部分介紹了 Semmle QL ，以及Microsoft安全響應中心（MSRC）如何使用它來稽核向我們報告的漏洞。這篇文章討論了一個我們如何主動使用它的例子，包括Azure韌體元件的安全審計。

這是Azure服務深度安全審查的更廣泛防禦的一部分，從假設對手的角度探索攻擊向量，該對手已經滲透了至少一個安全邊界，現在位於服務後端的操作環境中（在下圖中用*標記）。

本次審查的目標之一是基於Linux的嵌入式裝置，它與服務後端和管理後端相連線，在兩者之間傳遞操作資料。該裝置的主要攻擊面是兩個介面上使用的管理協議。

對其韌體的初步手動審查表明，該管理協議是基於訊息的，有400多種不同的訊息型別，每種型別都有自己的處理程式功能。手動審計每一個函式都是乏味且容易出錯的，所以使用Semmle來擴充套件我們的程式碼審查能力是一個簡單的選擇。我們使用本文中討論的靜態分析技術，總共發現了33個易受攻擊的訊息處理函式。

定義攻擊面

我們的第一步是編寫一些QL來模擬來自攻擊者的資料。管理協議以請求-響應為基礎工作，其中每個訊息請求型別都用類別號和命令號來標識。這是在原始碼中使用如下結構陣列定義的，例如：

MessageCategoryTable g_MessageCategoryTable[] =
{
{ CMD_CATEGORY_BASE,g_CommandHandlers_Base },
{ CMD_CATEGORY_APP0,g_CommandHandlers_App0 },
…
{ NULL,NULL}
};
CommandHandlerTable g_CommandHandlers_Base [] =
{
{ CMD_GET_COMPONENT_VER,sizeof(ComponentVerReq),GetComponentVer,… },
{ CMD_GET_GLOBAL_CONFIG,-1,GetGlobalConfig,… },
…
{ NULL,NULL,NULL,… }
};

在上面的示例中，類別型別為 CMD_CATEGORY_BASE 、命令型別為 CMD_GET_COMPONENT_VER 的訊息將被路由到 GetComponentVer 函式。命令處理程式表具有關於請求訊息的預期大小的資訊，該資訊在呼叫處理函式之前在訊息排程例程中得到驗證。

我們使用以下QL定義了訊息處理程式表：

class CommandHandlerTable extends Variable { 
CommandHandlerTable() { 
exists(Variable v | v.hasName("g_MessageCategoryTable")
and this.getAnAccess() = v.getInitializer().getExpr().getAChild().getChild(1)
) 
} 
}

這需要一個名為 g_MessageCategoryTable 的變數，找到它的初始化表示式，並匹配該表示式的所有子表示式——每個子表示式對應於訊息類別表的一行。對於每一行，它採用第二列(這是 getChild(1) ，因為getChild的引數是零索引的)，每一列都是對命令處理程式表的引用，並匹配引用的變數。在上面的例子中，它們是 g_CommandHandlers_Base 和 g_CommandHandlers_App0 。

我們使用類似的方法定義了訊息處理函式集：

class MessageHandlerFunction extends Function { 
Expr tableEntry; 

MessageHandlerFunction() { 
exists(CommandHandlerTable table |
tableEntry = table.getInitializer().getExpr().getAChild()
)
and this = tableEntry.getChild(2).(FunctionAccess).getTarget()
}

int getExpectedRequestLength() { 
result = tableEntry.getChild(1).getValue().toInt() 
} 
…
}

這個QL類使用成員變數 tableEntry 來儲存所有命令處理程式表中所有行的集合。這就是為什麼它可以在（ messageHandlerffunction ( ) {…} )和 getExpectedRequestLength ( ) 中引用，而無需重複定義。

所有這些都對映到上面的程式碼結構，如下所示：

每個訊息處理函式都有相同的簽名：

typedef unsigned char UINT8;
int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse);

並遵循一種通用模式，其中請求資料被轉換為表示訊息佈局的結構型別，並通過其欄位進行訪問：

int ExampleMessageHandler(UINT8 *pRequest, int RequestLength, UINT8 *pResponse)
{
ExampleMessageRequest* pMsgReq = (ExampleMessageRequest *)pRequest;
…
someFunction(pMsgReq->aaa.bbb)
…
}

在這個分析中，我們只對請求資料感興趣。我們在MessageHandlerFunction QL類中定義了兩個額外的謂詞來對請求資料及其長度進行建模：

class MessageHandlerFunction extends Function {
Expr tableEntry;
…

Parameter getRequestDataPointer() {
result = this.getParameter(0)
}

Parameter getRequestLength() {
result = this.getParameter(1)
}
}

抽象出訊息處理函式的定義，它可以像任何其他QL類一樣使用。例如，該查詢按照迴圈複雜性的降序列出了所有訊息處理程式函式：

from MessageHandlerFunction mhf
select
mhf, 
mhf.getADeclarationEntry().getCyclomaticComplexity() as cc
order by cc desc

分析資料流

既然我們已經為不可信資料定義了一組入口點，下一步就是找到它可能以不安全的方式被使用的地方。為此，我們需要通過程式碼庫跟蹤這些資料流。QL提供了一個強大的全域性資料流庫，它抽象出了大部分複雜的語言細節。

DataFlow 庫通過以下方式被納入查詢範圍：

import semmle.code.cpp.dataflow.DataFlow

它通過子類化 DataFlow::Configuration 和覆蓋謂詞來定義資料流，就像它應用於 DataFlow::Node 一樣，這是一個QL類，表示資料可以流過的任何程式假象：

配置謂詞	描述
`isSource(source)`	資料必須來自 source
`isSink(sink)`	資料必須流入 sink
`isAdditionalFlowStep(node1, node2)`	資料也可以在 node1 和 node2 之間流動
`isBarrier(node)`	資料無法通過 node 流動

大多數資料流查詢將如下所示：

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

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

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

override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2) { 
…
}

override predicate isBarrier(DataFlow::Node node) { 
…
}

}
from DataFlow::Node source, DataFlow::Node sink 
where any(RequestDataFlowConfiguration c).hasFlow(source, sink) 
select 
"Data flow from $@ to $@", 
source, sink

請注意，QL資料流庫執行過程間分析——除了檢查函式本地的資料流，它還將包括通過函式呼叫引數的資料。這是我們安全審查的一個基本特性，因為儘管下面討論的易受攻擊的程式碼模式在簡單的示例函式中顯示以便於演示，但是在我們目標的實際原始碼中，大多數結果都有跨越多個複雜函式的資料流。

發現記憶體安全漏洞

由於這個韌體元件是純C程式碼庫，我們首先決定搜尋與記憶體安全相關的程式碼模式。

這種錯誤的一個常見來源是不執行邊界檢查的陣列索引。單獨搜尋這種模式將提供很大一部分結果，這些結果很可能不是安全漏洞，因為我們真正感興趣的是攻擊者對索引值的控制。因此，在這種情況下，我們在尋找資料流，其中接收器是陣列索引表示式，源是訊息處理函式的請求資料，並且任何資料流節點都有一個由相關邊界檢查保護的屏障。

例如，我們想要找到匹配程式碼的資料流，如下所示：

int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
ExampleMessageRequest* pMsgReq(3) = (ExampleMessageRequest *) pRequest(2);
int index1(6) = pMsgReq(4)->index1(5);
pTable1[index1(7:sink)].field1 = pMsgReq->value1;
}

但我們也希望排除程式碼的資料流，如下所示：

int ExampleMessageHandler(UINT8 *pRequest(1:source), int RequestLength, UINT8 *pResponse)
{
ExampleMessageRequest* pMsgReq(3) = (ExampleMessageRequest *) pRequest(2);
int index2(6) = pMsgReq(4)->index2(5);
if (index2 >= 0 && index2 < PTABLE_SIZE)
{
pTable2[index2].field1 = pMsgReq->value2;
}
}

源是使用前面討論的 MessageHandlerFunction 類定義的，我們可以使用 ArrayExpr 的 getArrayOffset 謂詞來定義合適的接收器：

override predicate isSource(DataFlow::Node source) {
any(MessageHandlerFunction mhf).getRequestDataPointer() = source.asParameter()
}

override predicate isSink(DataFlow::Node sink) { 
exists(ArrayExpr ae | ae.getArrayOffset() = sink.asExpr())
}

預設情況下，資料流庫只包括在每個節點保留值的流，如函式呼叫引數、賦值表示式等。但是我們也需要資料從請求資料指標流向它被轉換到的結構的欄位。我們將這樣做：

override predicate isAdditionalFlowStep(DataFlow::Node node1, DataFlow::Node node2)
{
// any terminal field access on request packet
//e.g. in expression a->b.c the data flows from a to c
exists(Expr e, FieldAccess fa |
node1.asExpr() = e and node2.asExpr() = fa |
fa.getQualifier*() = e and not (fa.getParent() instanceof FieldAccess)
)
}

要使用邊界檢查排除流，我們在控制流圖中較早的某些條件語句中使用變數或欄位的任何節點上放置一個屏障（目前，我們假設任何這樣的邊界檢查都是正確完成的）：

override predicate isBarrier(DataFlow::Node node) { 
exists(ConditionalStmt condstmt |
// dataflow node variable is used in expression of conditional statement
//this includes fields (because FieldAccess extends VariableAccess)
node.asExpr().(VariableAccess).getTarget().getAnAccess()
= condstmt.getControllingExpr().getAChild*()
// and that statement precedes the dataflow node in the control flow graph
and condstmt.getASuccessor+() = node.asExpr()
// and the dataflow node itself not part of the conditional statement expression
and not (node.asExpr() = cs.getControllingExpr().getAChild*())
) 
}

將此應用於以上兩個示例，通過每個節點的資料流將是：

在我們的韌體程式碼庫中，此查詢在15個訊息處理程式函式中共定位了18個漏洞，這是攻擊者控制的越界讀寫的混合。

我們應用了類似的分析來查詢函式呼叫的引數，而不首先驗證訊息請求資料。首先，我們定義了一個QL類來定義感興趣的函式呼叫和引數，包括呼叫 memcpy 的 大小 引數和類似的函式 _fmemcpy ，以及 CalculateChecksum 的 長度 引數。 alculateChecksum 是一個特定於此程式碼庫的函式，它將返回緩衝區的CRC32，並且可能被用作資訊公開原語，訊息處理函式將這個值複製到它的響應緩衝區中。

class ArgumentMustBeCheckedFunctionCall extends FunctionCall {
int argToCheck;

ArgumentMustBeCheckedFunctionCall() {
( this.getTarget().hasName("memcpy")and argToCheck = 2 ) or
( this.getTarget().hasName("_fmemcpy")and argToCheck = 2 ) or
( this.getTarget().hasName("CalculateChecksum") and argToCheck = 1 )
}
Expr getArgumentToCheck() { result = this.getArgument(argToCheck) }
}

接下來，我們修改了上一個查詢的接收器，以匹配 argumentMustBecheckedFunctioncall 而不是陣列索引：

override predicate isSink(DataFlow::Node sink) {
// sink node is an argument to a function call that must be checked first
exists (ArgumentMustBeCheckedFunctionCall fc | 
fc.getArgumentToCheck() = sink.asExpr())
}

該查詢揭示了13個訊息處理程式中的另外17個漏洞，大部分是攻擊者控制的越界讀取（我們後來確認在響應訊息中披露了這一點），其中一個是越界寫入。

汙點跟蹤

在上面的查詢中，我們重寫了 DataFlow 庫的 isAdditionalFlowStep 謂詞，以確保當資料流向一個結構指標時，該結構的欄位將作為節點新增到資料流圖中。我們這樣做是因為預設情況下，資料流分析僅包括資料值未經修改的路徑，但我們希望跟蹤它可能也受影響的特定表示式集。也就是說，我們定義了一組被不受信任的資料汙染的特定表示式。

QL包含一個內建庫，可以應用更通用的方法來進行汙點跟蹤。它在 DataFlow 庫之上開發，會覆蓋 isAdditionalFlowStep， 併為值修改表示式提供更豐富的規則集。這是 TaintTracking 庫，它以類似於 DataFlow的 方式匯入：

import semmle.code.cpp.dataflow.TaintTracking

它的使用方式與資料流庫幾乎相同，只是要擴充套件的QL類是 TaintTracking :: Configuration ，配置謂詞如下：

配置謂詞	描述
`isSource(source)`	資料必須來自 source
`isSink(sink)`	資料必須流入 sink
`isAdditionalTaintStep(node1, node2)`	node1上的資料也會汙染 node2
`isSanitizer(node)`	資料無法通過 node 流動

我們重新運行了先前的查詢，刪除了 isAdditionalFlowStep （因為我們不再需要定義它）並且將 isBarrier 重新命名為 isSanitizer 。正如預期的那樣，它返回了上面提到的所有結果，但也在陣列索引中發現了一些額外的整數下溢缺陷。例如：

intExampleMessageHandler（UINT8 * pRequest （1：source），intRequestLength，UINT8 * pResponse）
{ 
ExampleMessageRequest * pMsgReq （3）=（ExampleMessageRequest *）pRequest （2） ; 
intindex1 （6）= pMsgReq （4） - > index1 （5） ;
pTable1 [ （ index1 （7）- 2 ）（8：sink） ]。field1 = pMsgReq-> value1; 
}

對於每種漏洞型別的內部報告，我們希望將它們與之前的查詢結果分開進行分類。這包括使用 SubExpr QL類對接收器進行簡單修改：

override predicate isSink(DataFlow::Node sink) {
// this sink is the left operand of a subtraction expression,
// 是陣列偏移表示式的一部分，例如[x - 1]中的x 
exists(ArrayExpr ae, SubExpr s | sink.asExpr() instanceof FieldAccess
and ae.getArrayOffset().getAChild*() = s
and s.getLeftOperand().getAChild*() = sink.asExpr())
}

使我們在2個訊息處理函式中增加了3個漏洞。

查詢路徑遍歷漏洞

為了找到潛在的路徑遍歷漏洞，我們使用QL來嘗試識別在檔案開啟函式中使用攻擊者控制的檔名的訊息處理函式。

這次，我們使用了一種稍微不同的方法來跟蹤汙點，定義了一些額外的汙點步驟，這些步驟將流經各種字串處理的C庫函式：

predicate isTaintedString(Expr expSrc, Expr expDest) {
exists(FunctionCall fc, Function f |
expSrc = fc.getArgument(1) and 
expDest = fc.getArgument(0) and
f = fc.getTarget() and (
f.hasName("memcpy") or 
f.hasName("_fmemcpy") or 
f.hasName("memmove") or 
f.hasName("strcpy") or 
f.hasName("strncpy") or
f.hasName("strcat") or
f.hasName("strncat")
)
)
or exists(FunctionCall fc, Function f, int n |
expSrc = fc.getArgument(n) and 
expDest = fc.getArgument(0) and
f = fc.getTarget() and (
(f.hasName("sprintf") and n >= 1) or 
(f.hasName("snprintf") and n >= 2)
)
)
}
…

override predicate isAdditionalTaintStep(DataFlow::Node node1, DataFlow::Node node2) {
isTaintedString(node1.asExpr(), node2.asExpr())
}

並將接收器定義為檔案開啟函式的路徑引數：

class FileOpenFunction extends Function {
FileOpenFunction() {
this.hasName("fopen") or this.hasName("open")
}
int getPathParameter() { result = 0 } // filename parameter index
}

…

override predicate isSink(DataFlow::Node sink) {
exists(FunctionCall fc, FileOpenFunction fof |
fc.getTarget() = fof and fc.getArgument(fof.getPathParameter()) = sink.asExpr())
}

通過對我們的目標裝置如何工作的一些預先了解，從最初的回顧中觀察到，在我們解決下一個排除資料驗證流程的問題之前，我們預計至少會有一些結果，就像之前的查詢一樣。但是，查詢根本沒有返回任何內容。

由於沒有要檢查的資料流路徑，我們回過頭來查詢函式呼叫圖，以搜尋訊息處理函式和呼叫檔案開啟函式之間的任何路徑，不包括path引數為常量的呼叫:

// this recursive predicate defines a function call graph
predicate mayCallFunction(Function caller, FunctionCall fc) {
fc.getEnclosingFunction() = caller or mayCallFunction(fc.getTarget(), fc)
}

from MessageHandlerFunction mhf, FunctionCall fc, FileOpenFunction fof
where mayCallFunction(mhf, fc)
and fc.getTarget() = fof
and not fc.getArgument(fof.getPathParameter()).isConstant()
select 
mhf, "$@ may have a path to $@",
mhf, mhf.toString(),
fc, fc.toString()

該查詢提供了5個結果——足夠少，可以手動檢查——由此我們發現了2個路徑遍歷漏洞，一個寫入檔案，另一個讀取檔案，這兩個漏洞都是攻擊者提供的路徑。事實證明，汙點跟蹤沒有標記這些，因為它需要傳送兩種不同的訊息型別：第一種是設定檔名，第二個讀取或寫入具有該名稱的檔案的資料。幸運的是，QL足夠靈活，可以提供另一種探索途徑。

結論

在微軟，我們採取深度防禦的方法來保護雲和客戶資料的安全。其中一個重要部分是對Azure內部攻擊面進行全面的安全審查。在這個嵌入式裝置的原始碼回顧中，我們應用了Semmle QL的高階靜態分析技術來發現基於訊息的管理協議中的漏洞。這在各種bug類中發現了總共33個易受攻擊的訊息處理程式。使用QL使我們能夠自動執行完全手動程式碼審查的重複部分，同時仍然應用探索性方法。

附：Part1在去年釋出的，已經有過他人翻譯：

使用Semmle QL進行漏洞探索 Part1： https://xz.aliyun.com/t/2641 （翻譯：@ Stefano ）