李忠慧

摘要：該文把靜態(tài)分析技術(shù)與基于模型的演繹驗(yàn)證結(jié)合起來提供了一個(gè)框架，分析應(yīng)用源代碼，自動(dòng)生成一個(gè)分析器，它能夠推斷關(guān)于給定程序行為的邏輯約束方面的信息。該文引入了一階邏輯斷言來描述API調(diào)用語義。這些斷言構(gòu)成分析器使用的模型。通過實(shí)驗(yàn)，該方法可被用來識(shí)別Java程序中的關(guān)于安全的邏輯錯(cuò)誤。

關(guān)鍵詞： Android；軟件安全；靜態(tài)分析

中圖分類號：TP393 文獻(xiàn)標(biāo)識(shí)碼：A 文章編號：1009-3044（2015）20-0182-02

Research of Static Detection Method Based on Model

LI Zhong-hui

（College of Information Engineering in Yancheng Teachers University， Yancheng 224002，China）

Abstract： This paper introduces a framework， which combines the static analysis technology and the deductive verification based on model. It is used for analysis of application source code， automatically generating an analyzer， which can give the inferred information on the logic of a given constraints of program behavior. This paper introduces first-order logic assertions to describe semantics of the API calls. These assertions constitute the model used by the analyzer. Through the experiment， this method can be used to identify the logic errors about the security in Java program.

Key words： Android；software security； static analysis

1 引言

Android系統(tǒng)是主要用于移動(dòng)智能設(shè)備上的源代碼開放的操作系統(tǒng)。由于其開源性和高額市場占有率，Android系統(tǒng)成為攻擊者的主要攻擊對象。軟件可能包含惡意代碼或漏洞，攻擊者利用來泄露敏感數(shù)據(jù)，執(zhí)行惡意的操作，修改有價(jià)值信息。因此，軟件的正確性和可靠性至關(guān)重要。

緩沖區(qū)溢出、空引用都可能被惡意應(yīng)用程序用來創(chuàng)建安全漏洞，以此來泄露的機(jī)密數(shù)據(jù)。許多這類錯(cuò)誤很容易被忽視，直到很久以后引起災(zāi)難性的后果。系統(tǒng)的運(yùn)行時(shí)錯(cuò)誤處理機(jī)制很難確保系統(tǒng)復(fù)蘇。另外，一個(gè)更重要的問題是缺乏適當(dāng)?shù)墓ぞ咧С謾z測應(yīng)用程序中的應(yīng)用依賴的邏輯錯(cuò)誤。很多軟件故障事件是由軟件的應(yīng)用依賴的邏輯錯(cuò)誤導(dǎo)致的[1][2]。這類邏輯錯(cuò)誤是深層次的，單獨(dú)使用目前的測試技術(shù)是難以檢測。

本文將靜態(tài)分析技術(shù)和基于模型的演繹驗(yàn)證相結(jié)合，對應(yīng)用軟件的源代碼分析，自動(dòng)生成一個(gè)能夠推斷關(guān)于依賴邏輯信息的分析結(jié)果。由于很多時(shí)候，我們并不能得到應(yīng)用軟件的源代碼，轉(zhuǎn)而分析該軟件的模型，基于模型的方法是必需的。所以，本文采用的靜態(tài)分析和模型技術(shù)相結(jié)合的方法。

2 相關(guān)工作

軟件驗(yàn)證技術(shù)主要分為三大類[3]。第一類是非形式化，動(dòng)態(tài)方法，如軟件測試和監(jiān)控等。這些技術(shù)擴(kuò)展性好，是最常用的技術(shù)。軟件測試在軟件開發(fā)工作中占百分之四十到六十。然而，傳統(tǒng)的軟件測試方法不能保證系統(tǒng)需要滿足的高層邏輯屬性的形式化規(guī)范和驗(yàn)證。在安全關(guān)鍵的軟件領(lǐng)域，指數(shù)級爆炸處理是不可避免的，傳統(tǒng)的測試技術(shù)很難被用來處理這種狀況。第二類是形式化方法。模型檢測等傳統(tǒng)形式方法和定理證明通常太繁瑣，需要相當(dāng)大的手動(dòng)工作，因而在實(shí)踐中很少使用。模型檢測是一種自動(dòng)驗(yàn)證方法，主要在處理有限狀態(tài)系統(tǒng)。第三類是靜態(tài)分析技術(shù)[4]和抽象解釋[5]。靜態(tài)分析是指在編譯時(shí)自動(dòng)推斷一個(gè)程序的行為的技術(shù)。雖然靜態(tài)分析工具取得巨大的實(shí)際成功，經(jīng)常結(jié)合先進(jìn)的編譯器，這類工具缺乏演繹能力，只能檢測淺顯的簡單錯(cuò)誤。傳統(tǒng)的靜態(tài)分析工具無法檢測死鎖的存在或并發(fā)程序違反互斥。抽象解釋是收集、比較、結(jié)合程序的語義的技術(shù)。它已經(jīng)成功地用于推斷出程序的運(yùn)行時(shí)性能，可用于程序優(yōu)化。近年來，在軟件的靜態(tài)分析上，已經(jīng)完成了大量的工作。

