基于Pi演算的Android多線程程序的數(shù)據(jù)競爭檢測

，

(1. 河北科技師范學院工商管理學院，河北秦皇島066004；2. 燕山大學信息科學與工程學院，河北秦皇島066004)

移動設備大多資源受限，為了能在其上流暢運行具有豐富功能的應用程序，Android等主流平臺廣泛采用了多線程等技術，有效降低了應用程序的響應延遲并提升了其并發(fā)執(zhí)行性能。與傳統(tǒng)應用程序的多線程模型不同，Android系統(tǒng)采用事件驅(qū)動模式，各種來源的輸入(比如UI、網(wǎng)絡、傳感器和Android生命周期等)都有可能觸發(fā)事件，使多線程模型中執(zhí)行的任務按某種規(guī)則以不確定的方式重新排序。這些復雜的并發(fā)特征容易產(chǎn)生數(shù)據(jù)競爭[1-3]等并發(fā)錯誤，糾錯十分困難。

傳統(tǒng)的數(shù)據(jù)競爭檢測技術[4-10]，提供了許多有益的建模理論和檢測方法，但并不適用于Android Apps多線程模型的數(shù)據(jù)競爭檢測。針對Android Apps的數(shù)據(jù)競爭檢測，學者們發(fā)展了靜態(tài)檢測[11-16]和動態(tài)檢測[17-18]的技術。文獻[11-12]采用新穎的方法對移動應用程序進行數(shù)據(jù)競爭檢測，但沒有考慮事件回調(diào)之間的happens-before關系，影響了其檢測精確度，同時存在大量誤報問題。SUN等[13]通過重放技術有效降低了誤報率。HU等[14]對并發(fā)動作及其時序關系進行建模，在降低誤報率的同時提高了檢測效率。FU等[15]提出了將事件回調(diào)之間的時序關系轉(zhuǎn)換為線程間的時序關系的線程化技術，大大降低了誤報率。WU等[16]提出一種流和上下文敏感的時序分析方法，可以檢測線程內(nèi)和線程間的數(shù)據(jù)競爭問題。但靜態(tài)檢測技術固有的狀態(tài)空間爆炸問題，難以突破檢測效率低的瓶頸，使得其實用性不足。文獻[17-18]采用動態(tài)檢測技術，通過采集Android Apps的執(zhí)行路徑信息，基于happens-before關系進行離線檢測，檢測效率高但代碼覆蓋率低，存在大量的漏報問題。因此，如何在多線程和事件驅(qū)動的Android平臺上精確描述和分析Apps中的并發(fā)行為，提高模型精確性的同時不犧牲模型的效率，是Android Apps行為建模與檢測研究過程中亟待解決的關鍵問題之一。

本文針對事件驅(qū)動機制下多線程模型的安全問題，構造一個基于Pi演算的并發(fā)行為檢測模型，并利用該模型對Android Apps中的數(shù)據(jù)競爭問題進行檢測。

1 數(shù)據(jù)競爭問題

圖1給出一個利用AsyncTask加載數(shù)據(jù)的示例AsyncApp。應用程序啟動時，主線程創(chuàng)建一個后臺線程執(zhí)行加載數(shù)據(jù)的異步任務。為了良好的用戶體驗，后臺線程持有MainActivity的引用并使用一個進度對話框(ProgressDialog)顯示加載的進度信息。待加載任務完成，后臺線程將加載數(shù)據(jù)返回到主線程用onPostExecute方法顯示出來，主線程調(diào)用對話框的dismiss方法撤銷對話框資源。如果用戶在數(shù)據(jù)加載過程中觸發(fā)后退操作(點擊導航菜單上的后退鈕)，則MainActivity被銷毀導致狀態(tài)丟失。但AsyncTask還持有MainActivity的引用，待異步任務返回onPostExecute，進度對話框調(diào)用dismiss撤銷對話框資源會引發(fā)NullPointer Exception異常。

