By HireHackking in HACKER
· 1 view
污點分析是一種挖掘安全漏洞的有效手段，即使對於大型代碼庫，也是如此。我的同事Lucas Leong最近演示瞭如何使用Clang Static Analyzer和CodeQL，通過污點分析來建模和查找MySQL NDB Cluster中的漏洞。受到該項工作的啟發，我也開始嘗試類似的東西，但這裡使用的工具是Binary Ninja，因為它也可以很好地處理閉源程序。
以下是我在從事這項工作時想到的幾件事：
◼在不進行邊界檢查的情況下，識別由於使用不受信任的值而導致的漏洞
◼污點的傳播和過濾應該對控制流敏感
◼支持過程間分析
對於這個問題，我將其作為一個圖的可達性問題來處理，這方面，“Tainted Flow Analysis on e-SSA-form Programs”是一篇很好的參考文獻。本文的所有分析都是基於MySQL Cluster 8.0.25和Binary Ninja 2.4.2846完成的。
定義污點源進行污點分析時，必須明確定義污點源。因為MySQL Cluster具有一個消息傳遞架構，所以，我們感興趣的污點源就是消息本身。本節提供了關於消息處理以及如何識別消息處理程序方面的詳細信息。
MySQL NDB Cluster信號MySQL NDB Cluster將功能定義為“塊”，將它們之間傳遞的消息定義為“信號”。 NDB塊通常以C++類的形式實現，每個塊在初始化時都註冊了多個信號處理程序，這些處理程序也是該類的方法。到目前為止，人們發現的大多數漏洞都位於這些消息處理程序中，也被稱為信號處理程序。
所有的塊都繼承了SimulatedBlock類，所以，它們都是使用addRecSignal()來方法來註冊其信號，而該方法則會調用SimulatedBlock:addRecSignalImpl()方法。實際上，註冊的信號處理程序的類型為ExecSignalLocal，並且需要一個參數。對這方面有興趣的讀者，可以參考Frazer Clement的文章“Ndb software architecture”，以及Steinway Wu的文章“Code Reading Notes – MySQL Cluster”，以了解更多細節。在本文中，我們只對信號處理程序的入口點感興趣。下面是一個NDBCNTR塊註冊信號處理程序的示例代碼：
addRecSignal(GSN_CNTR_WAITREP,Ndbcntr:execCNTR_WAITREP);
SimulatedBlock:addRecSignalImpl(GlobalSignalNumbergsn,ExecSignalLocalf,boolforce)
typedefvoid(BLOCK:*ExecSignalLocal)(Signal*signal);處理程序收到的“Signal”對象通常都包含不受信任的數據，而信號處理程序可以通過signal-getDataPtr()方法或其他一些方法來訪問這些數據。處理程序也可以進一步將'Signal'對像傳遞給其他函數。對於這一步的分析，方法有多種。比如，我們可以分析任何以Signal為參數的函數，或者通過交叉引用，查找對SimulatedBlock:addRecSignalImpl()的調用，只分析實際的信號處理程序，然後，通過過程間分析來處理剩下的問題。這裡，我們先介紹前面一步，至於過程間分析，我們將在後文加以介紹。
雖然Signal對象的大小為0x8030字節，但是，並非所有的字節都應該被視為污點。相反，我們應該只把該對象的一小塊內存區域定義為污點，這樣的話，只有從污點區域讀取的內存數據才會被傳播。如果將整個結構都標記為污點的話，會導致大量的誤報。就本例來說，信號的污點數據從偏移量0x28處開始，也就是說，從這個偏移量處開始加載的任何內存數據，都被標記為污點。另外，方法Signal:getDataPtr()和Signal:getDataPtrSend()都會返回一個指向該內存地址的指針。
Uint32m_sectionPtrI[3];
SignalHeaderheader;
union{
Uint32theData[8192];/*Taintedmemoryregionatanoffset0x28*/
Uint64dummyAlign;
};
Uint32m_extra_signals;
inlineconstUint32*Signal:getDataPtr()const{
returntheData[0];
}
inlineUint32*Signal:getDataPtrSend(){
returntheData[0];
}將類型信息從IDA Pro移植到Binary Ninja上這里分析的可執行文件是“ndbd”，它是利用DWARF調試信息構建的NDB Cluster Data Node Daemon進程。為了查找以指向Signal對象的指針作為參數的函數，請檢查所有函數的類型信息，如下所示：
forfuncinbv.functions:
forindex,paraminenumerate(func.parameter_vars):
ifparam.typeisnotNoneandparam.type.type_class==TypeClass.PointerTypeClass:
ifparam.type.tokens[0].text=='Signal':然而，就目前來說，Binary Ninja還無法像IDA Pro那樣魯棒地處理DWARF信息。 Binary Ninja的另一個問題是：在分析C++可執行文件時，它無法檢測“this”參數。因此，它的參數檢測並不准確，從而對我們的污點源分析帶來很大障礙。一個簡單的解決方法是，將類型信息從IDA Pro導入Binary Ninja。例如，Dblqh:prepareContinueAfterBlockedLab()方法在IDA Pro中的類型信息如下所示：
void__fastcallDblqh:prepareContinueAfterBlockedLab(Dblqh*this,Signal*signal,Dblqh:TcConnectionrecPtrtcConnectptr)同樣的函數，在Binary Ninja中看起來卻差別很大。就本例來說，“this”指針“不見”了，而Signal則成了第一個參數。因此，如果將“arg1”標記為污點源的話，將使整個分析出錯：
int32_t*Dblqh:prepareContinueAfterBlockedLab(Signal*arg1,__gnu_cxx:__ops:_Iter_comp_iter由於我們只對Signal參數的正確參數位置和類型信息感興趣，因此，我們可以使用ida2bn目錄中提供的腳本對其進行修復：
int32_t*Dblqh:prepareContinueAfterBlockedLab(void*arg1,Signal*arg2,int64_t*arg3,int32_targ4)一旦類型信息得到修復，我們就可以使用Signal參數來識別函數並標記污染源了。關於通過Binary Ninja處理類型的更多細節，請參考https://docs.binary.ninja/guide/type.html。
污點的傳播與過濾污點傳播的目標很簡單：當某變量被賦予來自Signal數據中的值時，將其標記為污點。如果任何其他變量是從受污染的變量派生出來的，也將其標記為受污染的變量，依此類推。當存在sanitizer時，挑戰就來了。假設一個變量被污染了，但是在某些代碼路徑中存在對該變量的驗證處理。在這種情況下，該變量在該代碼路徑中就不會受污染了。污點傳播應該對控制流敏感，以避免過度污染和誤報。在下面的小節中，我們將介紹如何使用Binary Ninja的IL和SSA形式解決這個問題。此外，如果讀者想要透徹掌握這個主題的話，可以進一步閱讀https://blog.trailofbits.com/2017/01/31/breaking-down-binary-ninjas-low-level-il/和https://blog.trailofbits.com/2017/01/31/breaking-down-binary-ninjas-low-level-il/這兩篇文章。
Binary Ninja的IL和SSA形式Binary Ninja支持各種中間語言（IL），如低級IL（LLIL）、中級IL（MLIL）和高級IL（HLIL）。由於MLIL用變量抽像出了堆棧內存訪問，並提供了與調用位置相關的參數，所以，我認為它更適合執行過程間的污點分析。此外，與HLIL相比，MLIL具有更加豐富的文檔可用。
Binary Ninja提供的另一種強大功能是：能夠為可用的IL提供靜態單賦值（Single Static Assignment，SSA）形式。在SSA形式中，每個變量只被定義一次。當變量被重新賦予另一個值時，會創建一個新的變量版本。因此，我們可以在函數中“全方位地”跟踪一個被污染的變量。現在，請考慮下面最簡單的例子：當變量x被重新賦值時，在SSA形式中會創建一個新版本的變量：
x=1x#0=1
x=x+1x#1=x#0+1SSA變量的def-use鏈Binary Ninja提供瞭如下兩個API：get_ssa_var_definition()和get_ssa_var_uses()，分別用來獲取一個變量的定義位置及其用途。為了便於說明，請看下面Thrman:execOVERLOAD_STATUS_REP()方法的MLIL SSA代碼片段：
Thrman:execOVERLOAD_STATUS_REP:
2@00784165rax#1=zx.q([arg2#0+0x28].d@mem#0)
3@00784168rcx#1=[arg2#0+0x2c].d@mem#0
4@0078416b[arg1#0+(rax#13)+0x3ca0].d=rcx#1@mem#0-mem#1這裡，arg2是一個指向Signal對象的指針。在地址0x00784165處，SSA變量“rax#1”被賦予了一個來自[arg2#0+0x28]的污點值。使用這個被污染的SSA變量rax#1的MLIL指令可以被通過下列方式獲得：
current_function.get_low_level_il_at(here).mlil.ssa_form
current_function.get_low_level_il_at(here).mlil.ssa_form.destssa_var=current_function.get_low_level_il_at(here).mlil.ssa_form.dest
current_function.mlil.ssa_form.get_ssa_var_definition(ssa_var)
current_function.mlil.ssa_form.get_ssa_var_uses(ssa_var)
[il:[arg1#0+(rax#13)+0x3ca0].d=rcx#1@mem#0-mem#1]這些API是我們進一步進行污染分析的構建塊。
用SSA def-use鏈進行污染傳播由於Binary Ninja的IL的組織形式為表達式樹，因此，某個操作的操作數可以由其他操作組成。下圖是BNIL Instruction Graph插件為MLIL SSA指令生成的：
current_function.get_low_level_il_at(here).mlil.ssa_form
current_function.get_low_level_il_at(here).mlil.ssa_form.operation 
其中，MLIL_SET_VAR_SSA操作標記了一個新SSA變量的定義，它將dest變量的值設為src表達式的結果，而src表達式可以由許多其他操作組成。就這裡來說，MLIL_ADD向Signal的基址添加偏移量0x28，然後，MLIL_LOAD_SSA從通過MLIL_ADD計算得到的地址中讀取該值。注意，有效的污染傳播需要訪問每個指令表達式的所有MLIL SSA操作。 Josh Watson的emILator和Jordan的IL指令計數代碼是訪問和處理MLIL SSA指令表達式的好例子。那麼，污點傳播算法到底做了些什麼呢？
◼線性訪問函數中的所有MLIL SSA指令
◼對於任何MLIL_SET_VAR_SSA操作，解析src表達式以檢查它是否是受污染的數據
◼如果src操作數返回受污染的數據，則使用get_ssa_var_uses()獲取dest SSA變量的使用情況
◼訪問使用受污染SSA變量的指令，並在遇到MLIL_SET_VAR_SSA時傳播受污染的SSA變量
◼一旦某個指令污染了某個變量，將其標記為已訪問，並且不再訪問該變量
對SSA變量的約束一旦確定了污點傳播算法，接下來該如何處理污點變量的sanitizer呢？我們只對不進行任何驗證的代碼路徑感興趣。考慮到這一點，讓我們重新審視一下基於def-use鏈的污點傳播算法。實際上，def-use鏈就是代碼的順序語句；因此，這種污點傳播對控制流並不敏感，具體請看下面的演示示例：
其中，傳遞給函數的變量“value”已經收到污染，並在兩個不同的代碼路徑中被用到。在執行0x1184處的基本塊的代碼路徑中，該變量進行了相應的驗證，並被認為是“乾淨的”。同時，用於該變量的get_ssa_var_uses()函數返回了3條指令，具體如下所示：
current_function.get_low_level_il_at(here).mlil.ssa_form.function.get_ssa_var_uses(dest)
[線性處理這3條指令會導致錯誤的結論，即驗證在污點值的兩次使用之前進行。實際上，只有一條指令是受保護的；而其他兩條指令則是易受攻擊的。這個問題可以通過引入控制流來解決。
基於約束圖的控制流敏感傳播其中，MediumLevelILInstruction類有一個il_basic_block屬性，可用來獲取MLIL指令的基本塊信息。
current_function.get_low_level_il_at(here).mlil.ssa_form.il_basic_block利用這個屬性，我們可以獲取SSA變量的定義和SSA變量的使用情況的基本塊，其中也包括進行驗證的基本塊。這些基本塊也被稱為“約束”塊。這些基本塊的一些特性如下所示：
◼定義塊總是支配著SSA變量的所有使用情況。
◼擁有定義的基本塊可以包含約束。這同樣適用於def-use鏈的任何基本塊。
◼一個定義塊總是可達的，因此，其中的所有指令也是可達的。
考慮到這是一個圖的可達性問題，所以，現在問題就變成：在有約束塊的情況下，我們能不能到達SSA變量的def-use鏈中的所有指令？為了回答這個問題，我們可以通過函數的CFG建立一個約束圖，並對其應用如下路徑查找算法：
◼從CFG中刪除約束塊的外向邊。這就是我們的約束圖。
◼在約束圖中尋找定義基本塊和其他def-use鏈的基本塊之間是否存在路徑。
◼如果任何def-use基本塊無法到達，那麼這些指令就不會被用於污點傳播。
由於每個賦值操作在SSA表示中都是唯一的，因此，我們可以維護一個包括約束圖在內的每個變量的必要信息的字典，以便做進一步的分析。下面是一個在存在約束塊的情況下尋找可達塊的示例偽碼：
self.var_def_uses.setdefault(ssa_var,dict())
refs=definition.function.get_ssa_var_uses(ssa_var)
basic_blocks=self.refs_to_basic_blocks(definition,refs)
forrefinrefs:
self.get_constrained_blocks(ref,constraint_blocks,ssa_var)
subgraph=self.get_constrained_subgraph(constraint_blocks)
self.var_def_uses[ssa_var]['subgraph']=subgraph
reachable_blocks=self.get_reachable_blocks(definition,ssa_var,basic_blocks)
forblk,stmtsinbasic_blocks.items():
ifblkinreachable_blocks:
pruned_refs+=stmts
self.var_def_uses[ssa_var]['def']=definition
self.var_def_uses[ssa_var]['refs']=pruned_refs要發現某個SSA變量是否在給定指令中被污染的，我們只需檢查其可達的def-use鏈即可：
defis_reachable(self,var,expr):
ifself.function_mlilssa[expr.instr_index]inself.var_def_uses[var]['refs']:
returnTrue將算術運算作為過濾器除了顯式過濾器之外，還可以將算術運算用作污點過濾器。例如，AND運算或邏輯右移(LSR)運算可能會對值施加約束。在這種情況下，可以使用啟發式方法過濾掉不想要的結果，例如：
在這裡，表面上看污染值並未與任何值進行顯式比較，但是，LSR和AND之類的邏輯運算實際上已經限制了輸入範圍。這就是我發現possible_values屬性非常有用的地方。 Binary Ninja的數據流分析可以為一個表達式提供可能的值：
current_function.get_low_level_il_at(here).mlil.ssa_form.src
current_function.get_low_level_il_at(here).mlil.ssa_form.src.possible_valuescurrent_function.get_low_level_il_at(here).mlil.ssa_form.src
current_function.get_low_level_il_at(here).mlil.ssa_form.src.possible_valuesunsignedranges:[處理污染變量的傳遞關係分析的第一階段，我們需要傳播污染數據並生成相關信息，如污染變量列表、每個SSA變量的約束，以及它們各自的約束子圖。
在分析的第二階段，我們將考察受污染的SSA變量之間的關係。為什麼這很重要？因為我們只尋找unbounded型SSA變量。雖然在第一階段已經處理了對SSA變量施加的任何直接約束，但還沒有處理通過傳遞關係施加給SSA變量的那些間接約束。考慮下面的示例：
變量index#0可能被污染且不受約束。但是，由於對派生變量constrained_var#1進行了驗證，從而間接地對index變量施加了約束，因此，index#3在0x11f2的內存訪問期間不會被污染。下面是另一個例子：
這裡，index#1、index#2、rax#1和constrained_var#1是變量index#0的副本或直接賦值。當變量constrained_var#1被驗證時，其他變量也會被驗證。因此，如果不分析約束對派生變量或變量副本的影響，則會導致誤報。接下來，我們將詳細介紹如何處理相關變量的約束問題。
通過傳遞關係施加給SSA變量的約束在污點傳播階段結束後，我們將遍歷所有有約束的污點變量。對於每一個有約束的變量，我們需要找出其子變量和父變量：
◼從給定變量派生的變量稱為子變量。
◼派生給定變量的變量稱為父變量。
為了檢查所考查的變量上的約束是否對其父變量或子變量產生影響，我們需要進行以下檢查：
為所考查的SSA變量挑選約束子圖。
檢查子變量的定義是否可以從當前變量的定義中到達：
如果不可達，則在CFG中定義子變量之前放置約束，因此，def-use鏈中的基本塊都不會被污染。
如果可達，則在CFG中定義子變量之後放置約束。在這種情況下，還要檢查子變量的de
Recommended Comments