使用共享變量分析和約束求解檢測安卓應用數據競爭?

孫 全 , 許 蕾 , 夏昕濛 , 張衛豐

1(計算機軟件新技術國家重點實驗室(南京大學),江蘇 南京 210023)

2(南京大學 計算機科學與技術系,江蘇 南京 210023)

3(南京郵電大學 計算機學院,江蘇 南京 210023)

移動互聯網時代,手機和平板逐漸普及,信息傳播和數據處理逐漸從電腦端向手機端遷移.

根據IDC(http://www.idc.com/prodserv/smartphone-os-market-share.jsp)關于智能手機操作系統的統計報告,截至2016 年第3 季度,安卓系統的市場份額高達86.8%.但由于安卓系統的開源性、手機廠商快速迭代盈利、開發者水平參差不齊,信息泄漏、惡意扣費、系統崩潰常見于安卓應用中.大量的技術和方法隨之被用于解決安卓系統存在的問題,包括GUI 測試[1-4]、惡意軟件檢測[5-7]、并發缺陷檢測[8-10]等.安卓應用并發缺陷檢測是近年興起的研究領域,早期多存在于Java,C/C++程序中.

在安卓應用中,并發缺陷檢測不僅面臨線程調度不確定性的挑戰,還面臨著事件調度不確定性的挑戰.因為安卓系統是事件驅動的,需要監聽多種類型的事件,這些事件來源于用戶的操作、傳感器和系統本身,并且這些事件是無序的、不可預計的、并發的.傳統的靜態分析[1,11-15]和動態分析[16-18]都不能直接應用于安卓系統中的并發缺陷檢測.

并發程序具有效率高、速度快的特性,但由于并發程序內多線程交互頻繁、調度復雜,存在缺陷的可能性也會更高,產生的結果也更嚴重.并發缺陷包括數據競爭、死鎖、原子性違反等多種類型,本文主要關注并發缺陷中的數據競爭問題.數據競爭的發生需要滿足兩個條件:(1)至少兩個語句并發執行,并訪問同一個共享變量,其中一個是寫操作;(2)沒有額外的同步機制進行同步操作.

本文實現了工具RaceDetector 來檢測安卓應用中的數據競爭,特別是關注空引用造成的有害數據競爭.因為無害的數據競爭并不會有明顯的嚴重后果,不會造成損失和嚴重的危害;而有害的數據競爭會嚴重影響用戶體驗,甚至會造成不可預計的損失,比如死機、系統應用的重啟等.

工具RaceDetector 主要包括2 個階段的工作:第1 階段記錄信息,并根據數據競爭的第1 個滿足條件產生可疑的數據競爭候選集合(CS);第2 階段根據安卓應用的先后序關系,使用約束求解方法識別真正數據競爭(RS).本文使用靜態分析解析全部源碼并記錄相關的信息,并使用擴展的共享變量分析來優化性能和提高準確率.

本文的主要貢獻如下:

(1)本文提出了安卓共享變量分析,優化了傳統的逃逸分析去定位安卓共享變量,減小了分析的維度,提高了檢測的性能和準確度.

(2)本文結合靜態分析和約束求解方法來檢測安卓應用中的數據競爭.相對于現有工具EventRacer[8]、CAFA[9]、RaceDroid[10]使用動態分析存在固有覆蓋率低的缺點,靜態分析能夠解析全部的源碼,并使用約束求解計算了所有可能執行的事件調度策略,提高了檢測覆蓋率.

(3)本文對數據競爭的危害程度進行了區分,重點關注由空引用造成的有害數據競爭.相對于無害數據競爭,有害數據競爭會影響用戶體驗,造成不可預期的后果.本文重點闡述空引用造成的有害數據競爭.

(4)實驗詳細闡述了安卓應用中數據競爭問題,并實現了相關工具RaceDetector.本文從Google Play 收集了15 個流行的應用APK 文件作為數據集,與現有工具EventRacer 默認產生300 隨機輸入事件并平均檢測2 個有害數據競爭相比,RaceDetector 平均報告了340 個數據競爭,誤報率為13%(44/340),其中,15 個為有害的數據競爭(4%=15/340).

本文第1 節主要介紹安卓系統以及數據競爭的基本概念.第2 節通過實例說明數據競爭檢測存在的挑戰.第3 節重點闡述檢測工具RaceDetector 各個模塊的設計和實現.第4 節是實驗評估以及實驗結果分析.第5 節介紹相關工作.第6 節總結全文.

1 基本概念

本節將介紹安卓系統相關的概念,并討論安卓應用中的數據競爭.

安卓系統有4 大基本組件.

(1)活動(activity):是安卓應用中最常見的組件,用于展現用戶可見的界面.該組件展現了相關的視圖,用戶可與之進行交互.

(2)服務(service):用于在后臺執行耗時較多的任務,并作相應的數據處理工作.

(3)廣播接收器(broadcast receiver):用于發起廣播和監聽廣播,從而傳遞消息,并據此及時響應和處理.

(4)內容提供者(content provider):可公開提供自己的數據存儲接口并提供路徑,其他組件可以通過路徑訪問相應的數據.

活動和服務有其自由的生命周期回調方法(onCreate(?),onStart(?),onBind(?),onUnBind(?),onDestroy(?)等).這些生命周期方法描述了組件不同的狀態和行為.所有的生命周期方法都被安卓系統所管理,不同的狀態和條件下,相關的組件會被創建或銷毀.

在安卓系統中,當一個應用啟動的時候,會創建一個主線程去處理界面渲染、與用戶交互等不同事件.在主線程中,循環體(looper)、處置器(handle)和消息隊列(message queue)共同處理事件的分發和處置,也就是所謂的消息隊列模型.通常,處置器會對相關的數據以及任務執行入隊操作;循環體則無限循環并取出消息隊列中的數據和任務,然后分發給相關的處置器處理.圖1 展示了主線程和工作線程的運行機制.因為主線程要不斷處理用戶交互以及界面渲染等工作,通常會創建工作線程去執行這些計算消耗型任務,包括AsyncTask、HandleThread等.這些工作線程可在后臺并發地執行相關任務,并通過相關的接口與主線程進行交互,從而更新界面.

Fig.1 Mutil-thread model of Android system圖1 安卓系統多線程模型

區別于過程驅動編程模型,安卓應用是事件驅動編程模型,通過監聽不同的事件運行并更新相關界面.用戶的操作、系統的事件、傳感器等都會作為輸入事件流[19].圖2 展現了安卓應用中事件的構成和相互間的關系.

Fig.2 Event driven model of Android system圖2 安卓系統事件驅動模型

一個輸入事件可以產生于硬件或者軟件:產生于軟件的事件通常發生于應用內部,如Message和Runnable;大部分事件屬于硬件事件(分為輸入事件、傳感器事件和系統事件),其中,輸入事件定義了用戶的交互操作行為,傳感器硬件監聽環境的信息狀態并傳遞給安卓應用,系統事件定義了安卓系統平臺自身狀態信息.這些事件被封裝成消息或者任務,最終經過消息隊列模型得到處置.通常,一個安卓應用中會包含上千個各類事件.

安卓應用中,復雜的系統平臺以及眾多的用戶操作和對應的事件處理函數使得數據競爭檢測變得極為困難:一方面,數據競爭可以發生在主線程和工作線程之間或者多個工作線程之間,即多線程數據競爭;另一方面,數據競爭可以僅發生在主線程中,也就是所謂的單線程數據競爭.單線程數據競爭最初是網絡服務程序中的概念[20-25].此類數據競爭通常發生在界面組件以及監聽事件的回調方法之間.另外,安卓系統中不同應用執行在不同進程當中,由于不同應用之間也可以交互,因此也存在多進程交互的問題,并造成多進程數據競爭.由于在現實世界中出現較少,本文不討論多進程數據競爭,只關注單線程數據競爭.

根據數據競爭危害程度上的差異,本文把數據競爭分為兩種類型:有害的數據競爭和良性的數據競爭.良性的數據競爭常見于多線程程序中,并不會對程序本身造成嚴重后果.在實際研究中,只檢測良性數據競爭意義不是很大.有害的數據競爭可分為兩種類型:一類是有具體的、明顯的有害行為,這類數據競爭一旦發生,就會在應用本身上所體現,例如應用卡頓、崩潰等行為;另一類并不會展現明顯的有害行為,但是對應用正常的邏輯和數據造成影響.本文關注的是第1 類有害數據競爭,并且具體到空引用(free-use)這一類問題上.

2 案例分析

本節將根據一個案例來詳細說明安卓應用中存在有害數據競爭,并討論現有方法檢測數據競爭的局限性.

我們選取了工具EventRacer 數據集中的一個應用OI File Manager(從谷歌應用市場下載了版本2.0.5).EventRacer 檢測OI File Manager 后,報告了785 個數據競爭:一部分是發生在輸入事件之間(Race #352,Race#12),一部分發生在IPC 事件之間(Race #784,Race #8).這些數據競爭數量比較多,但都沒有造成嚴重后果.

我們發現,在OI File Manager 中存在由空引用(使用了已經釋放的對象)所導致的有害數據競爭,但是EventRacer 沒有檢測出來.圖3 展示了相關信息.類MultiDeleteDialog 是一個Fragment,綁定在相應的Activity并繼承了DialogFragment.它展現了一個界面,用戶可以進行相應的操作.當用戶點擊確定按鈕,會創建一個異步執行的任務,即繼承了AsyncTask 的RecursiveDeleteTask 類.在執行異步任務的過程中,主界面會初始化一個進度框,顯示任務執行的進度.具體的執行過程在方法doInBackground(?)中進行.最后會在onPostExecute(?)方法中執行dismiss(?)方法中止進度框.但是如果用戶在任務執行過程中,點擊回退按鈕,則可能造成數據競爭.

在真實場景下,由于用戶可在任何時刻按下回退按鈕(其他操作也可能觸發onDestory等回調函數,這里僅以按下回退按鈕舉例),繼而onPause(?),onStop(?),onDestroy(?)回調方法會被調用銷毀Activity,繼而銷毀進度框(進度框是在嵌入在Activity 上繪制的,彼此共享同一個共享變量window).因此,當異步任務執行完成進而調用dismiss(?)方法銷毀進度框時,就會獲得一個空對象,進而引發異常,導致應用崩潰.

工具EventRacer 默認使用工具AndroidMonkey(http://developer.android.com/tools/help/monkey.html)產生300 個隨機事件去觸發相應的回調方法獲取執行軌跡.這些隨機的事件只能覆蓋到應用中一部分代碼.因此,EventRacer 會遺漏許多數據競爭,即存在漏報.如果增加隨機事件的數量,則EventRacer 的性能會急劇下降.

Fig.3 Harmful data races in application OI File Manager圖3 應用OI File Manager 中的有害數據競爭

這個案例說明了動態分析技術的局限性,即現有的檢測工具存在漏報的問題.為此,本文通過靜態分析去識別所有的疑似數據競爭(符合數據競爭第1 個條件),即在不同的線程中訪問同一個共享變量的2 個語句.此階段會覆蓋所有的源碼,達到最大的覆蓋率.在此基礎上,依據安卓應用中的發生序規則去檢查每個疑似數據競爭是否有同步措施,通過將其上下文語句轉化為相應的約束條件,編碼后放入Z3 求解器進行計算,從而檢測出盡可能多的數據競爭,并對其中有害數據競爭進行分析.

3 檢測工具的設計與實現

本節首先概述工具RaceDetector 的構成,繼而詳細描述各組成模塊:安卓共享變量分析、可疑的數據競爭集合分析、約束求解.

3.1 概述

圖4 概述了工具RaceDetector的工作流程.頂部方框展示了處理模塊,底部的方框則展示了相應輸入以及輸出的數據結構,虛線箭頭展現了輸入關系,實線的箭頭展現了輸出關系,最后的方框展現了工具RaceDetector 的輸出結果.在圖4(a)中,RaceDetector 使用工具SOOT(一個安卓代碼分析框架,支持別名分析、SSA 分析和Jimple格式)解析識別安卓應用的APK 文件,進而匹配識別相應的語句.在圖4(b)中,主要進行靜態分析,記錄相關的組件信息、進程信息、共享變量信息和回調方法信息.根據圖4(b)中記錄的信息以及安卓框架的發生序規則,在圖4(c)中進行約束條件的編碼.最后,在圖4(d)中使用z3 求解器去識別真正的數據競爭,并分析得出數據競爭報告.

Fig.4 Workflow of RaceDetector圖4 RaceDetector 的工作流程

3.2 安卓線程共享變量分析

在并發程序中,導致數據競爭的根本原因是沒有處理好對共享變量的讀寫操作.對共享變量的操作進行分析是先決條件,也是靜態解析的第1 步,其分析結果也是提高檢測性能和準確性的關鍵[26].EventRacer、CAFA、DroidRacer 等工具根據逃逸分析[26]在執行軌跡上進行安卓線程共享變量分析.逃逸分析方法用于判斷一個分配的對象作用域是否逃逸出創建它的方法或線程,即一個變量的作用域是否在多個線程之間.但是一方面,這些工具是基于執行軌跡,有著其動態執行固有的低覆蓋率問題;另一方面,傳統逃逸分析的局限性也影響其性能.

(1)一個線程逃逸的對象可能不會被多個線程訪問,例如靜態變量通常被視為逃逸的,但是大部分靜態變量只被訪問在當前線程中.

(2)一個對象是線程逃逸的并不意味著所有與此對象相關的數據都是共享的.

(3)一個線程逃逸的對象可能是不可變的,因為在初始化之后,沒有語句對它進行寫操作.

因此,傳統逃逸分析中所定義的共享變量,在實際情況下,有一些共享變量并沒有真正被多個線程訪問.因此,合理優化共享變量分析的方法,識別出真正被多個線程共同訪問的共享變量,不僅能提高準確性,而且能夠降低工具分析問題的復雜性.

共享變量是指一個變量的作用域超出定義這個變量的所在線程.在安卓應用中,除常規意義下的共享變量外,還需擴展Java 語言中的線程共享類型,以覆蓋安卓應用特有場景.若符合以下情況之一,均為安卓共享變量.

(1)View 和Component:用來定義UI 界面的組件,例如TextView、EditText、ImageView 等.

(2)Window(窗口):在此基礎上定義了可視化的界面,例如Activity、Dialog 和Toast,它們共享同一個變量window.因此,當Activity 被銷毀時,Dialog 和Toast 也同樣會被銷毀.

(3)數據存儲:包括Internet、SharedPreference、Sqlite、Content Provider 和SD card.

安卓共享變量給出了在安卓中可以在多個線程之間共享的變量類型,但是在實際情形中,可以在多個線程之間共享的變量很多,而真正在多個線程之間共享的變量的數據則很少.因此降低共享變量的分析空間,識別出真正在多個線程之間共享的變量,有助于提高整體的性能.

定義1(安卓線程共享變量分析(ATSA)).在安卓應用中,對共享變量的操作即為安卓線程共享變量分析(決定安卓應用中程序語句是否讀取或寫入一個線程共享數據).在安卓應用中,變量v定義在線程T中,如果v的作用域D超出線程T,則認為變量v是線程可共享變量.如果存在2 個語句s1和s2,在不同的線程t1和t2中對變量v進行訪問,并且有一個為WRITE 操作,則認為該變量是線程真實共享變量.從可共享變量中獲取真實共享變量的過程,稱為安卓線程共享變量分析.

具體操作時,使用工具SOOT 解決Java 語言的別名問題,并且基于三地址碼格式的Jimple 語句,可識別每一個語句的變量讀寫情況.因此,使用SOOT 首先獲取所有的可共享變量,在解析源碼時,使用全局的Map 記錄對可共享變量進行讀寫操作的線程和語句信息,用于標記;繼而集成靜態優化算法到傳統的逃逸分析中[26],并識別安卓特有的場景,然后過濾掉并沒有真正在多個線程之間傳遞的共享變量,從而獲取真實共享變量的集合.具體過程如算法1 所示.

算法1.安卓線程共享變量分析(ATSA).

定義2.線程真實共享變量TSO={O1,O2,O3,…,On},n是線程共享對象的數量.TSO中的每一個對象是一個四元組:O=〈o,ID,ClassName,Type〉,ID唯一標識了真實共享變量對象o,ClassName信息定義了該共享變量o所處的線程信息,Type信息則定義了該對象o的類型(View、Window、數據存儲或傳統線程等).例如,在圖2 的示例OI File Manager 中,真實共享變量為O1=〈window,ID(獨特整數標識),RecursiveDeleteTask(AsyncTask),Window〉.

3.3 可疑的數據競爭候選者集合

上文根據數據競爭第1 個條件去獲取可疑的數據競爭候選者集合.本節首先對真實共享變量進行讀寫分析,針對每一個真實共享變量,得出對該真實共享變量進行讀寫的回調方法集合.

讀寫函數集合FS=〈F1,F2,…,Fm〉,m為FS集合中語句的數量.F為一個四元組:

?f是對真實共享變量o進行讀寫操作的回調方法,在該回調方法中,存在多次對真實共享變量o進行讀寫操作的語句.

?ID和ClassName分別定義了讀寫函數的唯一標簽和讀寫函數所處的線程類信息.

?SourceEvent是一個輸入事件,觸發了該回調方法的執行,通過逆向查找匹配確定,即在確定觸發該回調函數的用戶輸入事件時,如果是用戶輸入事件,會事先注冊事件監聽(每個Event 都有對應的Listener),通過Listener 關聯到回調函數,將可能的情況一起放在列表中,然后逐一確認.

具體到例子OI File Manager,存在兩個F,分別為F1=〈onDestroy,ID1,MultiDeleteDialog(Activity),back〉,F2=〈onPostExecute,ID2,RecursiveDeleteTask(AsyncTask),Button.onClick〉.針對每一個真實共享變量o,對應著多個對它進行讀寫操作的回調函數F.為此,給出了定義3 來表示這種關系.

定義3.函數活動FA=〈TID,F,O,H〉.回調方法F.f產生于F.SourceEvent,在TID標志的線程中,對共享變量O.o執行讀寫操作H(READ,WRITE),由此產生了函數活動集合.具體到OI File Manager,函數活動對為FA1=〈TID1,F1,O1,WRITE〉和FA2=〈TID2,F2,O1,READ〉.然后,根據定義4 疑似數據競爭判定規則,即數據競爭定義的第1個競爭條件,最終識別出可疑數據競爭候選者集合.

定義4(疑似數據競爭判定規則).若FAi=FA(TIDi,Fi,Oi,Hi)∧FAj=FA(TIDj,Fj,Oj,Hj)∧TIDi!=TIDj∧Oi=Oj∧(Hi=WRITE∨Hj=WRITE),即〈FAi,FAj〉發生在多線程之間,則為疑似多線程數據競爭;若〈FAi,FAj〉發生在一個線程和相關的監聽者之間并滿足上述條件,則為疑似單線程數據競爭.

由此產生數據競爭候選者集合Data Race Candidate Set(CS),CS的每一個元素是一個函數活動對〈FAi,FAj〉,如OI File Manager 的〈FAi,FAj〉,這個函數活動對發生在主Activity 線程和相對應的Listener 之間,且滿足定義4,因此為單線程數據競爭.

3.4 約束求解

安卓應用中的發生序關系(happens-before,簡稱HB)形成了語句之間執行的約束關系[18,27,28].文獻[10]首次把HB 關系應用到安卓系統中,文獻[9]擴展了HB 關系.它們基于安卓應用中的HB 關系構造全局的HB 關系圖,進而去診斷2 個共享變量讀寫操作是否滿足HB 關系.這些方法是基于動態執行的路徑構造HB 關系圖,覆蓋率低.如果構建全局HB 關系圖,則會嚴重影響性能.

得到包含相應的共享變量、線程ID、方法語句、讀寫操作等信息的可疑的數據競爭集合之后,根據這些信息進行約束編碼,借助求解器生成所有可能的線程調度方案,從而找出真正的數據競爭.對每一個可疑數據競爭候選者,基于它們的上下文構造局部HB 關系圖,能夠輕量地檢測到盡可能多的數據競爭.

針對安卓應用事件(指除去SDK 提供的已有規則確定事件外的用戶事件和其他事件)回調方法,有定義5.

定義5(事件回調方法之間的次序關系).

(1)同一個事件產生的多個回調方法之間是有序的.

(2)不同事件產生的回調方法之間是沒有HB 關系的.

(3)事件的觸發會調用相應的回調方法.然而事件的觸發是不可預計的,因此事件之間是沒有HB 關系的,事件所對應的回調方法之間也沒有HB 關系.

因此,對于可疑的數據競爭候選者〈FAi,FAj〉,由于它們的觸發事件不同,FAi和FAj之間是沒有HB 關系的.因此,如果沒有額外的同步機制,則FAi和FAj可能引發數據競爭.我們使用約束求解的方法來識別FAi,FAj的上下文中是否有額外的同步措施.

約束編碼廣泛應用在程序中數據競爭的檢測、再現和修復[29-31].基于安卓平臺以及事件驅動特性和多線程模型,本文提出了以下相關約束:變量約束、條件約束、讀寫約束、數據競爭約束、同步約束.這些約束模擬了所有Java 語言程序語句的特性.首先給出約束系統的基本概念.

(2)符號變量Ok表示語句k的調度順序.

變量約束定義了賦值語句和定義語句中對共享變量的讀寫約束.針對共享變量x,位置i語句x=v,表示為;語句x=y在i位置,并且y變量定義在j位置,表示為;語句z=x⊕y(⊕表示標準的二元運算符,例如加減乘除等),x定義在位置j,y定義在位置k,語句發生在位置i,表示為zi=xi⊕yi∧xi=xj∧yi=yk.

條件約束定義了條件語句中的約束情況.對于語句if(z),會檢查條件z的值,進而去判斷相關的分支語句塊是否被執行,表示為:z∧z是一個條件語句.

讀寫約束定義了所有對共享變量進行讀寫操作的語句約束情況.對于一個共享變量x,讀操作所得到的值等于之前最近一次對x寫操作寫入的值.因此,如果位置i讀取的值等于位置j寫入的值,則(Oj?Oi),并且對于位置k對x的寫操作,則有(Ok?Oj)或者(Oi?Ok).表示為

數據競爭約束定義了兩個特殊的語句次序約束,這兩個語句共享同一個共享變量,并可能導致數據競爭的發生.對于語句i和j,如果它們訪問同一個共享變量,并且其中一個是寫操作.同時我們想去確定這兩個語句之間有沒有HB 關系.定義其數據競爭約束為.

同步約束包括線程內同步、鎖同步、Start/Join/Wait/Notify約束以及安卓中特殊的同步方法,具體介紹如下.

(1)線程內同步:同一個線程中,所有的語句都是順序執行的,表示為O1?O2?…?On.

(3)Start/Join/Wait/Notify約束:Start/Join/Wait/Notify是Java 語言中用于同步線程常用的操作,Start的操作用于開啟運行一個新的線程,Join操作用于通知該線程已經執行完畢;Wait操作用于等待獲取一個鎖,Notify操作用于通知已經釋放了鎖.因此,表示為Start?Join,Wait?Notify.

(4)安卓中特殊的同步:對安卓HB 規則約束編碼,對于兩個語句i,j,如果它們遵循HB 規則,有Oi?Oj.

例如,我們會檢查如下線程間同步機制:startActivity,startService,AsyncTask.execute,addListener等,并用methodinit(m),methodexit(m)表示開始執行當前方法和已經執行完畢當前方法.

對所有的語句進行約束編碼之后,將得到關于可疑數據競爭候選者的約束文件.約束文件中,首先,對約束變量進行定義;其次,根據以上規則對數據競爭候選者的上下文語句進行編碼;最后,將約束文件放入Z3solver(https://z3.codeplex.com/)中去檢測是否有解,從而去識別真正的數據競爭.

具體到本文示例OI File Manager,首先,通過線程共享變量分析,可以定位到共享變量window,根據共享變量相關的上下文以及其讀寫集合,可以得到兩個事件回調方法onDestroy(?)和onPostExecute(?),對這兩個回調方法對語句進行約束編碼.具體到super.onDestroy(?)和dialog.dismiss(?),可以得出window(write)=null和y=window(read);同時,設定它們的調度序列O1,O2.針對數據競爭約束條件,可以將此編碼為O1=O2,然后把兩個語句相關的約束語句和數據競爭約束O1=O2輸出到一個約束文件中,并放入Z3 求解器中進行求解,去判斷數據競爭約束在安卓并發語義的Happens-Before 規則下面是否真實發生,即在所有的事件調度和線程調度解空間中是否有解.如果有解,則認定它們為數據競爭.

4 實驗分析

本節主要介紹工具RaceDetector 的實現、數據集、實驗及其結果分析,并結合案例討論與現有工具的異同.

4.1 工具RaceDetector的實現

本文使用Java 語言實現了工具RaceDetector.靜態分析模塊通過靜態解析整個安卓應用APK 文件來大幅度地提高源代碼的覆蓋率.這里使用SOOT 工具將APK 文件轉換為三地址碼(Jimple 格式)的簡單語義文件,繼而進行安卓應用線程共享變量分析,并優化了傳統的逃逸分析算法(第4.2 節).根據線程共享變量,得出該共享變量的讀寫語句集合,從而得出數據競爭候選者集合(第4.3 節).在約束求解模塊中,我們根據安卓應用的先后序關系規則對疑似數據競爭對應的兩個代碼片段進行約束編碼,得到一個定義了兩個代碼片段發生序關系的約束文件,并通過Z3 求解器求解,判斷有數據競爭約束的兩個語句是否有HB 關系,從而找到真正的數據競爭.

本文借助了兩個輔助工具——SOOT 和Z3 求解器.

?SOOT 是一個可以分析安卓應用程序的框架平臺,能夠將安卓應用的APK 文件解析為三地址碼格式.SOOT 還提供了別名分析和數據流分析等常用的靜態分析方法.SOOT 工具的API 可以識別安卓應用每一個類的信息、屬性信息、方法信息以及類與類之間、方法與方法之間的調用信息,從而可以進行線程共享變量分析和疑似數據競爭分析.

?Z3 求解器是一個在廣泛的解空間中檢測某些約束條件是否有解的工具.它接受一系列的約束條件作為輸入.這些約束條件定義了相關變量之間的關系.針對數據競爭的約束文件,Z3 求解器輸出SAT,表明兩個包含數據競爭約束條件的語句并沒有違反安卓應用中的先后序關系規則,也即這兩個語句之間沒有先后序關系,因此它們是數據競爭.

4.2 數據集

本文根據以下標準挑選出了15 個流行的App 作為數據集.

(1)廣泛流行.這些App 來自Google Play Store 排行榜的前列,或者來自于其他論文中的數據集[8-10].

(2)不同的類別,包含了媒體、工具到社交、新聞等類別.

(3)不同的大小,小的有8k 多行,大的有400k 多行(這里是按照Jimple 格式顯示的代碼行).

表1 展示了這些App 的相關信息,按照Jimple 格式代碼行的大小,從小到大進行排列.表1 的第2 列是代碼行數.第3 列展示了每一個App 中的線程共享變量,斜線左邊的是可共享變量的數目,右邊是經過ATSA 實際得出的、真實的共享變量數目.可以看出,線程可共享變量廣泛存在于App 中,數量從幾百到幾千不等.但是真實共享變量數目遠遠小于可共享變量數目.第4 列～第7 列分別是安卓應用的活動、服務、異步任務和線程的數量信息.這些信息展現了每一個應用中的線程數量:安卓應用中,每一個活動都運行在主線程;每一個服務代表了一個在后臺執行的任務;AsyncTask 是安卓應用中發起異步執行任務的框架;Thread 則是傳統的Java 語言線程.最后一列是監聽器Listener 的數目,每個監聽器Listener 會監聽相應的輸入事件,并引發一個或者多個回調函數的執行.

由此可見,大小應用中均存在多線程運行的場景,即多線程在安卓應用中是普遍存在的.每個應用都有相應的監聽者,對應著各種輸入事件,并且輸入事件的類型多且復雜.因此,輸入事件的不可預期性、無序性以及相互之間的調度也是數據競爭問題產生的原因.

Table 1 Information statistics of data set表1 數據集信息統計

4.3 實驗結果分析

本文實驗均使用處理器為Intel Core i5-4570 3.20GHz、內存為8GB、操作系統為64 位Windows 7 專業版的計算機所完成.實驗工具由Java 語言來實現,使用的開發環境為JDK 7.0,使用的IDE 為Eclipse Kepler.靜態分析部分的功能使用了SOOT 工具輔助,約束求解部分使用了Z3 求解器.表2 展示了相應的實驗結果.

Table 2 Information statistics of experimental results表2 實驗結果信息統計

表2 的第2 列展現了工具的執行時間,包括線程共享變量分析的時間、約束編碼的時間和求解器求解的時間.可以看出,工具的執行時間隨著應用大小近似線性增長.對于小的應用,RaceDetector 基本都在1min 內完成任務.執行時間最短的應用是Tomdroid,僅需要6.3s.在表2 的底部區域,對于大的應用來說,執行時間幾乎都超過了1min,最慢的應用是Pandora,其執行時間超過了3min.除此以外,我們發現執行時間也受到共享變量、數據競爭候選者數目的影響,例如,Instagram 是15 個應用中最大的,與Pandora 相比,其執行時間少了近1min.這是因為它的數據競爭候選者數目(42)遠小于Pandora 的候選者數目(239).另外我們發現,約束求解執行的時間平均在1min 左右,約束編碼占據了大部分時間.這是因為我們把全局的先后序關系約束分解為針對每一個候選者的約束文件,有效降低了約束求解的執行時間.隨著候選者數量的增多,約束求解執行的時間也隨之增長.

表2 的第3 列是經過ATSA 分析過后得到的實際情況下線程間共享變量的數目.在安卓應用中,開發人員經常會定義作用域超出自身所在線程或者自身所在類別的對象,但是實際情況下,真正能夠被多線程共同訪問的共享變量數目是極少的.因此,優化后的ATSA 分析方法極大地降低了需要分析的共享變量數目,減少了程序的空間消耗和時間消耗.

表2 的第4 列是可疑的數據競爭候選者(函數對)數目,對照表2 的第3 列可以看出,可疑的數據競爭候選者數目大于線程共享變量的數目,即每一個線程共享變量會存在多個數據競爭候選者.因此,會存在許多個線程或者Listener 共同訪問同一個共享變量.每一個數據競爭候選者對應一個函數對,符合數據競爭定義的第1 個數據競爭條件,針對每一個函數對,我們會產生一個約束文件,并放入求解器中進行求解.

表2 的第5 列～第8 列展現了具體檢查出的數據競爭結果.本文將數據競爭分類成單線程數據競爭和多線程數據競爭,并識別出其中有害的數據競爭(第8 列).根據實驗結果,可以得出以下結論.

(1)相對于安卓應用中的單線程數據競爭,多線程數據競爭的數目更多.

(2)每個函數對代表了針對一個共享變量的約束文件,平均每個約束變量都會引發5 個以上的數據競爭.

(3)在數據競爭中,我們關心的有害數據競爭(空引用)僅占據很小的比例.

(4)針對每個應用,RaceDetector 平均報告了340 個數據競爭.針對應用Pandora 檢測到的數據競爭最多,達到1 939.結合表1 和表2 可以看出,Pandora 應用使用了大量的線程并發執行代碼.

表2 的最后一列展現了誤報的數據競爭的數目,平均的誤報率為13%(44/340).誤報的數據競爭數目是通過實驗過后人工審查分析得出的結果.我們對這些誤報的數據競爭特性進行了總結,具體原因分析如下.

(1)一些數據競爭發生在用戶代碼和安卓系統API 調用之間,表現為多個線程共同訪問同一個共享變量,訪問的語句直接或間接調用系統API.我們認為:這些數據競爭對線程共享變量進行了讀或寫的操作,沒有同步措施.而真實情況是,系統API 對線程共享變量已采取了相應的同步措施.由于本文未解析安卓API 代碼,因此產生誤報.

(2)單線程數據競爭往往發生在活動Activity 和與相關的Listener 所觸發的回調方法之間,但只有當活動處于前端時,用戶才可執行交互;同時,工作線程不能改變主進程UI 組件的狀態.具體展現的是在某些Listener 所監聽的事件處于活動進行前后臺切換情況下,處于前端的Activity 會轉入后臺,并觸發調用一些回調方法進行資源的釋放和銷毀.在實驗中,我們未覆蓋到相關事件類型所導致的額外回調方法的執行,因此產生誤報.

(3)數據競爭檢測階段所使用的Happens-Before 規則和安卓應用的并發語義是基于前人的相關工作,但是隨著安卓系統的發展和更新,Happens-Before 規則和并發語義并沒有全方位覆蓋到.因此在實際排查中,我們發現具體實驗過程中會遺漏一些Happens-Before 規則.

4.4 案例討論

表1 已列出的線程類型有5 種:活動(activity)、服務(service)、Thread、AsyncTask、Listener.我們進一步統計了不同線程類型之間的數據競爭,詳見表3.

Table 3 Information statistics of data race types表3 數據競爭類型信息統計

在所定義的數據競爭中,數據競爭可以發生在不同的線程之間.由于安卓應用存在多種類型的線程框架,根據發生數據競爭所在的兩個線程的不同類型,具體有8 個類型:Act-Lis、Act-ST、Act-Async、ST-ST、ST-Async、ST-Lis、Async-Async、Async-Lis(Act:Activity,ST:Service 或者 Threads,Async:AsyncTask,Lis:Listener).因為AsyncTask、Service 和Thread 可以運行在后臺,而Listeners 一部分與Activity 綁定,一部分與Sensor 綁定.

表3 表明,Activity、Service、Listener 間的數據競爭占據很大比例,數據競爭大多集中在Act-Lis、Act-ST、ST-ST、ST-Lis 這幾個類型,說明了Listener 執行的不可預計性.我們選取數據集中的3 個應用進行案例討論.

?OI File Manager

在表2 中,RaceDetector 報告了11 個數據競爭,其中有8 個有害數據競爭.它們發生在Activity 和AsyncTask之間.當Activity 正在執行異步任務時,會訪問一個Dialog,這時用戶可能按下回退按鈕中止Activiy,同時中止相應的Dialog.這樣,正在進行異步任務的AsyncTask 訪問Dialog 時會獲取一個null 值,從而導致有害數據競爭的發生.

?Connectbot

數據競爭發生在Activity 和Listener 之間.這個應用里,一個數據庫用來存儲數據,相應Listener 會監聽數據庫狀態,從而會更新數據競爭的狀態.大部分數據競爭發生在Activity 和Listener 的回調方法之間,多數為讀取數據庫狀態的操作,其中存在兩個有害數據競爭,都涉及到了對數據庫的寫操作或者對數據庫進行銷毀的操作,具體發生在Activity 的onStop(?)方法和Listener 的回調方法之間.一旦用戶操作導致Activity 的中止,onStop(?)方法會銷毀數據庫,此時數據庫更新數據的操作會獲取到一個null 值,從而導致有害的數據競爭.

?Music

這是一個音樂播放的應用,用戶可以改變Music 音樂播放器的狀態或者下載更新相關的音樂.所導致數據競爭發生的核心共享變量由一個表示音樂播放器的狀態變量state所導致.該應用中,有多個線程擁有訪問該狀態變量的權限.多數的數據競爭為正常的更新狀態變量來改變應用的狀態,并不會導致有害的行為.有害的數據競爭發生在后臺任務下載音樂和播放音樂之間,當發起一個后臺任務下載音樂時,用戶的不同操作會導致應用處于前臺的不同狀態.當后臺任務下載完成更新數據時,如果用戶銷毀相關頁面,將會導致數據競爭.

通過分析上述應用中數據競爭產生的具體情況可知,多線程并發執行任務是安卓應用中常見的場景,如果沒有完善的同步措施,數據競爭很可能發生并導致不同程度的危害.

4.5 工具對比

本節將對相關的安卓應用數據競爭檢測工具進行比較和分析,包括CAFA、DroidRacer 和EventRacer.

(1)分析方法和覆蓋率

DroidRacer、CAFA 和EventRacer 使用動態分析方法進行建模,對原App 插樁,并動態執行App 獲取相關的執行軌跡.其中,CAFA 主要檢測空指針異常所導致的數據競爭;DroidRacer 主要關注發生在用戶代碼中的事件交互所導致的數據競爭;EventRacer 不僅識別了用戶代碼中的數據競爭,同時也對安卓框架SDK 進行了分析.但是動態分析覆蓋率較低,尤其在安卓應用中,一方面,一次動態執行很難觸發所有事件去覆蓋回調方法;另一方面,一次事件執行的軌跡是固定的,但多線程的事件和線程調度是不確定的,如果要觸發更多的執行軌跡,將會顯著增加性能消耗.

考慮到動態分析方法在覆蓋率方面的缺陷,RaceDetector 使用了靜態分析方法,能夠保證具有較高的覆蓋率,另外還使用了約束求解方法去動態生成所有可能的事件和線程調度.

(2)執行軌跡的產生和性能

CAFA、DroidRacer 和 EventRacer 都是通過插樁并執行 App 來獲取執行軌跡.這里,我們詳細分析EventRacer 工具.EventRacer 通過AndroidMonkey 產生隨機的輸入事件觸發App 的執行,相關的命令為adb shell monkey–s 42–throttle 60–v 1000.這里產生了1 000 個輸入事件,運行時間在1min 左右.隨著輸入事件的增加,執行時間也會相應增加.由于這些事件是隨機產生的,而安卓應用中界面的跳轉往往需要觸發特定的事件,因此隨機事件存在大量的冗余,通常只是在固定的幾個界面中執行重復的動作,而不能執行特定事件,進而覆蓋到其他界面.

相反,RaceDetector 抽取所有組件、線程和事件回調方法信息,并檢查所有的事件回調方法間是否會滿足數據競爭定義的第1 個條件;另外,還通過求解器判斷是否滿足數據競爭定義的第2 個條件,保證覆蓋率和性能.

(3)模型

CAFA、DroidRacer 和EventRacer 都使用發生序HB 模型,它們構建了全局HB 圖.其中,EventRacer 擴展了CAFA 和DroidRacer 的HB 圖,并優化了圖查找識別算法.它們所構造的HB 圖是基于動態執行產生執行軌跡.

與此相反,考慮到構造一個全局的HB 模型會對性能產生很大的影響,RaceDetector 對每一個可疑的數據競爭候選者上下文構建局的HB 圖,即把全局的HB 圖劃分為多個小的局部HB 圖,優化了算法和執行時間.

(4)實驗結果

我們使用EventRacer 和RaceDetector 對本文的數據集進行了對比實驗.因為相關安卓平臺和版本的差異,數據集中的部分應用無法直接進行對比,最終6 個應用的比較結果展現在圖4 中.所有的實驗都是在EventRacer默認的設置下進行的,EventRacer 默認設置產生300 個輸入事件去獲取執行軌跡.

表4 的第1 列顯示了6 個應用名稱.第2 列顯示了EventRacer 和RaceDetector 執行時間.EventRacer 的執行時間包括以下幾個部分:啟動安卓模擬器、執行App、檢索執行軌跡文件、分析執行軌跡文件.EventRacer的平均執行時間約為50s.這是由于其默認生成的300 個輸入事件數量較少,事實上,某些App 的Listeners 就已經遠遠超過了300 個.如果EventRacer 產生更多隨機事件去覆蓋Listeners,相應的執行時間也會大為增加.RaceDetector 分析小的安卓應用只需要極少的時間,最少的OI File Manager 只需要8s.RaceDetector 平均需要49.2s 的執行時間,但考慮到RaceDetector 覆蓋了全部的Activity、Thread 和Listeners,這個時間還是可以接受的.

Table 4 Data race detection reports by EventRacer and RaceDetector表4 EventRacer 和RaceDetector 檢測的數據競爭報告

表4 第3 列～第6 列是詳細的數據競爭信息.EventRacer 對數據競爭劃分了4 個不同的類型.

EventRacer 和RaceDetector 檢測到的數據競爭總數在第7 列.我們可以看出,RaceDetector 檢測出的數量遠遠小于EventRacer.這是由于RaceDetector 只檢測了用戶代碼,EventRacer 檢測了用戶代碼和安卓相應版本的SDK 代碼.然而,安卓SDK 對線程共享變量已經做了很好的同步,沒進行同步的是良性的數據競爭,對App 的行為并沒有有害的影響.

表的最后一列顯示了有害的數據競爭,可以看出,EventRacer 檢測出的數據競爭中,有害的數據競爭極少.相反,RaceDetector 檢測出的有害數據競爭則占據一定的比率.具體對于OI File Manager 和Tomdroid,EventRacer分別報告了785 個和1 605 個數據競爭,沒有一個是有害的數據競爭.相反,RaceDetector 報告了11 個和106 個數據競爭,其中,對于OI File Manager 有8 個有害的數據競爭,對于Tomdroid 有3 個有害的數據競爭.

針對Pandora,可以發現,RaceDetector 報告的數據競爭超過了EventRacer 報告的數據競爭.這是因為對于小的應用,EventRacer 通過分析執行軌跡和安卓SDK 能夠分析出較多的數據競爭.我們靜態檢索了所有的用戶代碼,但是應用小,報告的數據競爭也少.對于Pandora,它是一個大的安卓應用.僅僅檢索用戶代碼,RaceDetector 報告的數據競爭就超過了EventRacer.因此對于越大的應用,EventRacer 將會遺漏更多的有害數據競爭.本次對比實驗中,與RaceDetector 相比,EventRacer 平均遺漏了近20 個有害的數據競爭.

5 相關工作

?數據競爭檢測方法

早期的數據競爭檢測方法是基于鎖的[16,32,33],最有代表性的工具為Eraser[33].但是基于鎖的數據競爭檢測方法屬于保守策略,有很嚴重的誤報問題(false positive).另一種數據競爭檢測方法是基于HB 關系[18,27,28].不同的工具通過靜態或者動態分析構造HB 圖.基于靜態分析的數據競爭檢測方法[1,11,12,14,15,20,34]有很好的覆蓋率,因為它們能夠解析所有的源碼和執行路徑;但存在誤報問題,因為無法確定動態加載的代碼和實際執行的路徑選擇.與此同時,覆蓋率的提高意味著性能的下降,解析全部的源代碼在大規模應用中對性能有嚴重影響.如何平衡、取舍,也是靜態分析方法所面臨的挑戰之一.基于動態分析的數據競爭檢測方法適合用于大的數據集,并且能夠產生比較精確的結果,但會受到低覆蓋率的影響,因為通過執行程序所獲取的上下文信息只能覆蓋很少的一部分代碼,會面臨漏報問題(false negative).綜合了靜態分析和動態分析的優點,基于預測性分析的數據競爭檢測方法[29-31,35,36]從動態分析出發獲取執行軌跡,進而分析執行軌跡所依賴的限制條件,在遵循限制條件的前提下,采取策略改變語句和線程的調度,生成新的執行軌跡,從而提高覆蓋率,既緩解了靜態分析的誤報問題,又緩解了動態分析的低覆蓋率問題.還有基于causally-precedes(CP)的方法[37],能夠避免誤報,但還是會有漏報.文獻[38]進一步將抽象的控制流信息引入到執行模型中,彌補了HB 和CP 方法的不足,增加了解空間.本文擴展了預測性分析中的約束求解方法,并結合靜態分析、共享變量逃逸分析和優化的HB 圖,實現了RaceDetector.

?安卓應用數據競爭檢測

針對安卓應用中數據競爭,文獻[10]首次形式化出了安卓應用中的并發語義,總結出了安卓應用中的HB 關系,并針對多線程代碼片段以及安卓中特有的單線程代碼片段,構建了安卓應用的HB 圖.基于動態插樁技術和HB 模型,文中實現了相關工具DroidRacer.文獻[9]基于安卓應用中的事件驅動模型系統,實現了工具CAFA,動態地獲取安卓應用的執行軌跡并分析檢測數據競爭.EventRacer[8]擴展了DroidRacer 的HB 模型,并優化了檢索算法.但是這些工具都是基于動態分析方法,存在固有的低覆蓋率問題,尤其針對安卓應用,除了線程發生序關系,還面臨定位事件發生序和事件發生時機的挑戰.因此,現有的安卓并發語義和發生序關系在真實面臨復雜的事件操作和線程調度往往也存在嚴重的誤報問題.除此之外,這些方法構造了全局的HB 圖,很難處理大的應用程序.即在安卓應用中檢測數據競爭,采用靜態分析所面臨的問題是如何平衡好覆蓋率和性能,并需要對性能進行優化,為此,我們進行了共享變量分析以縮小范圍;應用動態分析將面臨低覆蓋率的問題,因為安卓應用是基于事件驅動的,相對于傳統的多線程程序,安卓應用的一次動態執行只能覆蓋很小比例的事件,為此,我們采用約束求解的方法來提升覆蓋率.

6 總結

本文主要研究了安卓應用中數據競爭這類并發缺陷,針對現有工具的不足,本文提出了改進的方法.

我們首先使用SOOT 工具解析安卓應用的APK,并記錄共享變量信息和線程、安卓組件等必要信息.針對線程共享變量信息,我們集成了安卓應用中的共享變量,并優化了傳統的共享變量分析方法:逃逸分析.提出了安卓線程共線變量分析方法ATSA,可以使得實際的線程共享變量數目遠遠小于可能的線程共享變量數目,極大地縮小了RaceDetector 的分析空間并提高了執行性能.繼而,我們形式化定義了可疑的數據競爭候選者集合,并針對每個可疑的數據競爭以及其上下文進行約束編碼.在約束編碼階段,我們集成了安卓應用中的Happens-Before 規則,并提出了局部的Happens-Before 圖.約束編碼之后,我們將產生的約束文件放入Z3 求解器中進行求解,Z3 求解器覆蓋了所有的事件調度和線程調度,極大地提高了RaceDetector 的覆蓋率.

相對于現有工具,本文所實現的RaceDetector 能夠有效檢測數據競爭,同時,我們的工作還存在一些不足之處:RaceDetector 通過SOOT 進行相關分析,相關的性能受到SOOT 的限制,SOOT 不能解析動態加載的代碼,并且針對部分App 會出現分析失敗的結果;同時,RaceDetector 基于現有的工具所提出的并發語義和Happens-Before 進行HB 關系分析,相關的性能和準確性也受此影響;另外,針對有害的數據競爭,我們并沒有準確定義它和良性數據競爭的邊界,我們只是從空引用這一個角度對有害數據競爭進行了定義和分析.因此,還需要更深入的研究和探索.

由于精力有限,本文未關注Android SDK 框架層代碼中的數據競爭.原因在于,一是框架層已經具備了很好的同步措施,技術相對成熟,并發缺陷較少,而應用層主要由用戶的代碼構成,代碼快速迭代很容易產生并發缺陷;二是SDK 框架層代碼中即使有并發缺陷,也不易修改(因為SDK 框架層過于復雜),但用戶層的用戶代碼可以修改并完成之后的修復工作.后續我們將繼續進行安卓應用數據競爭重現和修復的研究.