圖1 AsyncApp程序示例代碼Fig.1 A motivating example of AsyncApp

由于主線程和后臺線程共享MainActivity數(shù)據(jù)，構成了數(shù)據(jù)競爭關系。UI事件(如點擊導航菜單上的后退鈕、旋轉(zhuǎn)屏幕等)和應用程序的回調(diào)事件并發(fā)，使得MainActivity的onDestroy和主線程的onPostExecute執(zhí)行時序不確定，產(chǎn)生了數(shù)據(jù)競爭問題。

可見，若共享的資源、程序片段被多個方法操作，且其中至少有一個執(zhí)行的是寫操作，則多個方法執(zhí)行次序的不確定就會引發(fā)數(shù)據(jù)競爭問題。

上例中，若onPostExecute總是先于onDestroy執(zhí)行，則不會發(fā)生異常。但Android是事件驅(qū)動的系統(tǒng)，UI事件由用戶隨意觸發(fā)導致了時序的隨機性。針對該問題，一種簡單的解決辦法是在使用共享數(shù)據(jù)之前進行判斷，稱為條件護衛(wèi)原則。如圖1中onPostExecute方法里注釋的if語句，但并不能保證App的開發(fā)者總能遵循該原則，因此需要發(fā)展一種自動進行檢測的方法。

2 擴展Pi演算

由于進程代數(shù)[19-20]可以有效描述并發(fā)行為和消息通信特性，本文將其中的Pi演算[21]作為建模語言，并對其進行擴展，使之適合描述Android Apps且利于編碼實現(xiàn)。下面給出擴展后的Pi演算的語法和語義規(guī)范，定義如下。

經(jīng)過擴展的Pi演算同時具備描述移動性、外部接口通信和內(nèi)部狀態(tài)遷移的能力，適合形式化地表示Android應用程序的執(zhí)行路徑和組件間通信的情況。

將進程P所有的行為跡組成的有限集合記為Ptraces。

定義2跡等價(trace equivalence)。給定兩個不同的進程P和Q，稱進程P和Q是跡等價的，當且僅當Ptraces=Qtraces成立。記為P≈tQ。

定義3α變換(alpha conversion)。將進程中的名字換成新的名字的變換稱為α變換。

一般來說，用于替換的新名字應為進程中原來不存在的名字，若該名字已存在，則須變換進程中的名字，以保證不會出現(xiàn)命名沖突。使用符號{b/a}P表示將P中的名字a替換為b。如P=υba.b，則有{c/a}P=υbc.b，{c/b}P=υca.c，{b/a}P=υb′b.b′。

選定了進程等價定義，就可以確定出相應的遷移規(guī)則。最常用的幾條遷移規(guī)則如下。

(F) SC-RES-COMPυx(P1‖P2)≡P1‖υxP2，若x?fn(P1)

3 形式化建模

與傳統(tǒng)的應用程序不同，Android Apps并不是獨立的封閉程序，需要在Android框架中運行。Android系統(tǒng)(包括Android運行時環(huán)境)在應用程序的代碼之外做了大量的工作。其中，Android系統(tǒng)為了管理應用程序，為每個組件預先定義好生命周期，應用程序可以為生命周期定義回調(diào)函數(shù)和監(jiān)聽函數(shù)。因此，為了得到更精確的模型，需要為Android生命周期構建形式化模型。

3.1 Android生命周期的形式化建模

以Activity組件的生命周期[22]為例，根據(jù)拓展Pi演算的形式化語法和語義，得到模型如下。

上述進程表達式中的τ為不可見動作，在這里指代不可預知的事件。其他組件(Service和Fragment等)生命周期的形式化模型構造方法與Activity組件相同，不再贅述。將這些組件的生命周期并發(fā)演算，得到Android Apps的生命周期的形式化模型。

3.2 多線程的形式化建模

當Apps啟動時，系統(tǒng)會為其創(chuàng)建一個主線程(main thread)來負責和UI組件進行交互。若某個操作比較耗時，就可能阻塞主線程而導致交互卡頓。Android系統(tǒng)主要通過HandlerThread、AsyncTask和線程鎖Lock等機制解決這個問題。