Uno、Splint、Polyspace等靜態(tài)分析工具[6]執(zhí)行輕量級數(shù)據(jù)流分析。Astree是一個(gè)靜態(tài)程序分析器，旨在證明嵌入式程序沒有運(yùn)行時(shí)錯(cuò)誤。Astree只能處理一個(gè)C語言子集，而不是完整的C語言。同時(shí)，它只適用于特定的運(yùn)行時(shí)錯(cuò)誤，而不是程序的一般屬性。Halbwachs等人使用線性關(guān)系分析來發(fā)現(xiàn)程序的數(shù)值變量之間的不變的線性不等式。Alur等人使用謂詞抽象來分析混合動(dòng)力系統(tǒng)，創(chuàng)建有限狀態(tài)自動(dòng)機(jī)。

3 Android平臺(tái)簡介

Android系統(tǒng)是一個(gè)用于移動(dòng)設(shè)備的軟件堆棧，包括操作系統(tǒng)、中間件和關(guān)鍵應(yīng)用程序。Android允許應(yīng)用程序與系統(tǒng)中其它應(yīng)用程序共享數(shù)據(jù)和函數(shù)[7]。Android系統(tǒng)沒有一個(gè)單一的入口點(diǎn)（沒有main（）函數(shù)）。系統(tǒng)已有基本組件，可以根據(jù)需要進(jìn)行實(shí)例化和運(yùn)行。四大組件是：Activity、Service、Broadcast Receivers、Content Providers。Android使用Intent激活前3個(gè)組件。對于Activity和Service，Intent是。接收機(jī)需要采取預(yù)定義的動(dòng)作來處理數(shù)據(jù)。在我們的分析框架中，Intent是關(guān)鍵。我們使用Intent對象來執(zhí)行數(shù)據(jù)流分析和函數(shù)調(diào)用分析。

Android框架支持使用手機(jī)功能構(gòu)建應(yīng)用程序，通過使錯(cuò)誤和惡意軟件的后果的最小化來保護(hù)用戶。在Android中，應(yīng)用程序可以與其他應(yīng)用程序共享數(shù)據(jù)和功能。為了安全，這些訪問必須嚴(yán)格控制。Android權(quán)限允許應(yīng)用程序有權(quán)執(zhí)行功能，如拍照、使用GPS、或打電話。在應(yīng)用程序安裝時(shí)，他們有一個(gè)獨(dú)特的UID，每個(gè)應(yīng)用程序總是運(yùn)行在特定設(shè)備上的UID下。應(yīng)用程序的UID是用來保護(hù)其與其他應(yīng)用程序共享數(shù)據(jù)。

4 基于模型的靜態(tài)檢測方法

圖1是本文采用的基于模型的靜態(tài)分析方法的流程圖。應(yīng)用程序的抽象集語義用標(biāo)記約束表示。API庫的語義是未知的，標(biāo)記是一組應(yīng)用程序?qū)?yīng)的API組合。本文用一階邏輯斷言或約束來描述調(diào)用的API語義。這些斷言就構(gòu)成模型，根據(jù)約束描述，進(jìn)行檢測，求解得到最終推斷結(jié)果。

圖1 本文分析方法的流程圖

本文對應(yīng)用分析的算法的主要步驟如下：

1） 通過逆向工程手段，得到應(yīng)用程序的源碼、配置文件以及一些資源文件等。根據(jù)manifest.xml文件，驗(yàn)證在Java源代碼中調(diào)用的API的權(quán)限。權(quán)限驗(yàn)證的結(jié)果是用來修改和建立API模型。

2） 對Java源代碼分析生成抽象收集語義約束。

3） 導(dǎo)入無語義的方法和對象的模型為斷言，和已經(jīng)生成的約束。

4） 通過添加適當(dāng)?shù)姆治龇矫娴募s束生成一個(gè)分析器。

5） 通過求解約束分析，得到推斷結(jié)果。

4.1 權(quán)限驗(yàn)證

Android的權(quán)限可分為不同的保護(hù)級別。應(yīng)用程序在Mainifest.xml文件中申請所需權(quán)限。我們通過分析程序中調(diào)用的API，構(gòu)建所需的權(quán)限列表，將其和 從Mainifest.xml文件中檢索的權(quán)限信息進(jìn)行比較。如果每個(gè)API所需的權(quán)限都已提供，我們認(rèn)為應(yīng)用程序沒有違反權(quán)限。否則，任何沒有提供適當(dāng)?shù)臋?quán)限的API調(diào)用將在分析斷言中返回1。

