使用 Semmle QL 進行漏洞搜索 Part 1
在這篇文章之前，我們曾討論過MSRC是如何自動化的對發現的漏洞進行原因分析並形成報告的。而在完成此操作後，我們的下一步是變體分析：查找和調查漏洞的任何變體。事實上這也是最為重要的一點，即找到所有這些變體並同時修補它們，否則我們就要承擔其在野外被利用的風險。在這篇文章中，我想闡述的其實就是如何自動化的發現這些漏洞的變體。
在過去一年左右的時間裡，我們一直在使用第三方靜態分析環境Semmle來擴充我們的手動代碼審查流程。它將代碼編譯到關係資料庫（快照資料庫 - 資料庫和源代碼的組合），使用Semmle QL查詢，Semmle QL是一種用於程序分析的聲明式的面向對象的查詢語言。
基本工作流程是，在原因分析之後，我們編寫查詢以查找在語義上與原始漏洞類似的代碼模式。任何結果都像往常一樣進行分類，並提供給我們的工程團隊以便開發修復程序。此外，查詢被放置在中央存儲庫中，以便由MSRC和其他安全團隊定期重新運行。這樣，我們可以隨著時間的推移和跨多個代碼庫擴展我們的變體發現。
除了變體分析之外，我們還在源代碼的安全性評估中主動使用QL。這將是未來博客文章的主題。現在，讓我們看看一些受MSRC案例啟發的現實案例。
整數溢出檢查不正確
第一種情況是一個直接定義的錯誤，但在大型代碼庫中找到變體會很繁瑣。
下面的代碼展示了在添加無符號整數時檢測溢出的常用習慣用法：
if (x + y
// handle integer overflow
}
不幸的是，當整數類型的寬度足夠小需要進行整體提升時，它就不能正常工作了。例如，如果x和y都是無符號short，則在編譯時，上面的代碼最終將等同於（unsigned int）x + y
這是一個匹配此代碼模式的QL查詢：
importcpp
fromAddExpr a, Variable v, RelationalOperation r
wherea.getAnOperand() = v.getAnAccess()
andr.getAnOperand() = v.getAnAccess()
andr.getAnOperand() = a
and forall(Expr op | op = a.getAnOperand() | op.getType().getSize()
and nota.getExplicitlyConverted().getType().getSize()
selectr, "Useless overflow check due to integral promotion"
在from子句中，我們定義了在查詢的其餘部分中使用的變數及其類型。 AddExpr，Variable和RelationalOperation是表示快照資料庫中各種實體集的QL類，例如， RelationalOperation通過關係操作（小於，大於等）覆蓋每個表達式。
where子句是查詢的核心，使用邏輯連接詞和量詞來定義如何關聯變數。將其分解後會發現，這意味著加法表達式和關係運算需要與其中一個操作數相同的變數（上面示例代碼中的x）：
a. getAnOperand() = v.getAnAccess() and r.getAnOperand() = v.getAnAccess()
關係操作的另一個操作數必須這樣被添加：
r.getAnOperand（）= a
添加的兩個操作數必須具有小於32位（4位元組）的寬度：
forall（Expr op | op = a.getAnOperand（）| op.getType（）。getSize（）
但是如果在加法表達式上有一個顯式的強制轉換，那麼它是否小於32位就不重要了：
not a.getExplicitlyConverted().getType().getSize()
（這樣的檢查就像（無符號short）（x + y）
最後，select子句就會定義結果集。
此漏洞最初在Chakra（Edge的JavaScript引擎）中被報告，其中特定無效溢出檢查的結果是內存損壞。該查詢與原始漏洞匹配，但在Chakra中沒有其他變體。但是，我們在將此確切查詢應用於其他Windows組件時發現了幾個變體。
不安全地使用SafeInt
滾動自己的整數溢出檢查的另一種方法是使用內置此類檢查的庫.SafeInt是一個C ++模板類，它覆蓋算術運算符以拋出檢測到溢出的異常。
以下是如何正確使用它的示例：
int x，y，z;
// ...
z = SafeInt （x）+ y;
但是這裡有一個被無意中誤用的例子 - 傳遞給構造函數的表達式可能已經溢出：
int x，y，z;
//...
z = SafeInt （x + y）;
如何編寫查詢來檢測這個？在前面的示例中，我們的查詢僅使用了內置的QL類。那麼對於這個，讓我們重新來定義我們的開始。為此，我們從（使用extends）中選擇一個或多個QL類進行子類化，並定義一個特徵謂詞，該謂詞指定快照資料庫中與該類匹配的那些實體：
class SafeInt extends Type {
SafeInt() {
this.getUnspecifiedType().getName().matches("SafeInt
}
}
QL類Type表示快照資料庫中所有類型的集合。對於QL類SafeInt，我們將其子集化為名稱以「SafeInt
接下來，我們定義可能會溢出的表達式子集。大多數算術運算都會溢出，但不是全部，這就要看我們使用QL的instanceof運算符來定義哪些運算符了。我們使用的是遞歸定義，因為我們需要包含諸如（x + 1）/ y之類的表達式，即使x / y不是。
class PotentialOverflow extends Expr {
PotentialOverflow() {
(this instanceof BinaryArithmeticOperation // match x+y x-y x*y
and not this instanceof DivExpr // but not x/y
and not this instanceof RemExpr) // or x%y
or (this instanceof UnaryArithmeticOperation // match x++ x-- ++x --x -x
and not this instanceof UnaryPlusExpr) // but not +x
// recursive definitions to capture potential overflow in
// operands of the operations excluded above
or this.(BinaryArithmeticOperation).getAnOperand() instanceof PotentialOverflow
or this.(UnaryPlusExpr).getOperand() instanceof PotentialOverflow
}
}
最後，我們在查詢中將這兩個類關聯起來：
from PotentialOverflow po, SafeInt si
where po.getParent().(Call).getTarget().(Constructor).getDeclaringType() = si
select
po,
po + " may overflow before being converted to " + si
.(Call) 和.(Constructor) 是內聯強制轉換的示例，類似於instanceof，是限制那些QL類匹配的另一種方式。在這種情況下，給定一個可能溢出的表達式，我們只需要關注其父表達式是某種調用就可以了。此外，我們只需要知道該調用的目標是否是構造函數，以及它是否是某個SafeInt的構造函數。
與前面的示例一樣，這是一個跨多個代碼庫提供了許多可操作結果的查詢。
JavaScript的重新使用到免費使用
下一個示例是Edge中由於重新進入JavaScript代碼而導致的漏洞。
Edge定義了許多可以從JavaScript調用的函數。此模型函數說明了此漏洞的本質：
HRESULT SomeClass::vulnerableFunction(Var* args, UINT argCount, Var* retVal)
{
// get first argument -
// from Chakra, acquire pointer to array
BYTE* pBuffer;
UINT bufferSize;
hr = Jscript::GetTypedArrayBuffer(args[1], &pBuffer, &bufferSize);
// get second argument –
// from Chakra, obtain an integer value
int someValue;
hr = Jscript::VarToInt(args[2], &someValue);
// perform some operation on the array acquired previously
doSomething(pBuffer, bufferSize);
…
問題是當Edge回到Chakra時，例如在VarToInt期間，可以執行任意JavaScript代碼。上面的函數可以通過傳遞一個覆蓋valueOf的JavaScript對象來釋放緩衝區來利用，所以當VarToInt返回時，pBuffer是一個懸空指針：
var buf = new ArrayBuffer(length);
var arr = new Uint8Array(buf);
var param = {}
param.valueOf = function() {
/* free `buf`
(code to actually do this would be defined elsewhere) */
neuter(buf); // neuter `buf` by e.g. posting it to a web worker
gc(); // trigger garbage collection
return 0;
};
vulnerableFunction(arr, param);
因此，我們在QL中尋找的特定模式是：從GetTypedArrayBuffer獲取指針，然後調用可能執行JavaScript的Chakra函數，然後使用指針。
對於數組緩衝區指針，我們匹配對GetTypedArrayBuffer的調用，其中第二個參數（Call的getArgument為零索引）是表達式（＆）的地址，並取其操作數：
class TypedArrayBufferPointer extends Expr {
TypedArrayBufferPointer() {
exists(Call c | c.getTarget().getName() = "GetTypedArrayBuffer" and
this = c.getArgument(1).(AddressOfExpr).getOperand())
}
}
這裡使用存在的邏輯量詞來將新變數（c）引入範圍。
有幾個Chakra API函數可用於JavaScript重入。我們可以識別執行此任務的內部Chakra函數，而不是通過名稱定義它們，並使用QL從調用圖中計算出來：
// examine call graph to match any function that may eventually call MethodCallToPrimitive
predicate mayExecJsFunction(Function f) {
exists(Function g | f.calls+(g) and g.hasName("MethodCallToPrimitive")
}
// this defines a call to any of the above functions
class MayExecJsCall extends FunctionCall {
MayExecJsCall() {
mayExecJsFunction(this)
}
}
調用謂詞的「+」後綴指定傳遞閉包 - 它將謂詞應用於自身，直到匹配為止。這允許對函數調用圖進行簡明定義的探索。
最後，此查詢將這些QL類定義放在一起，通過控制流將它們相關聯：
from TypedArrayBufferPointer def, MayExecJsCall call, VariableAccess use, Variable v
where v.getAnAccess() = def
and v.getAnAccess() = use
and def.getASuccessor+() = call
and call.getASuccessor+() = use
select use,
"Call to " + call + " between definition " + def + " and use " + use
謂詞getASuccessor（）指定控制流中的下一個語句或表達式。因此，使用例如call.getASuccessor +（）= use將跟隨調用的控制流圖，直到有匹配使用。下圖說明了這一點：
除了最初報告的漏洞之外，此查詢還發現了四個變體，所有這些變體都被評估為嚴重程度。好了，本篇就到此為止了。下一部分將介紹使用QL進行數據流分析和污點跟蹤，以及我們對Azure固件組件的安全性審查中的示例。
TAG:嘶吼RoarTalk |