Android中實現(xiàn)多線程的方式有兩種：(a)繼承Thread類，并重寫類中的run()方法，但一個類只能繼承一個父類；(b)實現(xiàn)Runnable接口。無論哪種方式實現(xiàn)，都會出現(xiàn)類似thread tr=new thread(…)和tr.start()的兩條語句。因此，按如下步驟進行形式化映射。

分析thread tr=new thread(…)類似語句及其上下文，確定新建線程tr的類名稱son和線程類所在基本塊。在這條語句的上文搜索，若出現(xiàn)P：son implements Runnable語句，則說明線程是通過實現(xiàn)Runnable接口實現(xiàn)的；若出現(xiàn)P：son extends Thread語句，則說明線程是通過繼承Thread類實現(xiàn)的。其中P表示基本塊的編號(標記了線程類所在基本塊)，son表示線程類的名稱，在實際分析中會以具體的值出現(xiàn)。

下面給出線程的映射規(guī)則，如圖2所示。新建線程實例tr的線程類名稱為son，對應的基本塊編號為S。線程類定義了該類線程實例的行為模式。因語句tr.start()執(zhí)行后線程實例tr就會和father線程實例并發(fā)執(zhí)行，所以在動作start后添加同步動作son(son線程類的地址)，并將其作為同步并發(fā)的通道。father線程的實例將start語句所在基本塊的地址(用新名字p表示)通過son通道傳送過去。線程類son的實例通過son通道接收p并將其存儲到l中，兩個線程開始并發(fā)執(zhí)行。

這個過程，可以形式化地描述如下。

其中，子線程son的進程S可能會產(chǎn)生多個，因此使用了復制算子。按照擴展Pi演算的操作語義，father線程和son線程進行并發(fā)演算，在使用了COMM-L、CLOSE-L等規(guī)則之后，經(jīng)過(newthread，start，τ(son))一系列動作后，father線程和son線程開始并發(fā)執(zhí)行。經(jīng)過這樣的映射，形式化地表示了父子線程間的并發(fā)特征。

圖2 多線程的映射規(guī)則Fig.2 Mapping rules of multithread

3.3 并發(fā)特征分析

下面以AsyncTask為例進行并發(fā)特征分析。

AsyncTask是Android提供的一個輕量級的異步任務處理的工具類，其時序圖如圖3所示。在執(zhí)行后臺耗時操作之前，AsyncTask在主線程里執(zhí)行onPreExecute進行一些初始化操作，然后在后臺線程里執(zhí)行doInBackground方法處理那些耗時任務。一旦任務執(zhí)行完畢，主線程就會調(diào)用onPostExecute方法將結果返回到主線程并更新UI界面。其中publishProgress方法運行在后臺線程用于更新任務進度，更新完成后主線程會執(zhí)行onProgressUpdate方法展示任務進度。

圖3 AsyncTask的時序圖Fig.3 Sequence diagram for AsyncTask

圖3中的幾個方法都被重寫，因此需要根據(jù)擴展Pi演算語法對這些過程間調(diào)用方法進行映射。如對于onPreExeCute的映射結果如下所示。

從映射結果可知，主線程的進程表達式PUIthread在和后臺線程的進程表達式Pworkthread并發(fā)演算之前，需要先和onPreExecute方法的進程表達式PonPreExecute并發(fā)演算，即主線程在位置ps處調(diào)用onPreExecute方法并將ps發(fā)送給onPreExecute方法所在地址并存儲為pr，等到onPreExecute方法調(diào)用結束后再通過pr返回。

