標題：基於Binary Ninja的靜態污點分析：以MySQL Cluster漏洞為例（下）

在上文中，我們為讀者介紹了污點源的定義等靜態污點分析方面的知識，在本文中，我們將繼續為讀者演示如何處理來自多個污染源的SSA變量的約束等技巧。

（接上文）

對來自多個污染源的SSA變量的約束在進行污染傳播時，如果有任何源變量被污染，包括PHI函數，我們就將目標變量標記為污染變量。在第二階段的過濾過程中，如果一個變量受到約束，我們會將約束應用於所有相關變量。但是，當派生變量（子變量）來自一個以上的獨立污點源（父變量），並且只有一個父變量被驗證，那麼，子變量也被認為被驗證過了。但這種做法是不可取的。考慮一下下面的例子：

假設x和y來自兩個獨立的污點源，而index是兩者之和，因此，它是一個派生變量。當x被驗證後，由於y沒有被驗證，所以，index仍然可能被污損——但是，之前的算法沒有考慮到這一點。

為了解決這個問題，我考慮將每個派生的污點變量與實際的源變量聯繫起來，稱為根變量，並維護每個根變量的def-use鏈副本。例如，變量index#3有兩個根變量：x#0和y#0變量。對於每個根變量，都利用與變量index#3相關的污點信息來維護一份可達塊的副本。當x#1變量被驗證時，只有變量index#3的副本x#0被標記為不可達，而副本y#0仍被視為污染變量。我們可以通過變量的依賴圖來表示這些關係。

使用依賴圖確定SSA變量之間的關係在變量依賴關係圖中，函數中的任何污點變量都被表示為一個節點。當一個變量來自另一個變量時，就形成了一條從父變量（節點）到子變量（節點）的有向邊。

為了建立變量之間的關係，使用get_ssa_var_definition()訪問所有污點變量的定義位置（definition site）。當MLIL表達式中的任何一個源變量被污染時，在圖中創建一個邊連接。由於在MLIL_LOAD_SSA操作中被污染的變量沒有父節點或傳入的邊，因此，它們就成為了根節點。

這樣的依賴關係圖通常存在許多弱連接的組件，因為加載自受污染的內存區的每一段內存都將被分配給一個新的變量，對應於圖中一個新節點。簡單地說，每個內存加載都會和它的派生變量一起創建一個子圖。當變量派生自多個根節點時，相應的子圖可能會與另一個子圖連接。下面是一個來自函數Dbtux:execTUX_ADD_ATTRREQ()的示例依賴關係圖：

另一個需要注意的屬性是，依賴關係圖不一定是有向無環圖（DAG）。這是因為循環可能是通過PHI函數中變量的循環依賴關係引入的。請考慮以下循環操作的SSA表示形式：

此處，counter#2的值取決於counter#1或counter#4，這是一個PHI函數，前置塊決定函數的結果。在循環的下方，counter#4依賴於counter#2。這種關係將在依賴關係圖中表示為一個循環。

生成依賴關係圖後，很容易獲得與任何受污染變量關聯的根變量。此外，還可以獲取任何給定變量的子變量和父變量來處理傳遞關係。現在唯一缺少的部分是沒有表示出受污染的信息是如何向前傳播到其他函數的。

靜態函數鉤子與過程間污點傳播一旦完成對當前函數的分析，所有帶有污染參數的MLIL_CALL_SSA和MLIL_TAILCALL_SSA指令都將被處理。對於具有已知目的地（例如，MLIL_CONST_PTR)的任何調用指令，都會提取符號以檢查靜態鉤子，具體見下面的示例代碼：

forexpr,callee_varsinself.callee.items():

ifexpr.dest.operation==MediumLevelILOperation.MLIL_CONST_PTR:

symbol=self.bv.get_symbol_at(expr.dest.constant)

forfuncinconfig.function_hooks:

ifsymbolandfuncinsymbol.name:

self.visit_function_hooks(expr,func,callee_vars)

break

else:

dest=expr.dest.constant

args=self.get_args_to_pass(expr,callee_vars)

callee_trace=MLILTracer(self.bv,dest)

callee_trace.set_function_args(args)

callee_trace.trace()靜態鉤子是處理函數的程序——與其他函數相比，我們打算以不同的方式處理這些函數。對libc函數memcpy的調用來說，無需進行污染傳播，相反，我們只對檢查受污染的大小、源或目標參數感興趣。為了向分析器提供這些信息並進行相應的配置，我們將使用具有函數名稱和參數的JSON配置，具體如下所示：

