【论文分享】SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code
論文名:SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code
來源會議:ICSE 2019
來源團隊:香港科技大學(源傘團隊)
簡介
盡管過去幾十年工業界和學術界都花很大努力在檢測內存泄露漏洞上,但是在工業界級的代碼量上的效果一直不是很好。現有的工作存在一個很難解決的悖論問題——犧牲擴展性換取高精度,或者擴展性好,但精度不高。
這篇文章用了staged approach(分步驟)來解決這個問題。第一步,使用擴展性好但是不精確的分析去計算候選的內存泄露路徑。第二步,使用更精確的分析去驗證這些候選路徑的可行性。第一步是可擴展的,因為使用了新的稀疏程序表示方法——use flow graph(UFG)。UFG能夠進行多項式時間狀態分析。第二步是精確和高效的,因為只有很小部分的候選路徑,并且設計了小巧的約束求解器。
實驗結果表示SMOKE能夠檢測高達800萬行的代碼,并且誤報只有24.4%。同時,SMOKE比現有的工業工具都要快,大概快5.2x到22.8x之間。在29個成熟的常用的benchmark里,smoke發現了30個未知的漏洞,均被開發者驗證,其中1個有CVE-ID。
要解決的問題
內存泄露漏洞很多。
- 2018上半年僅僅火狐瀏覽器和谷歌瀏覽器就檢測出超過680個內存泄露漏洞。
- 2017年超過240個CVE都是內存泄露漏洞。
現在的檢測工具在擴展性和準確性做權衡。
其中一類工作犧牲路徑敏感性來換取擴展性,但同時精確度也不高。比如SABER,最近的一個路徑不敏感的內存泄露檢測技術,在我們的評估中有66.7%的誤報。
另外一種工作,遍歷控制流圖,并使用路徑敏感分析來實現高精度。然而經常會遇到擴展性問題,尤其是對整個程序進行分析時。比如SATURN在500萬行的代碼上檢測內存泄露需要超過23小時。其他的比如CSA和INFER,兩個小時后就撲街了。
如何解決的
作者發現程序中只有一小部分的路徑會導致內存泄露。為了檢測成千上百萬行的代碼,作者認為稀疏值流分析可以通過VFG來追蹤數據依賴圖的關系,并且效果要比控制流圖要好。然而,作者發現VFG要檢車任意的有限狀態機屬性(比如內存泄露問題)效果不是很好。作者再簡單證明了一下直接用VFG方法來檢測內存泄露問題是個NP難問題。
為了解決這一問題,作者擴展了VFG,叫做UFG,將堆對象的定義和使用都編碼進圖了。所有堆對象的使用的地方根據控制流圖來排序,并且用多項式時間圖搜索方法來找到潛在的內存泄露路徑。驗證過程是很高效的,平均路徑長度只有21…作者使用了約束求解器來過濾掉一些矛盾的路徑。最后用z3來解決剩下的候選路徑。
smoke系統的框架如下圖所示。作者將LLVM 字節碼文件作為輸入。首先預處理階段使用流敏感和上下文敏感的指針分析去計算數據依賴。同時在控制流圖的逆向圖里計算控制依賴。為了構建調用圖,我們使用must-alias結果來解決函數指針的問題,同時用class hierarchy 分析來解決虛函數調用問題。在狀態分析里,只考慮內存分配操作成功的情況。比如,x=malloc()。
下面幾張圖感覺很淺顯易懂,讓我們知道文章的UFG圖到底干了啥。
到達的效果如何
作者選擇的測試程序有SPEC2000和17個開源程序。同時和相關工作SABE,PINPOINT,CSA和INFER做了對比。主要針對擴展性、準確性和召回率做了評估。并且還對兩個步驟的貢獻程度做了評估。此外還貼了代碼說明自己的誤報在哪里。
擴展性的實驗結果如下:
準確性和召回率的結果:
兩個分析步驟的數據:
一個誤報例子:
還有哪些沒解決的
在某些情況下準確率也不好。
-
lack of library specification,詳見figure11
-
指針分析自身的不精確的問題。
-
有些在分支條件里弄了很多復雜運算、或者復雜數據依賴、或者很深的過程間影響的路徑都沒辦法識別出來。犧牲擴展性可以緩解該問題。
總結
感覺文章的圖畫的不錯,寫作上也很清晰,以后寫論文可以照這篇來寫。
總體來說是不錯的工作。值得借鑒學習!
文章工作開源于:https://smokeml.github.io/
總結
以上是生活随笔為你收集整理的【论文分享】SMOKE: Scalable Path-Sensitive Memory Leak Detection for Millions of Lines of Code的全部內容,希望文章能夠幫你解決所遇到的問題。
- 上一篇: 选择开关的电气符号
- 下一篇: c语言驻波,C版:基于声学驻波的液位检测