Saluki: 使用靜態屬性檢查查詢汙點風格的漏洞
作者： {wh1t3p1g}@ArkTeam
原文作者： Ivan Gotovchits，Rijnard van Tonder，David Brumley
原文標題： Saluki: Finding Taint-style Vulnerabilities with Static Property Checking
原文會議： Network and Distributed Systems Security (NDSS) Symposium 2018
原文連結： http://www.ndss-symposium.org/wp-content/uploads/sites/25/2018/07/bar2018_19_Gotovchits_paper.pdf
saluki是一種用於檢查二進位制程式碼中的汙點（資料依賴）安全屬性的新工具。 Saluki提供了一種用於表達基於汙點的策略的特定語言。Saluki在二進位制程式分析中包含兩個新想法。首先，Saluki使用μflux對二進位制檔案中資料依賴進行敏感路徑，敏感上下文的恢復。其次，Saluki引入了一個合理的邏輯系統來推理資料依賴。作者在該邏輯系統上開發了一種特定的語言，用於表達安全屬性。
1.saluki 執行結構
使用者分兩步檢查安全策略。 首先，使用者使用 Saluki 策略語言指定他們的安全策略。 Saluki 安全策略用於描述安全汙點模式的路徑屬性。 策略包括兩部分：（ a ）識別感興趣的程式模式，例如，諸如 recv 和 system 之類的 API 呼叫，以及（ b ）在感興趣的位置之間進行檢查資料依賴關係。
如圖所示，saluki的執行結構
- 載入規則
- 將二進位制解析為可用於分析的中間程式碼
- 執行 μflux 以收集有關每個特定來源的執行的資料流。
- 在策略、程式和收集的事實的基礎上執行解算器。解算器將確定這個屬性是否成立。該求解器實現了一個圍繞特定 DSL 構建的新型邏輯系統和演算法。
- Saluki 輸出結果。
以下面的樣例安全屬性為例
通常不希望從recv函式中獲取到資料直接流入到system函式，所以定義兩個感興趣的API函式（recv，system），其中recv函式可以接受4個引數，但是隻對buf感興趣，這裡可以用_來表示不感興趣的引數。其中cmd/buf，用來限制資料流，從buf進入到cmd
2.saluki 邏輯系統和語言
作者開發了用於描述安全屬性的語言，1中提到的案例就是其中一個例子。語言語法允許我們將屬性指定為一系列模式和一組約束。 如果所有模式在給定約束下匹配，則屬性成立。 下圖為該語言語法
-
定義2——抽象程式模型
抽象程式模型是一個三元命題函式 P = （ T ， D ， P ）。 命題 Tt 表示存在項 t （見定義2）。 命題 D （ l’ ， R’,l ， R ）表示從具有標記l的程式項中定義的變數 R 到具有標記 l’ 的程式項中使用的變數 R’ 的資訊流（資料依賴性）。 命題 P （ p ， l ， R ）表示使用者定義的謂詞 p ，其用於在具有標號 l 的程式項中使用的變數 R.
-
定義2——程式項t
程式項t是一個5元組 (L t , S t , C t , D t , U t )
其中 L t 是唯一標識術語的標籤， S t 是一組靜態後繼者， C t 是影響後繼者選擇的一組程式變數， D t 是由術語定義的一組程式變數 ， U t 是一組程式變數，用於術語中。
其中語法中的相關定義具體見論文，這裡由於篇幅不詳細敘述
Saluki 以 1675 行 OCaml 程式碼實現。 它建立在 BAP 平臺之上，目前支援將 x86 ， x86-64 和 ARM 體系結構提升為中間表示。 BAP 為 GNU C 庫執行 CFG 恢復和函式原型推理， BAP 使用 LLVM 作為反彙編後端。
專案線上地址： https://github.com/BinaryAnalysisPlatform/bap-plugins/tree/master/saluki
3.討論
文章主要通過在二進位制檔案中使用安全屬性提取相關敏感路徑和上下文，從而進一步分析。文中提到了作者開發的安全屬性語言，使用該語言用以描述我們所感興趣的函式之間的上下文關係。這點其實有點類似屬性圖的實現，使用屬性圖的方式構造出相關程式碼屬性庫，通過類SQL語句，推論上下文關係，從而判斷是否存在程式碼安全問題。文章的提取敏感路徑和上下文的方式可供借鑑。