{

'memset':['arg0','arg1','arg2'],

'bzero':['arg0','arg1'],

'bcopy':['arg1','arg2'],

'memcpy':['arg0','arg1','arg2'],

'memmove':['arg0','arg1','arg2'],

'strncpy':['arg0','arg1','arg2'],

'strlcpy':['arg0','arg1','arg2']

}要檢查的參數從0開始索引。對於memcpy函數來說，所有3個參數都被標記為需要進行分析。與JSON配置中提供的參數索引相關的SSA變量，都需要進行污染檢驗。例如，配置文件中的arg2將映射到一個與memcpy函數的size參數相關的SSA參數變量：

defget_var_for_arg(self,expr,arg):

params=expr.params

argno=lambda_arg:int(_arg.split('arg').pop())

ifargno(arg)len(params):

param=params[argno(arg)]

ifparam.operationinoperations.MLIL_GET_VARS:

returnparam.vars_read[0]

defvisit_function_hooks(self,expr,func,tainted_vars):

args=config.function_hooks[func]

forarginargs:

ssa_var=self.get_var_for_arg(expr,arg)

ifssa_varintainted_vars:

logging.info('Potentialcontrolledargsincallto%s@0x%lx%s%s',func,expr.address,expr,self.get_stack_trace())靜態鉤子也可用於標記要被污染和進一步傳播的函數的輸出變量或返回值。但是，由於未考慮特定於函數的相關細節，因此，目前尚未實現該功能。必要時，可以重用MLIL_SET_VAR_SSA操作的visitor處理程序，以在CALL操作期間實現反向污染傳播。對於沒有鉤子的任何其他函數，可以通過將目標函數的變量標記為已污染來傳播污染信息。

defset_function_args(self,funcargs):

forarg,valueinfuncargs.items():

#BNfunction.parameter_varsisbuggy#2463

forvarinself.function.vars:

ifvar.name==arg:

ssa_var=SSAVariable(var,0)

ifself.is_pointer(value):

self.source_vars[ssa_var]=value

elifself.is_tainted(value):

self.tainted_vars[ssa_var]=value通過可達塊跟踪漏洞一旦污點傳播和過濾階段結束，分析的最後一個階段就是遍歷所有污點變量，並檢查潛在洩漏點（sink）的可達塊。根據已經報告的漏洞，我將查找目標定為涉及越界(OOB)內存訪問、函數調用API（如memcpy）期間的緩衝區溢出、不可信的指針輸入以及受污染的循環計數器的漏洞。本節的其餘部分將詳細介紹其他檢測策略。

OOB讀寫MySQL Cluster中的大多數漏洞都是OOB讀寫相關的內存訪問漏洞，這些是由於缺少對不可信數組索引的驗證所致。為了檢測這些漏洞，我們可以將任何MLIL_LOAD_SSA或MLIL_STORE_SSA視為洩漏點。以下是來自DBDIH:execget_latest_gci_req()的示例代碼：

Signal*arg2{Registerrsi}

int64_targ1{Registerrdi}

Dbdih:execGET_LATEST_GCI_REQ:

0@005b4b24rax#1=zx.q([arg2#0+0x28].d@mem#0)

1@005b4b27rax_1#2=zx.q([arg1#0+(rax#12)+0x9b784].d@mem#0)

