董 航,劉 洋,李承澤,付 戈,張 淼,楊義先
?
基于語義的Android敏感行為靜態(tài)分析方法
董 航1,劉 洋2,李承澤1,付 戈2,張 淼1,楊義先1
(1. 北京郵電大學(xué)信息安全中心 北京海淀區(qū) 100876;2. 國家計算機(jī)網(wǎng)絡(luò)應(yīng)急技術(shù)處理協(xié)調(diào)中心 北京朝陽區(qū) 100029)
提出一種基于語義的Android敏感行為靜態(tài)分析方法。該方法首先基于樣本統(tǒng)計結(jié)果,利用精簡Dalvik指令集作為本文分析的中間語言,實現(xiàn)對指令層的形式化語義描述;之后,基于中間語言發(fā)現(xiàn)檢測樣本中的敏感調(diào)用,并通過控制依賴關(guān)系追溯調(diào)用路徑;最后,在控制流分析基礎(chǔ)上, 對存在敏感調(diào)用的路徑約束求解路徑條件。最終求解出具體后臺行為及觸發(fā)條件,揭示出樣本后臺行為的執(zhí)行全過程。該方法緩解了符號執(zhí)行中的路徑爆炸問題,實驗驗證了該方法可以有效地對移動應(yīng)用后臺行為進(jìn)行分析,并及時獲取特征檢測無法發(fā)現(xiàn)的未知移動惡意應(yīng)用程序。
Android; 行為分析; 約束求解; 形式化描述
近年來,在諸多移動平臺中,針對Android平臺的惡意程序比例迅速攀升,數(shù)量呈爆發(fā)式增長[1]。新增的移動惡意程序中,Android平臺占據(jù)了絕大多數(shù),增長率超過了33%,遠(yuǎn)遠(yuǎn)大于傳統(tǒng)的桌面平臺,從而導(dǎo)致移動應(yīng)用安全形勢異常嚴(yán)峻。
基于終端的惡意程序的發(fā)展過程有著清晰的脈絡(luò)。在Symbian系統(tǒng)上,文獻(xiàn)[2]在2004年最早揭示了手機(jī)病毒,引起了人們對移動平臺軟件安全分析的逐步重視。2007~2009年間,文獻(xiàn)[3-4]相繼研究了智能手機(jī)的病毒特征,對智能手機(jī)系統(tǒng)結(jié)構(gòu)和安全機(jī)制進(jìn)行了分析,并提出了一種病毒檢測及預(yù)警系統(tǒng)。隨后文獻(xiàn)[5]在Android應(yīng)用分析中引入了自組織網(wǎng)絡(luò)中的分布式計算機(jī)制,提高了分析效率。與此同時,Android平臺著名應(yīng)用分析工具Androguard利用歸一化壓縮距離(normalized compression distance, NCD)進(jìn)行Android的應(yīng)用程序相似性分析[6],以壓縮特征判斷惡意軟件。進(jìn)一步,文獻(xiàn)[7]以此為基礎(chǔ),從Davlik指令層面提取惡意軟件特征。但這些方法大部分都是針對應(yīng)用自身特征,難以識別含有未知特征的樣本,從而引起漏報。
基于語義的檢測方法的提出為更好地檢測未知惡意軟件提供了支撐,桌面平臺下已有部分研究人員開展了相關(guān)研究,并取得了較好的效果[7],但是移動平臺下的研究才剛剛開始。在與移動平臺語義檢測相關(guān)的工作中,文獻(xiàn)[8]最早通過對指令和成員的符號描述,將符號計算應(yīng)用于Java card虛擬機(jī)中;文獻(xiàn)[9]借助于Java分析工具Java pathfinder,將符號執(zhí)行機(jī)制引入Android源代碼分析中,自動化地分析Android源碼中的缺陷,但是,其分析目標(biāo)是程序源碼,并不能對Android應(yīng)用程序中Dalvik字節(jié)碼進(jìn)行檢測。文獻(xiàn)[10]在分析應(yīng)用程序缺陷時對Android Dalvik指令進(jìn)行了符號描述,但該分析方法主要面向缺陷分析,在分析應(yīng)用的惡意行為時效率不高。
為了解決Android平臺惡意代碼分析問題,識別應(yīng)用程序敏感行為,發(fā)現(xiàn)未知的惡意應(yīng)用,本文在總結(jié)幾種現(xiàn)有的智能終端應(yīng)用程序分析方法和工具的基礎(chǔ)上,提出了一種基于語義的Android應(yīng)用行為檢測方法,通過分析測試樣本中的后臺行為及其觸發(fā)條件,從而更準(zhǔn)確地識別未知的惡意程序。
本文將移動應(yīng)用程序的敏感和惡意行為看作一系列操作序列,這些序列最終均會觸發(fā)關(guān)鍵的系統(tǒng)調(diào)用。本文提出的方法中,需要將重要系統(tǒng)調(diào)用做“敏感”標(biāo)記,并以此建立規(guī)則模版。在規(guī)則模板中,認(rèn)為正常行為與敏感行為的區(qū)別在于觸發(fā)這些操作的源頭:若一條包含敏感調(diào)用的操作序列的源來自于用戶交互,則認(rèn)為此行為源自用戶操作,在完成此敏感操作時用戶是知情的;反之,則認(rèn)為此序列為應(yīng)用后臺發(fā)起的敏感調(diào)用。
同時,為了計算和驗證這些存在敏感調(diào)用的路徑條件,本文在流追蹤的基礎(chǔ)上借鑒符號執(zhí)行的思想,約束求解路徑條件,優(yōu)化分析路徑,最終提出了基于語義的代碼行為檢測模型,用于解出樣本的具體后臺行為和觸發(fā)條件。
本文提出的檢測模型如圖1所示,核心思想是通過函數(shù)調(diào)用關(guān)系圖G=(,)提出包含敏感調(diào)用的函數(shù)節(jié)點(diǎn)N,之后以N為結(jié)束符號遍歷G,獲取G中包含N的所有可能路徑,并判斷這些路徑的源函數(shù)節(jié)點(diǎn)是否包含用戶交互行為;之后,使用數(shù)據(jù)流分析方法分析包含用戶行為的敏感路徑P的每個方法,去除無關(guān)節(jié)點(diǎn),進(jìn)一步優(yōu)化分析路徑;最后,對路徑求解約束,由N中敏感調(diào)用的具體參數(shù)計算得出敏感路徑P的觸發(fā)條件。
如圖1所示,分析引擎通過分析由抽象語法樹提取的控制流、數(shù)據(jù)流,定位敏感行為發(fā)生的關(guān)鍵位置,結(jié)合通過對控制依賴關(guān)系的分析,去掉不必要的分支,優(yōu)化分析對象,緩解路徑爆炸問題并節(jié)省約束求解時間;接下來,根據(jù)到達(dá)定值定理先完成對規(guī)則指定的關(guān)鍵變量的分析,精簡出必要的路徑供符號計算模塊進(jìn)行進(jìn)一步分析。符號計算模塊通過語義表達(dá)式對由simple-dalvik intermediate language(SDIL)中間語言描述的程序行為抽象進(jìn)行約束求解,去掉冗余路徑,提升分析效率,最終計算出敏感行為的觸發(fā)條件及其可達(dá)性。
圖1 檢測模型
為了減輕符號計算中語義描述的工作量,提高分析效率,本文對3000個Android樣本中的所有指令分布情況進(jìn)行統(tǒng)計分析,結(jié)合指令的實際執(zhí)行結(jié)果,在保留Dalvik指令集的基礎(chǔ)上,總結(jié)出一個以Dalvik指令為基礎(chǔ),包含了13條指令的精簡指令集作為本文分析的中間語言,稱此指令集為SDIL,具體語法如下:
SDIL的語法中,用于表示應(yīng)用程序中的目標(biāo)文件,由類(cls)、域(fld)、方法(mtd)和字符串(str)組成。在原Dalvik指令集中,str是以id為索引的資源映射,其中包括方法名、類名等信息,而在SDIL中,為了分析的方便,將映射全部展開,在之后的符號計算中不需要尋找映射,而可以直接使用str。
應(yīng)用程序的其他組成部分cls、fld與mtd均有各自的展開式,如cls由名稱、父類、接口與主體組成,主體又是由fld與mtd組成,mtd由方法名及方法主體mbody構(gòu)成。
語句stmt存在于方法的主體mbody中,包括了多種表達(dá)式,如指令move reg reg,表明當(dāng)前SDIL指令為move,后面操作數(shù)限定為兩個寄存器。這些指令的具體語義將在后文詳細(xì)表述。
SDIL的語義表達(dá)式由3種參數(shù)組成:pc表示當(dāng)前執(zhí)行指令,代表當(dāng)前分析的DEX文件,表示執(zhí)行當(dāng)前指令前的堆棧初始狀態(tài),。
語義表達(dá)式中的每一個狀態(tài)語句的計算都符合以下形式化表達(dá):
如SDIL中const指令的語義表達(dá)式為:
參考Dalvik指令官方文檔并結(jié)合實際分析,結(jié)果表明,在執(zhí)行指令const后,靜態(tài)堆和動態(tài)堆不變,而調(diào)用堆中計數(shù)器加一,操作數(shù)的值將被賦給目的寄存器。類似地,本文對所有SDIL指令都進(jìn)行了形式化的語義表達(dá)。
3.1 路徑提取
詞法和語法解析器可以對中間語言遍歷,生成對應(yīng)的抽象語法樹。通過遍歷抽象語法樹,可以很容易地獲取程序的控制依賴關(guān)系和生成控制流圖。
在獲取SDIL指令集的抽象語法樹之后,即可通過對其遍歷分析和提取函數(shù)調(diào)用關(guān)系圖,遍歷過程使用深度優(yōu)先算法,獲取函數(shù)調(diào)用關(guān)系圖G=(,)。函數(shù)調(diào)用關(guān)系圖G是一個有向有環(huán)圖,其邊的方向表明函數(shù)調(diào)用關(guān)系。
路徑提取的實質(zhì)是對包含了敏感調(diào)用的函數(shù)節(jié)點(diǎn)V的函數(shù)調(diào)用關(guān)系圖G遍歷,本文采取的方法是對函數(shù)調(diào)用關(guān)系圖G逆向搜索??紤]到圖G是一個有向有環(huán)圖,在遍歷的過程中需要重點(diǎn)考慮環(huán)的處理,通過對節(jié)點(diǎn)是否會構(gòu)成環(huán)進(jìn)行判斷,實現(xiàn)有環(huán)圖的開環(huán)。
算法1說明了從遍歷函數(shù)調(diào)用關(guān)系圖G=(,)中尋找所有到節(jié)點(diǎn)V的可能路徑并開環(huán)的過程。
算法1:遍歷調(diào)用關(guān)系圖尋找敏感調(diào)用路徑
輸入:函數(shù)調(diào)用關(guān)系圖G=(),包含敏感調(diào)用的函數(shù)節(jié)點(diǎn)
輸出:包含敏感調(diào)用的函數(shù)調(diào)用路徑
new stack=null
push
findPath(,)
for each=prev &&→unmarked do
if.serch()!= null
mark circle
continue
else
push
findPath(,)
end if
end for
if !mark circle
save path
end if
pop
與通常意義上的靜態(tài)缺陷分析要求遍歷完整路徑的思想不同,本文所提方法主要針對惡意應(yīng)用中的特定行為分析,故可以通過去掉與敏感行為發(fā)生路徑無關(guān)的節(jié)點(diǎn),僅提取與分析目標(biāo)相關(guān)的函數(shù)調(diào)用路徑,在降低路徑爆炸風(fēng)險的同時,也為進(jìn)一步分析節(jié)省了大量的計算工作。
以圖2所示的函數(shù)調(diào)用關(guān)系圖為例,其中函數(shù)包含了敏感調(diào)用HttpClient.execute(),經(jīng)過算法1計算,可以提取出與敏感調(diào)用相關(guān)的路徑,如表1所示。
圖2 函數(shù)調(diào)用關(guān)系圖示例
表1 與敏感調(diào)用相關(guān)的調(diào)用路徑
通過路徑提取可以對包含敏感調(diào)用的路徑進(jìn)行簡單分析:若通過算法1提取出的路徑的開始節(jié)點(diǎn)僅為用戶交互函數(shù),或僅為非用戶交互函數(shù),則可以初步判斷路徑是否為后臺路徑,然而圖2的遍歷結(jié)果中既包括了與用戶交互相關(guān)的路徑,也包含了無用戶交互的路徑。在這種情況下,需要在此基礎(chǔ)上對路徑中的數(shù)據(jù)流與控制流進(jìn)行追蹤,通過SDIL語義描述,使用符號計算的思想,約束求解路徑條件。
3.2 路徑優(yōu)化
符號計算通常會占用大量的資源,然而本文引入符號計算的主要目的只是為了求解移動應(yīng)用中特定敏感行為的觸發(fā)條件,并不需要展開完整控制流。為了避免產(chǎn)生路徑爆炸等問題,在進(jìn)行符號計算之前,需要對函數(shù)內(nèi)部的控制流圖進(jìn)行預(yù)處理,通過對函數(shù)內(nèi)部細(xì)節(jié)的優(yōu)化,減少不必要的計算分支。數(shù)據(jù)流分析是本文處理和優(yōu)化函數(shù)內(nèi)控制流的主要思想,利用到達(dá)定制定理,計算并剔除與敏感數(shù)據(jù)無關(guān)的分支,從而達(dá)到減少計算量的目的。本方法所涉及的一些定義如下。
定義 對順序出現(xiàn)的兩條語句1與2,定義以下4種數(shù)據(jù)依賴關(guān)系:
1) 若1給某變量賦值,而2使用了此變量,則稱這兩條語句之間存在流依賴關(guān)系,記為;
2) 若2給某變量賦值,而1使用了此變量,則稱這兩條語句之間存在反依賴關(guān)系,記為;
3) 若1與2都給某個變量賦值,則稱這兩條語句之間存在輸出依賴關(guān)系,記為;
4) 若2是否會執(zhí)行取決于1,則稱這兩條語句之間存在控制依賴關(guān)系,記為。
該定義也可擴(kuò)展為控制流圖中的基本塊之間的關(guān)系。
本文分析的一段帶有敏感調(diào)用的SDIL代碼為:
BLOCK 1
new2<-ArrayList
1<-paramString
6<-′imei′,7<-3
2.@add(5<-@BasicNameValuePair(6,7))
6<-″pm″,7<-″1″
2.@add(5<-@BasicNameValuePair(6,7))
BLOCK 2
:gogo_1
5<-m6
if5==0 :cond_1
BLOCK 3
5<-@equal(5,6<-″″)
if5<=0 goto cond_1
BLOCK 4
6<-′ostype′,7<-6
2<-@add(5<-@BasicNameValuePair (6,7))
BLOCK 5
:cond_1
5<-@RU.U11.U5( )
6<-5
BLOCK 6
5<-″newhi″
5<-@endsWith(1,5)
if5!=0
BLOCK 7
6<-″php″
1.@append(6)
BLOCK 8
5<-1.length
6<-0x14
if5 >6 :cond 2
BLOCK 9
3<-@HttpPost(1)
6<-″UTF-8″
3.@setEntity(5<-@UrlEncodedForm Entity(2),6)
5<-5.@execute(3).@getSatusLine(). @getStatusCode()
if5 != 0xc8 gote :cond_3
BLOCK 10
6<-′pm′,7<-′1′
2.@add(5<-@BasicNameValue Pair(6,7))
BLOCK 11
:cond_3
6<-′pm′,7<-′-1′
2.@add(5<-@BasicNameValue Pair(6,7))
goto :goto_1
BLOCK 12
:cond2
3<-@RU.U11.U3()
本文所使用的流優(yōu)化算法的核心思想是在到達(dá)定值定理的基礎(chǔ)上,根據(jù)所需追蹤的數(shù)據(jù)條件約束,判斷控制流圖G=(,,start,end)中與無關(guān)的分支,從而達(dá)到優(yōu)化的目的,算法主要包括7個步驟:
1) 初始化到達(dá)定值分析中的in[B],out[B],gen[B]與kill[B]。其中對in[B]的初始化需要考慮函數(shù)兩種情況,即:
2) 迭代計算得到所有的基本塊的in[B]與out[B]。
7) 結(jié)束所有基本塊的搜索,將剩余的基本塊按照控制關(guān)系生成新的控制流圖,可達(dá)路徑保存至可達(dá)路徑隊列,以備符號計算。
圖3展示的是優(yōu)化前后的控制流圖對比,其中編號為9的基本塊中存在敏感API調(diào)用。
圖3 SDIL指令及對應(yīng)控制流圖
3.3 符號計算
通過路徑優(yōu)化可以極大地降低后續(xù)符號執(zhí)行過程中的計算量,在得到優(yōu)化后的控制流圖后,就可以對其進(jìn)行展開和符號計算。
符號計算中的約束來源于精簡指令集的語義規(guī)則。結(jié)果表明,當(dāng)路徑條件為時,關(guān)鍵參數(shù)3的值為HttpPost(1).@setEntity(@UrlEncoded FormEntity(2),UTF8')。從約束求解的結(jié)果可以看出,敏感調(diào)用的參數(shù)依賴于整個函數(shù)的入?yún)?,單對此函數(shù)的計算并不能完整分析出敏感調(diào)用的具體參數(shù)。在這種情況下,需要持續(xù)迭代,將函數(shù)及參數(shù)1做為主調(diào)函數(shù)中的敏感調(diào)用,基于前文算法逐個進(jìn)行優(yōu)化和符號計算,最終求解出完整的路徑條件與敏感參數(shù)表達(dá)式。
本文使用的計算方法為靜態(tài)計算,也會遇到一般符號執(zhí)行中所面臨的外部環(huán)境交互問題。本文采用的是對系統(tǒng)調(diào)用函數(shù)構(gòu)建環(huán)境建模庫的方法,緩解對外部調(diào)用的依賴。
本文主要從語義提取后路徑優(yōu)化效率及分析結(jié)果兩方面進(jìn)行評估。為了評估本文所提算法的優(yōu)化效率,從測試數(shù)據(jù)中隨機(jī)選取5個樣本,對其經(jīng)過優(yōu)化前后的指令條數(shù)進(jìn)行了統(tǒng)計,統(tǒng)計結(jié)果如表2所示。
表2 路徑優(yōu)化比例
從分析結(jié)果可以看出,本文所提路徑優(yōu)化算法可以極大地降低實際分析的工作量,基于敏感路徑分析的優(yōu)化算法一般情況下可以去掉80%~90%的無關(guān)指令;通過數(shù)據(jù)流優(yōu)化算法,可以在此基礎(chǔ)上進(jìn)一步優(yōu)化20%左右的無關(guān)路徑。最終輸入到符號計算中的僅為不到10%的指令,極大地提升了分析效率。
圖4 檢測工具所檢測的發(fā)送短信行為
基于前文的理論和算法,開發(fā)了一套用于分析手機(jī)惡意軟件后臺行為的分析工具,并用實際樣本進(jìn)行了測試,從測試的正常樣本中發(fā)現(xiàn)了一些具有后臺行為的應(yīng)用程序。這些應(yīng)用程序并未被殺毒軟件劃歸為惡意應(yīng)用范疇,但是其行為又可能對用戶產(chǎn)生影響。分析中發(fā)現(xiàn),很多軟件會在后臺將用戶相關(guān)數(shù)據(jù)通過網(wǎng)絡(luò)或短信發(fā)送,如圖4所示。這些信息若被不法分子利用,將會嚴(yán)重危害用戶的個人信息安全。
本文作者所在項目組已將通過本方法發(fā)現(xiàn)的10余類典型惡意樣本提交至國家互聯(lián)網(wǎng)應(yīng)急響應(yīng)中心處置。
本文的貢獻(xiàn)主要包括以下3個部分:
1) 提出了一套以Dalvik指令集為基礎(chǔ)的精簡指令集。指令集針對移動惡意代碼行為的特點(diǎn),將原指令集進(jìn)行語義歸納與優(yōu)化,同時仍保持源程序的語義與控制關(guān)系;
2) 在精簡指令集的基礎(chǔ)上,提出了基于語義的行為分析方法,方法通過精簡指令對樣本代碼進(jìn)行符號化抽象,跟蹤敏感調(diào)用追蹤相關(guān)數(shù)據(jù)流和控制流變化,解決了一般的分析方法無法有效追蹤移動應(yīng)用行為的問題;
3) 完成了原型系統(tǒng)開發(fā),實現(xiàn)了基于語義的移動惡意代碼行為提取和檢測等功能。測試結(jié)果表明,本文所提方法可以有效發(fā)現(xiàn)移動應(yīng)用的后臺行為,對未知惡意軟件具有較好的識別能力。
本文提出的方法將Android指令集精簡并提煉出了用于分析應(yīng)用行為的中間語言,可以高效地對應(yīng)用行為進(jìn)行形式化描述。通過對控制流、數(shù)據(jù)流和控制依賴關(guān)系的深度分析,在并在計算的過程中不斷優(yōu)化分析路徑,緩解了符號執(zhí)行中的路徑爆炸問題。最終通過路徑追溯,可以發(fā)現(xiàn)應(yīng)用在非用戶確認(rèn)的情況下執(zhí)行的后臺行為并計算其觸發(fā)條件,揭示出樣本后臺行為的執(zhí)行全過程。實驗表明本方法可以發(fā)現(xiàn)特征檢測無法發(fā)現(xiàn)的未知移動惡意應(yīng)用程序,在一定程度上彌補(bǔ)了現(xiàn)有特征分析不能有效發(fā)現(xiàn)未知應(yīng)用的問題。
[1] 工信部國家互聯(lián)網(wǎng)應(yīng)急中心. 2013年我國互聯(lián)網(wǎng)網(wǎng)絡(luò)安全態(tài)勢綜述[EB/OL]. [2014-03-20]. http://www.199it.com/ archives/206597.html.
CNCERT. Overview of 2013 China's Internet network security situation[EB/OL]. [2014-03-20]. http://www. 199it.com/archives/206597.html.
[2] DAGON D, MARTIN T, STARNER T. Mobile phones as computing devices: the viruses are coming![J]. Pervasive Computing, 2004, 3(4): 11-15.
[3] CHEUNG J, WONG S, YANG H, et al. Smartsiren: Virus detection and alert for smartphones[C]//Proc of the 5th Int Conf on Mobile Systems, Applications and Services. New York: ACM, 2007: 258-271.
[4] SHABTAI A, FLEDEL Y, KANONOV U, et al. Google Android: a state-of-the-art review of security mechanisms[EB/OL]. [2014-03-20]. http://www.docin. com/p-189587298.html.
[5] SCHMIDT A D, BYE R, SCHMIDT H G, et al. Static analysis of executables for collaborative malware detection on Android[C]//ICC'09 IEEE Int Conf on Communications. [S.l.]: IEEE, 2009: 1-5.
[6] DESNOS A. Android: Static analysis using similarity distance[C]//2012 45th Hawaii Int Conf on System Science (HICSS). Los Alamitos: IEEE Computer Society, 2012: 5394-5403.
[7] 李挺, 董航, 袁春陽, 等. 基于Dalvik指令的Android惡意代碼特征描述及驗證[J]. 計算機(jī)研究與發(fā)展, 2014, 51(7): 1458-1466.
LI Ting, DONG Hang, YUAN Chun-yang, et al. Description of android malware feature based on dalvik instructions[J]. Journal of Computer Research and Development, 2014, 51(7): 1458-1466.
[8] 王蕊, 馮登國, 楊軼, 等. 基于語義的惡意代碼行為特征提取及檢測方法[J]. 軟件學(xué)報, 2012(2): 378-393.
WANG Rui, FENG Deng-guo, YANG-Yi, et al. Semantics- based malware behavior signature extraction and detection method[J]. Journal of Software, 2012(2): 378-393.
[9] SIVERONI I A. Operational semantics of the java card virtual machine[J]. The Journal of Logic and Algebraic Programming, 2004, 58(1): 3-25.
[10] MIRZAEI N, MALEK S, PASAREANU C S, et al. Testing Android apps through symbolic execution[J]. Sigsoft Softw Eng Notes, 2012, 37(6): 1-5.
[11] KARLSEN HS, WOGENSEN ER, OLESEN MC, et al. Study, formalisation, and analysis of Dalvik bytecode[C]// Proc of the Seventh Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2012). Tallinn: ETAPS, 2012.
編 輯 葉 芳
Semantic-Based Sensitive Behavior Analysis Method for Android
DONG Hang1, LIU Yang2, LI Cheng-ze1, FU Ge2, ZHANG Miao1, and YANG Yi-xian1
(1. Information Security Center, Beijing University of Posts and Telecommunications Haidian Beijing 100876; 2. National Computer Network Emergency Response Technical Team/Coordination Center of China Chaoyang Beijing 100029)
This paper proposes a semantic-based sensitive behavior analysis method for Android. With sample statistics results, the method firstly adopts a simple-Dalvik intermediate language (SDIL) as the intermediate language for text analysis, thus giving a symbolic semantics description for instructions. Then the method uses SDIL to detect sensitive calls from the samples and traces the call paths according to the control dependence. Then based on control-flow analysis, the method adopts constraint solving to obtain path conditions. At last, the method finds the background behaviors with trigger conditions, thus the whole process of background behavior execution will be showed as well. This method can release the path explosion problem in the process of symbolic execution. With experiment under our platform, it proves that the method can analyze the background behaviors of mobile application efficiently, and find the unknown mobile malicious applications which can not be found by traditional feature detection methods in time.
Android; behavior analysis; constraint solve; formal description
TP309.5
A
10.3969/j.issn.1001-0548.2017.02.019
2014-05-16;
2016-07-06
國家自然科學(xué)基金(61302087);國家科技支撐計劃(2012BAH06B02);教育部博士點(diǎn)基金(20120005110017)
董航(1986-),男,博士,主要從事軟件安全和移動互聯(lián)網(wǎng)安全方面的研究.