線程間的關系主要是交互關系和時序關系，可以在線程間構造一些交互通道，巧妙地描述出這些關系。如主線程執(zhí)行完onPreExecute方法之后，后臺線程才能夠執(zhí)行doInBackground方法。為了描述這種時序關系，構造一個通道t1，主線程在執(zhí)行完onPreExecute方法后，由通道t1向后臺線程發(fā)送一個空消息，后臺線程在doInBackground方法之前插入通道t1，保證只有在t1上接收一個消息后才能執(zhí)行doInBackground方法，這樣，就描述出了線程間的時序關系。對于交互關系，如publishProgress方法會把任務進度消息發(fā)送給onProgressUpdate方法，它們之間通信的通道在程序里沒有體現(xiàn)出來，因此，也為它們構造一個通道i1，通過該通道傳輸任務進度消息。于是可得到如下映射結果。

PAsyncTask=υt1t2i1i2(PUIthread‖Pworkthread)。

其中并沒有對后臺線程Pworkthread使用復制算子，因為異步任務的線程一般只能被執(zhí)行一次。由于用到了doInBackground方法中定義的publishProgress，所以給出了doInBackground的過程間調(diào)用的映射。但為了突出本文研究的問題，其他方法的過程間調(diào)用的映射被省略。

由擴展Pi演算的遷移規(guī)則可知，PAsyncTask經(jīng)過路徑(onPreExecute,τ(t1),τ(doInBackground), publishProgress,τ(i1), [onProgressUpdate, publishProgress],τ(i2),[ onProgressUpdate,τ(ds)],τ(t2),onPostExeCute/onCancelled)后成功終止。其中“[ ]”里的動作可能會以任意次序發(fā)生，如[onProgressUpdate, publishProgress]表示其路徑可能是(onProgressUpdate, publishProgress)或是(publishProgress, onProgressUpdate)?！?”表示兩個動作只能取其一，如onPostExeCute/ onCancelled表示要么onPostExeCute執(zhí)行，要么onCancelled執(zhí)行，但不會都執(zhí)行?？梢?，本映射方法準確地描述了AsyncTask的并發(fā)特征。

4 并發(fā)行為檢測

進程表達式描述了系統(tǒng)的行為模式，而系統(tǒng)需滿足的安全約束則可用演算規(guī)則和遷移規(guī)則來描述。安全約束是指保證提供某種安全保護所必須遵守的規(guī)則。如為了保證多線程模型的時序安全，doInBackground方法必須在onPostExecute方法之前執(zhí)行，該規(guī)則就是一條安全約束。

本文用包含進程表達式的IF-THEN規(guī)則表示演算規(guī)則和遷移規(guī)則，這意味著行為模式和行為所需滿足的安全約束之間可以演算和遷移，達到自動分析和檢測的目的。

4.1 規(guī)則構建

演算規(guī)則2(同步阻塞) IFa?A，x∈A，THENa.P‖x.Q=a.(P‖x.Q)。

其中0表示故障停機。規(guī)則1、2表明，同步動作必須與其補動作同步執(zhí)行而不能單獨執(zhí)行，且可以同步時必須優(yōu)先執(zhí)行同步動作。規(guī)則3表明，若一個系統(tǒng)中當前可執(zhí)行的動作皆為同步動作且不互補，則會導致故障停機，發(fā)生同步異常錯誤。

演算規(guī)則4(異步演算) IFa,b?A，THENa.P‖b.Q=a.(P‖b.Q)+b.(a.P‖Q)。

規(guī)則4表明，一般動作(不屬于同步集A中的動作)以不確定的方式異步執(zhí)行。這種不確定性導致異步演算中的并發(fā)進程最終能轉(zhuǎn)換為和進程。

以上4條規(guī)則可容易地利用進程等價(定義2)進行證明，不再贅述。根據(jù)擴展Pi演算的語法和語義，利用這些演算規(guī)則可得到如下安全約束。

由約束2可知，可以提取出各種時序關系并通過比對Android Apps的進程表達式的時序，檢測應用程序中存在的缺陷。還可以依據(jù)這些時序重寫進程表達式，并在運行時檢測應用程序中的API序列是否滿足這些時序關系，從而判定行為是否正常。