4.2 程序語義的收集和推斷

為了分析Java程序的深入邏輯屬性，我們對其進(jìn)行過程內(nèi)和過程間分析。在過程內(nèi)分析中，從源代碼的數(shù)據(jù)流分析，構(gòu)建一個(gè)約束系統(tǒng)，來捕捉其收集語義。在過程間分析中，建立一個(gè)與不同的API調(diào)用相關(guān)的調(diào)用圖和定義一些外部規(guī)則，檢測分析代碼是否違反這些規(guī)則。

5 實(shí)驗(yàn)結(jié)果分析

我們分析了Android Bluetooth ChatServices應(yīng)用的源代碼。這個(gè)應(yīng)用程序構(gòu)建一個(gè)藍(lán)牙網(wǎng)絡(luò)平臺(tái)，它允許設(shè)備與其他藍(lán)牙設(shè)備交換數(shù)據(jù)。它有三個(gè)主要功能：發(fā)現(xiàn)藍(lán)牙設(shè)備、可連接設(shè)備、這些設(shè)備之間傳輸數(shù)據(jù)。應(yīng)用程序使用了如下的API調(diào)用：BluetoothAdapter.getDefaultAdapter（），BluetoothAdapter.getRemoteDevice（address），BluetoothSocket 和BluetoothChatService。對于這個(gè)應(yīng)用程序，我們只是考慮到應(yīng)用程序可以設(shè)置藍(lán)牙服務(wù)和可以連接到任何設(shè)備發(fā)現(xiàn)。所以我們設(shè)BluetoothChatService返回一個(gè)非null對象，在SMT規(guī)范中，我們對API函數(shù)值建模為（not ?1）。源代碼分析滿足規(guī)范。我們下載了幾個(gè)免費(fèi)的android應(yīng)用程序源代碼，運(yùn)行源代碼靜態(tài)分析工具。發(fā)現(xiàn)應(yīng)用程序SMSPopup含有命令注入錯(cuò)誤；命令聲明是一個(gè)數(shù)組，來自另一個(gè)函數(shù)，它可能提供一個(gè)錯(cuò)誤的語句，應(yīng)用openGPStracker擁有比它實(shí)際需要更多的權(quán)限，有硬編碼的密碼。

6 結(jié)論

Android應(yīng)用程序可以使用系統(tǒng)提供機(jī)制相互溝通，如文件、活動(dòng)、服務(wù)、BroadcastReceivers、contentprovider。我們的程序分析框架可以幫助開發(fā)人員靜態(tài)地檢測違反編程錯(cuò)誤和違反權(quán)限。開發(fā)人員需要了解哪些權(quán)限需要正確設(shè)置，需要一些邏輯和約束求解的背景知識(shí)。我們未來的工作重點(diǎn)是設(shè)計(jì)一個(gè)良好的用戶界面，來幫助用戶輕松設(shè)置約束，揭示程序中的邏輯錯(cuò)誤。

參考文獻(xiàn)：

[1] 方喆君，劉奇旭，張玉清.Android應(yīng)用軟件功能泄露漏洞挖掘工具的設(shè)計(jì)與實(shí)現(xiàn)[J].中國科學(xué)院大學(xué)學(xué)報(bào).2015，32（1）：127-135.

[2] 楊歡，張玉清，胡予濮，等.基于多類特征的Android應(yīng)用惡意行為檢測系統(tǒng)[J].計(jì)算機(jī)學(xué)報(bào).2014，37（1）：15-27.

[3] 陳楠，王震宇，竇增杰，等.可執(zhí)行可信軟件安全性分析技術(shù)研究[J].計(jì)算機(jī)工程與設(shè)計(jì)，2010，31（22）：4802-4805.

[4] 匡春光，陳華，張魯峰.針對Java程序的一種脆弱性靜態(tài)分析技術(shù)[J].計(jì)算機(jī)系統(tǒng)應(yīng)用，2008，5：89，94-96.

[5] 屈婉霞，李暾，郭陽，等.模型檢驗(yàn)中抽象技術(shù)研究綜述[J].計(jì)算機(jī)工程與應(yīng)用，2006，33：15-19.

[6] 王凱，孔祥營.軟件靜態(tài)分析工具評析[J].指揮控制與仿真，2011，33（2）：109-111，119.

[7] 張玉清，王凱，楊歡，等.Android安全綜述[J].計(jì)算機(jī)研究與發(fā)展.2014，51（7）：1385-1396.