2@005b4b2e[arg2#0+0x28].d=rax_1#2.eax@mem#0-mem#1

3@005b4b32returnrax_1#2

current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.srcil:[arg1#0+(rax#12)+0x9b784].d@mem#0current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.src.operation

current_function.get_low_level_il_at(0x5b4b27).mlil.ssa_form.src.src.vars_read

[ssa在這裡，rax#1是已污染的，因此，使用MLIL_LOAD_SSA的讀操作可以被認為是一個OOB讀條件。類似地，考慮一下來自Thrman:execOVERLOAD_STATUS_REP()的另一個案例：

Signal*arg2{Registerrsi}

void*arg1{Registerrdi}

Thrman:execOVERLOAD_STATUS_REP:

0@0078415fr14#1=arg2#0

1@00784162r15#1=arg1#0

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

current_function.get_low_level_il_at(0x78416b).mlil.ssa_formil:[arg1#0+(rax#13)+0x3ca0].d=rcx#1@mem#0-mem#1

current_function.get_low_level_il_at(0x78416b).mlil.ssa_form.operation

current_function.get_low_level_il_at(0x78416b).mlil.ssa_form.dest.vars_read

[ssa在這裡，rax#1再次受到污染，因此，使用MLIL_STORE_SSA的寫入操作可以被視為OOB寫入條件。

API緩衝區溢出靜態函數鉤子可用於檢測由於傳遞給memcpy、memmove等函數的參數缺乏驗證而導致的緩衝區溢出漏洞。有關此問題的詳細信息已經在上面的“靜態函數鉤子與過程間污染傳播”一節中進行了詳細的說明。簡單來說，只要掛鉤函數的任何我們感興趣的參數受到了污染，我們就會將其記錄為潛在漏洞。

不可信的指針解引用在某些情況下，我注意到MySQL Cluster會將不可信的輸入轉換為指針，然後進行指針解引用。為了識別這種漏洞，我們可以藉助於Binary Ninja的類型信息。 MLIL變量對像有一個Type屬性，用於返回與變量相關的Type對象。一個Type對象的類型可以用type_class屬性來訪問。這裡的模型是，污點源指向Signal結構中的一個污點內存區域，而目標變量是PointerTypeClass類型的。 Type對像還有一個confidence屬性，具體如下圖所示：

current_function.get_low_level_il_at(here).mlil.ssa_form

current_function.get_low_level_il_at(here).mlil.ssa_form.destcurrent_function.get_low_level_il_at(here).mlil.ssa_form.dest.var

current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type

current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type.type_class

current_function.get_low_level_il_at(here).mlil.ssa_form.dest.var.type.confidence

255對於變量類型來說，confidence的最大值為255。為減少誤報，分析器僅考慮具有最大置信度的類型信息。

if(dest.var.type.type_class==TypeClass.PointerTypeClass

anddest.var.type.confidence==255andexpr.src.operation==MediumLevelILOperation.MLIL_LOAD_SSA):

instr=self.function_mlilssa[expr.instr_index]

logging.info('Potentialuntrustedpointerload@0x%lx%s%s',expr.address,instr,self.get_stack_trace())循環中的污點控制流操作我們知道，依賴於受污染變量的某些循環終止條件會導致我們感興趣的漏洞。然而Binary Ninja的MLIL並沒有提供關於循環的信息，因此，替代方案是通過HLIL來檢測受污染的循環條件。比如，Cmvmi:execEVENT_SUBSCRIBE_REQ()中循環語句的HLIL如下所示：

/*0050516b*/do

/*0050516b*/uint64_trsi_7=zx.q(*(r12+(rcx_32)+0x30))

/*00505170*/if(rsi_7u0x10]=rsi_7.b

/*00505184*/rdx_5=*(r12+0x2c)

/*00505160*/rcx_3=rcx_3+1

/*00505160*/while(rcx_3uzx.q(rdx_5))這裡的問題是，我們已經使用MLIL實現了整個污點傳播，而Binary Ninja卻無法提供MLIL和HLIL之間的映射。因此，即使可以檢測到循環，也需要知道受污染的MLIL變量是否映射到循環條件中使用的HLIL變量。

不過，倒是存在一個變通方法，即HLIL指令具有一個條件屬性，該屬性可以用來獲取與循環關聯的條件語句，而這個條件語句的地址可以映射到相應的MLIL_IF指令。

exprHLIL_DO_WHILE:dowhile(rcx_3uzx.q(rdx_5))expr.conditionHLIL_CMP_ULT:rcx_3uzx.q(rdx_5)expr.operation

hex(expr.condition.address)

'0x505169'

current_function.get_low_level_il_at(here).mlil.ssa_form

hex(current_function.get_low_level_il_at(here).mlil.ssa_form.address)

'0x505169'因此，如果任何一條MLIL_IF指令被污染，並且是HLIL循環條件的一部分，那麼分析器就會將其記錄為一個潛在的漏洞。

關於支配關係的實驗支配關係提供了關於基本塊執行順序的相關信息。如果所有通向Y的路徑都要經過X，那麼，我們就可以說基本塊X支配著另一個基本塊Y。

在所提供的圖中，節點B支配著節點C、D、E和F，因為通往這些節點的所有路徑必須經過節點B。因此，被節點B支配的全部節點集包括B、C、D、E和F節點。此外，還有一個相關的概念叫做嚴格支配方，它並不考慮可疑的節點。因此，被節點B嚴格支配的所有節點的集合包括節點C、D、E和F。

Binary Ninja的BasicBlock對象具有dominators和strict_dominators屬性，提供關於函數中支配關係的相關信息。

current_function.mlil.ssa_form.basic_blocks

[

current_function.mlil.ssa_form.basic_blocks[2].dominators

[

current_function.mlil.ssa_form.basic_blocks[2].strict_dominators

[那麼，我們該如何利用Binary Ninja中可用的dominance屬性來處理污染約束，而不是通過networkx包中的圖可達性算法來處理這個問題呢？

將約束映射到支配塊為了檢查一個SSA變量的def-use鏈中的所有基本塊是否可達，我們可以遵循以下步驟：

查找與該變量關聯的所有約束塊。

使用def-use鏈獲取所有引用該變量的基本塊。

對於每個基本塊，檢查它是否被約束塊嚴格支配。如果是，則該變量被認為是該基本塊的有效變量，並且被認為是不可達的。

回到同一個示例，索引在中得到驗證，而它又是的支配方。因此，通過檢查支配方的約束塊，就可以確定可達性