利用安全約束1和安全約束2，可將相關研究中的happens-before關系[13-18]形式化地構造成IF-THEN規(guī)則，這樣就可以復用這些成果，提高模型的精確性。

根據(jù)上面給出的演算規(guī)則，還可以推導出更多的演算規(guī)則。如由規(guī)則1和規(guī)則4可知，

由規(guī)則4可知，

IFa,b,c,d?A，

THEN (a.P+b.Q)‖(c.R+d.S)=a.(P‖(c.R+d.S))+b.(Q‖(c.R+d.S))+

c.((a.P+b.Q)‖R)+d.((a.P+b.Q)‖S)。

接下來，給出遷移規(guī)則。根據(jù)和進程的定義，容易得到其遷移規(guī)則。

由和進程的遷移規(guī)則可知，遷移動作必須是和進程中某項的前綴動作，否則將無法進行遷移而發(fā)生異常，表述如下。

由和進程的遷移規(guī)則和演算規(guī)則可以推導出其他的遷移規(guī)則。如由演算規(guī)則1和5可知，若存在x∈A，則有

結合演算規(guī)則1和安全約束1，可得同步遷移規(guī)則。

結合演算規(guī)則2、4和安全約束2，可得到異步遷移規(guī)則。

由同步遷移規(guī)則可知下面情況無法遷移，會發(fā)生異常。

構建了并發(fā)行為的運算規(guī)則后，就可以據(jù)此進行行為檢測，判定Android Apps中是否存在可能導致同步異常、遷移異常以及數(shù)據(jù)競爭等違反安全約束的行為。

行為檢測的大體思路是：依據(jù)演算規(guī)則和遷移規(guī)則，由輸入信息驅(qū)動進程表達式進行演算和遷移。本文模型將靜態(tài)檢測和動態(tài)檢測相結合，靜態(tài)檢測模塊將需要滿足的規(guī)則作為輸入，驅(qū)動模型執(zhí)行檢測；動態(tài)檢測模塊在目標App運行時，獲取其API調(diào)用和觸發(fā)事件(生命周期事件、UI事件)序列、Activity棧等信息作為輸入，驅(qū)動模型執(zhí)行檢測。動、靜態(tài)檢測的輸入雖然不同，但檢測算法和步驟是相同的。

4.2 行為檢測算法

為了在行為檢測過程中記錄進程表達式演算和遷移的狀態(tài)，為每個App維護一個行為狀態(tài)集asSet，由演算狀態(tài)集calcSet和遷移狀態(tài)集tranSet組成，即asSet::={calcSet,tranSet}。演算狀態(tài)集記錄當前演算前后的進程，即calcSet::={(oldprocess, newprocess)}。遷移狀態(tài)集記錄當前遷移到的進程和位置，即tranSet::={(process,{location})}，其中l(wèi)ocation可能有多個。

初始化演算狀態(tài)集calcSet的方法描述如下：

(ⅰ)初始化calcSet為空；

(ⅱ)將目標App的進程表達式app_proess作為一個演算前進程添加到calcSet，即calcSet={(app_proess,NULL)}。

初始化遷移狀態(tài)集tranSet的方法描述如下：

(ⅰ)初始化tranSet為空；

