源傘科技Pinpoint,作為BAT都在使用的一款靜態代碼分析工具,到底有什么領先於其他廠商的能力?
1. 擴展和部署功能對比
- 源傘科技Pinpoint現有的檢查器可以通過簡單的json配置文件擴展業務邏輯。比如敏感數據泄露到日志檢查器,企業或許有很多自己的日志打印函數,我們可以通過人工配置指定,即可提高檢測質量。
- 如果不想人工配置,Pinpoint有未公開發布的庫函數學習工具,可以通過線下分析企業代碼庫自動學習和生成上述配置文件。
- Pinpoint對分布式多機掃描部署支持比Coverity好,並發掃描和結果合並x性能也比Coverity更強,能更好支持BAT級別的數千代碼庫掃描(已在BT部署驗證)。
2. 分析能力對比
本節補充一些人工構造的例子介紹Pinpoint在分析能力上比Coverity強的部分。本節所有代碼示例,Coverity均有誤報或漏報。
- Pinpoint更懂數據流
- 精確深度的指針分析,深入分析內存中的程序行為
- 高深度高精度函數調用鏈分析,查找跨越多層函數的深度問題
示例代碼如下:
(鏈接:https://www.sourcebrella.com/online-showcase/?id=5b483da03a21cd078346028f),此示例代碼基於空指針(Null Pointer Dereference)問題檢測。
准備代碼:
代碼中我們定義了一個base基類和兩個衍生類,其中Derived1的doit函數返回了空指針(見(1))這個空指針隨后會被用到。后邊我們又定義了一個user類,里邊有兩個變量,dat1初始化為derived1類型(有空指針),dat2初始化為derived2類型,是安全的(見(2))。user類有一個swap函數交換兩個變量的值,每交換一次,dat1和dat2的虛函數doit是否返回空指針會被交換一次,也就是是否安全的信息會被交換一次(見(3))。如果交換兩次,實際上相當於沒有效果。
然后我們創建confuser類,增加函數調用以及數據流的復雜度,其中所有的swap函數都會交換dat1和dat2的值,我們這里大量使用交換兩次的方式,也就是交換再還原的方式,既沒有改變任何狀態,同時可以增加數據流復雜度(見(4))。最終有SwapData函數交換dat1和dat2, get1函數取dat1的值,get2函數取dat2的值(見(5))。其中get1函數和get2函數各自總計調用54次User::swapData(), 調用鏈最大長度為6 : get1()->f31()->f21()->f11()->swapData()->swapData1()->User::swapData()。
觸發空指針的代碼如下:
代碼中我們先定義了一個confuser類的對象,同時由構造函數初始化為confuer.user.dat1不安全,confuser.user.dat2安全,然后經過了一系列的交換還原操作(見(6)),dat1和dat2的空指針安全性沒有被修改,然后我們進入觸發階段(見(7)),由於沒有被修改dat1對應的get1()函數的doit虛函數會返回空指針,而dat2對應的get2函數是安全的,然后我們交換一次(見(8)),結果就相反了,再交換回來(見(9)),結果又還原了。
這里pinpoint可以完全完美還原這里的每個信息,精確找到其中的空指針問題,這里涉及復雜的調用鏈以及調用關系,復雜的內存數據流(每次confusing.swapData會在內部隱式修改confusing.user.dat1和confusing.user.dat2的值),同變量在不同的程序位置值不相同,以及虛函數對應,每一個都是現有技術很難處理的。因為程序本身的復雜性,精確的建模往往無法規模化,所以很難同時做到深入以及精確的分析。Pinpoint用獨創的整體分析技術【Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, Charles Zhang. Pinpoint: Scalable and Precise Sparse Value-flow Analysis. PLDI.2018】可以精確分析理解整個流程。
- Pinpoint精確分析每個數值
示例代碼如下:
(鏈接:https://www.sourcebrella.com/online-showcase/?id=5b483da03a21cd078346028f),此示例代碼基於整數溢出(Integer Overflow)問題檢測
這里我們定義了7個場景,都是跨函數的數值賦值,然后由相應函數處理過的值進行乘積運算是否會越界的問題,其中f1是標准的越界問題,就是兩個大數乘積是否越界,f2,f3使用了不同的全局變量做除數對導致不同的越界結果。Pinpoint精確建模了全局變量以及數值運算,並進行完整的約束求解,可以精確區分不同數值的大小。f4到f7同時又引入了程序執行路徑的信息,不同的數值可以產生不同的執行路徑,而不同的執行路徑又可以產生不同的執行結果,pinpoint精確建模了每一個數值,即使是和要檢測的目標(這里也就是整數溢出)無關。Pinpoint可以做到用精確的數值信息做執行路徑的建模。
- Pinpoint精確理解多線程行為
- 精確建模線程間同步機制
- 精確匹配線程之間的共享內存
示例代碼如下:
(鏈接:https://www.sourcebrella.com/online-showcase/?id=5b483da03a21cd078346028f),此示例代碼基於數據競爭(Data Race)問題檢測
這里共有8個測試用例,包括測試對線程同步的建模(鎖:test2, test7,信號:test5, test6, fork-join:test1)另外還有對執行路徑了建模(test3,test4)以及共享變量判定(test8)。
對於多線程問題pinpoint精確建模了多線程程序的執行語義,包括線程之間的同步關系。pinpoint可以精確建模函數的調用關系以及精確建模內存結構的能力使得我們有機會可以完整建模多線程的執行語義包括哪些函數可以並發執行,哪些變量是共享變量等。由於線程機制往往要跨越多級函數,涉及共享變量,以及復雜的時序關系,現有工具往往不會深度建模線程語義,也就無法發現深層次多線程問題
- Pinpoint精確深度跟蹤敏感數據,挖掘深度埋藏的安全隱患
- 后門代碼可能被深度埋藏,必須深入精確分析理解程序執行流程才可能發現
- 敏感數據來源和使用點可能距離很遠,需要深度跟蹤才能發現埋藏很深的問題
示例代碼如下:
(鏈接:https://www.sourcebrella.com/online-showcase/?id=5b485a453a21cd0783460294),此示例代碼基於相對路徑遍歷(Relative Path Traversal)問題檢測
這里我們定義了兩個類DataStore用來存儲數據,Confuser用來處理數據。我們定義DataStore類存儲兩個數據,一個char* dat存儲了一個路徑信息,如果路徑信息是來自外部輸入,那么這里就有可能出現路徑遍歷安全隱患,makesafe標志如果被置為非零值,那么getDat()函數將無論如何都會返回安全的/dev/null。
Confuser類自定義了3個transfer函數用來傳遞DataStore中(被污染)的數據,tranfer1-3函數依次調用。如果參數makesafe置為非零值,那么transfer函數將一定會返回安全的數據/dev/null。
在main函數中,我們定義了4個測試。分別對應由於(1)由於dataStore的makesafe置為非零保護危險數據成為安全數據,(2)沒有保護危險數據,(3)安全數據,(4)在數據傳遞過程中進行保護而保證安全的數據。Pinpoint由於有能力完整分析程序中的各個函數以及之間的調用關系,可以完美處理所有示例。
這個例子中的安全問題藏的比較深,而且無法直接手動建模,因為confuser::transfer是用戶自定義函數。這樣如果沒有對於程序執行的深入理解,我們將無法正確的分析confuser::transfer函數的語義,也就沒有辦法精確查找這樣的安全問題。或者無法報出來,或者無法區分那三個實際上安全的情況。
為國產靜態代碼分析工具源傘科技Pinpoint打Call!!