完整流程

Securify分三個(gè)步驟進(jìn)行：

1. 將合約的EVM字節(jié)碼反編譯成靜態(tài)的單一賦值形式（ SSA——static-single assignment）；

2. 將SSA形式的代碼轉(zhuǎn)為基本事實(shí)（base facts）并推斷關(guān)于合約的其他語(yǔ)義事實(shí)（semantic facts）；

3. 匹配由特定領(lǐng)域語(yǔ)言（DSL）編寫的各種安全屬性，輸出對(duì)應(yīng)模式并整合成安全報(bào)告。

安全模式匹配結(jié)果分為真陽(yáng)性（violation）、假陽(yáng)性、真陰性（compliance、no violation）、假陰性。對(duì)于真陽(yáng)性與真陰性Securify都能直接給出準(zhǔn)確結(jié)果，而對(duì)于假陽(yáng)性與假陰性Securify只能在報(bào)告中給出警告標(biāo)識(shí)（warning），之后通過額外人工或其他檢測(cè)方式繼續(xù)識(shí)別確定。

SSA

先講講SSA是什么東西。靜態(tài)單一賦值形式（SSA）是中間表示（IR）的屬性，它要求每個(gè)變量只分配一次，并且每個(gè)變量在使用之前定義。原始IR中的現(xiàn)有變量被拆分為版本，新變量通常由原始名稱用下標(biāo)表示，以便每次定義都有自己的版本。（注：在本方案中部分操作碼如push、dup等會(huì)被消除）

base fact

當(dāng)EVM字節(jié)碼反編譯成SSA形式的中間表示之后，我們需要將其轉(zhuǎn)換成基本事實(shí)。

上圖即一個(gè)基本事實(shí)的表示，其中instr是指令名稱，L是指令標(biāo)簽（CFG中的基本塊），Y是存儲(chǔ)指令結(jié)果的指令（如果有的話），Xn是參數(shù)。

semantic fact

接著我們用基本事實(shí)推斷出語(yǔ)義事實(shí)。

在智能合約的語(yǔ)義分析中，我們通常需要根據(jù)兩種依賴關(guān)系來推斷語(yǔ)義事實(shí)（流控制依賴+數(shù)據(jù)控制依賴）。

意思是存在某條路徑使得L1基本塊流向L2基本塊。

意思是對(duì)任何路徑都是L1基本塊流向L2基本塊。

意思是數(shù)據(jù)T修改了，數(shù)據(jù)Y也可能跟著被修改。

意思是數(shù)據(jù)Y和數(shù)據(jù)T是相等的。

意思是數(shù)據(jù)T不同的取值會(huì)導(dǎo)致數(shù)據(jù)Y的取值不同。

注：

1. 使用通配符(_)來代替在規(guī)則中只出現(xiàn)一次的變量

2. isConst、Taint、join是其他謂詞表達(dá)，與op、mload、mstore、goto同樣屬于基本事實(shí)的表達(dá)。

trace、property

結(jié)論：

trace：指區(qū)塊鏈從一個(gè)老狀態(tài)更新到新狀態(tài)，狀態(tài)包括存儲(chǔ)和內(nèi)存狀態(tài)、堆棧狀態(tài)、事務(wù)信息和塊信息。

property：指在trace上的一種關(guān)系，用一階邏輯規(guī)則定義。

DSL（領(lǐng)域?qū)Ｓ谜Z(yǔ)言domain specific language）

• some+BNF合取范式：一部分路徑符合條件

• all+BNF合取范式：全部路徑符合條件

security patterns of properties

pattern classification

• instruction patterns：指令模式，即由某條指令導(dǎo)致違反該安全屬性（例如上圖中后6個(gè)安全模式）。

• contract pattern：合約模式，即因?yàn)檎麄€(gè)合約的整體原因?qū)е逻`反該安全屬性（很難找出一個(gè)單一的指令對(duì)其違反負(fù)責(zé)，例如上圖中第一個(gè)安全模式）。

Securify2.0

文章傳送：https://arxiv.org/pdf/1806.01143.pdf