(ⅱ)使用GetFirstActions(app_proess)獲取目標App的進程表達式app_proess中所有可能的首個前綴動作，并將其添加到tranSet。若app_proess中所有可能的首個前綴動作為a、b和c，則tranSet= {(app_proess,{a,b,c}}。

檢測過程中，每次演算或遷移都更新一次asSet，更新算法如算法1所示。

算法1更新行為狀態(tài)集asSet。

Input: API調(diào)用和觸發(fā)事件序列、Activity棧等信息(動態(tài)檢測)；需滿足的規(guī)則，分為進程表達式和包含進程表達式的IF-THEN規(guī)則(靜態(tài)檢測)。

Output:行為狀態(tài)集asSet。

Procedure:

1: Pe Cp,Rp,P,Q

2:action[] actlist, act

3:algorithm *alg, *algo

4:int algotype //1為演算算法，2為遷移算法

5: while Input!=NULL do

6: actlist=GetAPIEventSequence (Input)

7: Cp=GetprocofActivity(GetActivity(Input))

8: Rp=GetprocofRule(Input)

9: alg=GetalgorithmofRule(Input)

10: algotype=GetalgotypeofRule(Input)

11: if algotype==1 then //演算

12: if alg!=NULL then

13: asSet.calculation(alg)

14: end

15: if Rp!=NULL then

16: asSet.InsertCalcSet(Rp)

17: end

18: while algo=canCalculus() do

19: asSet.calculation(algo)

20: end

21: if algotype==2 then //遷移

22: asSet.InserttranSet(Cp)

23: while actlist!=NULL do

24: act=actlist.GetAction()

25: asSet.transition(act)

26: end

27: end

28: Input.Next()

29: end

30: return asSet。

算法中，1～4行分別聲明了進程表達式、action數(shù)組、聲明演算或遷移算法的引用和算法類型。6～10行分別從輸入信息Input中獲取API調(diào)用和事件序列、取得當前棧頂Activity所對應的進程表達式、取得IF-THEN規(guī)則名(算法引用)、獲取算法類型(1為演算算法，2為遷移算法)。11～20行為演算操作，21～27行為遷移操作。其中calculation(calcRule)為進程演算算法，會依據(jù)指定的演算規(guī)則calcRule進行演算。transition(action)為進程遷移算法，由動作action驅(qū)動，依據(jù)遷移規(guī)則進行遷移，其遷移流程如圖4所示。

圖4 行為遷移流程Fig.4 Procedure of behavior transition

4.3 數(shù)據(jù)競爭檢測

數(shù)據(jù)競爭檢測的大體思路為：若操作共享數(shù)據(jù)的動作間包含了寫操作，則對這些動作進行檢測。動作間具有確定時序，則判定為正常；否則，判定為存在數(shù)據(jù)競爭問題。下面給出競爭關系集的數(shù)據(jù)結構。令raceRelationSet::={raceRelation}為競爭關系集，其中raceRelation為競爭關系，由競爭數(shù)據(jù)及其相關動作組成，即raceRelation::={racedata, {action}}。檢測步驟如下。

(A)初始化競爭關系集。將目標App中的組件對象(如Activity對象、Service對象等)設置為競爭數(shù)據(jù)，并將與之有關的回調(diào)事件、UI事件、生命周期事件作為相關動作，構造競爭關系。

(B)掃描目標App的數(shù)據(jù)流圖，利用文獻[23]的方法獲取共享數(shù)據(jù)和相關操作，加入raceRelationSet。

(C)在構造的raceRelationSet中，逐個檢測競爭數(shù)據(jù)的使用是否遵循了條件護衛(wèi)原則，若已遵循，則表明無數(shù)據(jù)競爭問題；若沒有遵循，則轉(zhuǎn)(D)。

(D)將與該共享數(shù)據(jù)相關的操作代入進程表達式，檢測其時序關系，若其具有確定時序，表明無數(shù)據(jù)競爭問題；若沒有，則表明存在數(shù)據(jù)競爭問題，生成檢測報告。

其中，第(A)步是為了得到App環(huán)境(Android平臺、UI操作等)中的數(shù)據(jù)競爭關系。下面以圖1為例，說明具體的檢測過程。

按照本文的建模方法，得到如下進程表達式。

PAsyncTask=υt1t2(PMainthread‖PBackgroundthread)

PAsyncApp=Paslifecycle‖PAsyncTask‖PonCreate。

PAsyncApp=Paslifecycle‖PAsyncTask‖PonCreate=

Paslifecycle‖υt1t2(PMainthread‖PBackgroundthread)‖PonCreate=

υt1t2(Paslifecycle‖PMainthread‖PBackgroundthread)‖PonCreate(SC-RES-COMP)=

從演算結果可以看出，onPostExecute和onDestroy之間沒有交互通道，由安全約束2知，兩者不存在時序約束，即其時序不確定，所以檢測出數(shù)據(jù)競爭問題。

5 實驗論證分析

5.1 實驗環(huán)境

為了便于對比分析，采用文獻[17]中提到的開源Apps驗證本文方法的有效性，從精確性和效率兩個方面進行評估，并與相關研究DroidRacer[17]、nAdroid[15]和Sard[16]進行對比。

建模過程需要使用Soot工具[24]進行控制流和數(shù)據(jù)流分析，資源消耗較高。因此，將建模與分析程序運行在Intel 3.20 GHz雙核CPU，8 GiB內(nèi)存的臺式機上。操作系統(tǒng)為Linux (rhel-server-5.4)，使用eclipse-kepler-SR2進行編譯和調(diào)試，Android的開發(fā)版本Android 6.0(API level 23)。測試用的開源Apps和運行時行為檢測程序都運行在8 GiB RAM、128 GiB ROM的Honor V20，其處理器為Kirin 980。

運行時行為檢測程序由API調(diào)用監(jiān)測模塊和檢測模塊組成。API調(diào)用監(jiān)測模塊采用API鉤子(API hook)技術，得到運行中的Apps的API的觸發(fā)時間、參數(shù)和返回值等信息。檢測模塊維護一個行為規(guī)則庫，其中存儲了IF-THEN格式的演算規(guī)則和遷移規(guī)則。依據(jù)行為規(guī)則，檢測模塊將API調(diào)用序列作為輸入，驅(qū)動進程表達式進行演算和遷移，給出檢測結果。

5.2 時空效率分析

a.c.τ(t).(b.0‖d.0)+c.a.τ(t).(b.0‖d.0)=

a.c.τ(t).b.d.0+a.c.τ(t).d.b.0+c.a.τ(t).b.d.0 +c.a.τ(t).d.b.0。

隨著進程中有更多的動作數(shù)以及App中有更多的并發(fā)進程，行為跡的數(shù)目將呈指數(shù)級增長，求解或遍歷程序的所有路徑將會引起狀態(tài)空間爆炸，導致極低的時空效率；不求解或遍歷程序的所有路徑，則會因檢測覆蓋面不全導致漏報問題。本文利用Pi演算的形式化和層次化特性，將各個子系統(tǒng)形式化為進程表達式，將子系統(tǒng)之間的時序、交互、同步和互斥等關系形式化為演算規(guī)則和遷移規(guī)則。依據(jù)這些規(guī)則，進程表達式通過并發(fā)演算可以還原出整個系統(tǒng)的結構信息。運行時行為檢測過程中，本文所提模型由捕獲的API驅(qū)動進行并發(fā)演算，這意味著，模型只會還原出程序該次運行所產(chǎn)生的路徑和相關結構信息。若程序的某次運行，其路徑上的API數(shù)為n，則模型的空間消耗為維護n個狀態(tài)列表的開銷，其規(guī)模與路徑上的API數(shù)n呈線性增長關系。

為了體現(xiàn)出擴展Pi演算層次化的特點，本文的建模方法將并發(fā)的行為抽象成進程表達式的并發(fā)集合及其上的演算，形成封閉的代數(shù)空間。由于沒有使用回溯算法，設進程表達式的長度為m，維護n個狀態(tài)列表的情況下，本文方法總的時間開銷為O(mn)，即運行時間是線性的，隨著m規(guī)模的增大并不會顯著地增加運行開銷。

5.3 檢測有效性分析

為了驗證本文所提出方法的有效性并與相關研究DroidRacer、nAdroid和Sard對比，使用10款開源的測試程序進行數(shù)據(jù)競爭檢測，結果如表1所示。其中檢測結果列、誤報數(shù)和漏報數(shù)列中由“/”分割的結果分別來自本文模型、DroidRacer、nAdroid和Sard。

從表1中可以看出，本文方法總計檢出數(shù)據(jù)競爭81處，實際數(shù)據(jù)競爭為69處，誤報15處，漏報3處。對比檢測結果、誤報數(shù)和漏報數(shù)可知，本文方法明顯優(yōu)于DroidRacer、nAdroid和Sard。這是因為本文方法通過將數(shù)據(jù)競爭的安全約束形式化地表示為包含進程表達式的IF-THEN規(guī)則，實現(xiàn)了行為模式和行為所需滿足的安全策略之間的并發(fā)演算，這種機制可以非常容易地將現(xiàn)有的安全約束應用在該模型中。并且，本文采用的是動靜態(tài)結合進行檢測。本文將DroidRacer檢測用戶代碼的讀寫競爭規(guī)則，nAdroid檢測Android Apps中時序規(guī)則和Sard中對線程內(nèi)和線程間并發(fā)錯誤的檢測規(guī)則都以IF-THEN規(guī)則的形式納入到本文模型中，因此有較高的精確性，且在提高檢測精確性的同時并沒有犧牲檢測的效率。

表1 數(shù)據(jù)競爭檢測結果

5.4 檢測性能分析

選取表1中的Android Apps作為目標程序進行時空負載的測試并與DroidRacer、nAdroid和Sard進行對比分析，其時間負載和空間負載分別如圖5、6所示。

由時間負載的測試結果可知，檢測過程中，本文方法運行引起的正常CPU時間在5倍以下，其時間負載表現(xiàn)良好。DroidRacer和Sard引起的正常CPU時間在7倍以下，差強人意。nAdroid引起的正常CPU時間最高達到了9.5倍，明顯高于其他方法，其檢測精確性提高的同時檢測效率卻大大降低，這直接影響了其實用性。

從空間負載的測試結果來看，本文方法的內(nèi)存空間增長率為3%～6%，非常穩(wěn)定，空間負載表現(xiàn)出色。這是因為本文方法檢測時并不需要將整個模型演算出來，而只需演算出待檢測的部分進行狀態(tài)遷移匹配，這有效地保障了模型的效率和實用性，測試結果也驗證了這一點。其他3種方法受應用程序規(guī)模的影響較大，其中nAdroid的內(nèi)存空間增長率為5%～12%，具有較高的空間負載。

圖5 時間負載測試結果Fig.5 Result of time overhead

圖6 空間負載測試結果Fig.6 Result of space overhead

6 結束語

本文針對事件驅(qū)動機制下的Android多線程程序的數(shù)據(jù)競爭問題，提出了一種形式化的行為檢測模型。利用擴展后的Pi演算對Android生命周期和多線程框架進行建模，探討了并發(fā)行為映射問題，并構建了并發(fā)行為的演算規(guī)則和遷移規(guī)則。擴展后的Pi演算的層次化特性適合于對Android Apps中組件化和基于通信的行為模式進行描述和檢測。進程演算等形式化特性有助于實現(xiàn)行為建模和檢測的自動化。通過將數(shù)據(jù)競爭的安全約束形式化地表示為包含進程表達式的IF-THEN規(guī)則，實現(xiàn)了行為模式和行為所需滿足的安全策略之間的并發(fā)演算，構建了檢測模型。將動態(tài)檢測與靜態(tài)檢測以相同的處理方式結合在檢測模型中，并給出了并發(fā)行為檢測算法和數(shù)據(jù)競爭檢測的方法。通過理論分析和實驗驗證，論證了該方法的檢測有效性和檢測性能。

本文模型特別適合對應用程序并發(fā)執(zhí)行導致的數(shù)據(jù)競爭進行檢測。演算規(guī)則越完備，模型越精確。但隨著演算規(guī)則的規(guī)模越來越大，如何驗證這些規(guī)則之間的一致性以規(guī)避規(guī)則的內(nèi)在沖突，如何將相關的規(guī)則約簡歸并以進一步提高檢測的效率是下一步亟需解決的問題。