基本信息
- 項目名稱:
- 基于程序安全行為模型的3G手機安全軟件
- 小類:
- 信息技術(shù)
- 大類:
- 科技發(fā)明制作B類
- 簡介:
- 在3G時代,手機功能日益豐富,用戶可以通過手機上網(wǎng)沖浪、玩在線游戲、下載程序等。然而,手機的信息安全隱患卻日益突出,比如: ● 私自發(fā)送短信; ● 竊取手機中的私人和商務(wù)信息; ● 刪除或破壞用戶數(shù)據(jù)(如手機拍攝的照片)。 傳統(tǒng)的防病毒軟件對已知病毒查殺頗為有效,但卻不能完全識別這些隱藏在“正常程序”中的千變?nèi)f化的惡意行為;防火墻死板地束縛了程序功能。為此,我們在理論創(chuàng)新的基礎(chǔ)上,提出了基于程序安全行為模型的改進的安全模型,研發(fā)了這套手機安全軟件。
- 詳細(xì)介紹:
- CoS手機安全軟件采用攜帶模型代碼(model-carrying code, MCC)方法的基本安全框架并進行改進: 1.在代碼生產(chǎn)方,通過自動靜態(tài)分析源代碼,生成基于擴展的下推自動機(extended pushdown automaton, EPDA)的程序安全行為模型,該模型描述代碼中所有安全敏感的方法調(diào)用,以及反映程序結(jié)構(gòu)的用戶自定義方法調(diào)用,并輔以數(shù)據(jù)流分析,描述方法參數(shù)的限定; 2.在代碼使用方,安全策略表達為擴展的有限自動機(extended finite state automaton, EFSA),可與程序安全行為模型自動機匹配,形式化驗證是否存在模型安全行為與安全策略的沖突; 3.代碼使用方運行程序時,對程序?qū)嶋H行為進行模型強制實施,截獲安全敏感方法調(diào)用后驗證是否與安全行為模型相符合,如果出現(xiàn)不一致可中止該進程。 理論創(chuàng)新主要包括: ● 采用擴展的下推自動機(EPDA)作為描述程序安全行為的模型:比以往采用的EFSA等模型更加精確,可有效處理模仿攻擊(mimicry),涵蓋更大范圍和絕大多數(shù)的惡意行為;同時保證運行時效率,模型描述能力大幅提高的同時沒有帶來顯著的額外開銷; ● 通過描述程序安全行為的EPDA和描述安全策略的EFSA相乘獲取程序行為和安全策略的沖突; ● 從以往針對過程式語言提升到針對工程化的面向?qū)ο笳Z言Java,具有更大的實用性和現(xiàn)實意義。 技術(shù)創(chuàng)新主要包括: ■ 實現(xiàn)了基于Eclipse Java開發(fā)工具接口、采用訪問者模式遍歷抽象語法樹進行數(shù)據(jù)流分析并獲得EPDA的方法技術(shù),該源代碼靜態(tài)分析技術(shù)比動態(tài)檢測技術(shù)更加方便用戶使用; ■ 實現(xiàn)了基于JVMDI的模型強制實施,采用通用軟件接口擴展Java虛擬機,突破修改Java字節(jié)碼和修改Java虛擬機的局限性,通用性和移植性更好。 實用創(chuàng)新性主要體現(xiàn)在: ◆ 解決了新問題 ○ 針對3G時代手機信息安全所面臨的前所未有的新威脅; ○ 填補了正常程序和病毒之間的“灰色地帶”,即針對包含惡意行為卻不足以被防病毒軟件識別為病毒的程序有效攔截; ◆ 采用了新方法 ○ 不依賴病毒庫,擺脫病毒與防毒軟件“道高一尺、魔高一丈”的循環(huán);通過程序安全行為模型的自動獲取及驗證,準(zhǔn)確識別千變?nèi)f化的未知惡意行為,有效處理移動代碼在移動過程中遭到篡改的情況; ○ 用戶在運行程序前即可通過模型概覽安全行為,避免用戶中止程序的負(fù)面作用,為用戶節(jié)省寶貴的手機運行時間(手機電池有限); ○ 面向特定程序自助配置安全策略,既不像代碼簽名機制對程序行為不加限制,也不像“沙盒”禁止一切本地資源訪問而喪失功能性,從而取得安全性和可用性的平衡,優(yōu)于現(xiàn)有軟件平臺的安全機制。
作品專業(yè)信息
設(shè)計、發(fā)明的目的和基本思路、創(chuàng)新點、技術(shù)關(guān)鍵和主要技術(shù)指標(biāo)
- 3G時代手機功能日益豐富,用戶越來越多地下載運行手機程序。然而手機信息安全隱患日益突出,如私自發(fā)送短信、竊取私人信息、刪除用戶數(shù)據(jù)等。防病毒軟件對已知病毒查殺頗為有效,但不能完全識別程序中千變?nèi)f化的惡意行為;防火墻死板地束縛了程序功能。我們的作品正是針對這些問題,為手機安全執(zhí)行非信任代碼設(shè)計的。 我們作品包括PC端和手機端:(1)PC端供Java程序員使用,是開發(fā)環(huán)境Eclipse的插件,可自動獲得安全行為模型,并與程序一同發(fā)布;(2)手機用戶下載程序和模型,首先驗證模型是否與手機安全策略相符;如有沖突表明存在安全風(fēng)險,用戶可不執(zhí)行程序,也可調(diào)整安全策略。程序執(zhí)行時,我們的擴展Java虛擬機監(jiān)控程序行為是否與模型相符,防止有篡改。 創(chuàng)新點: 一、解決了新問題:(1)針對3G手機信息安全面臨的新威脅;(2)填補了正常程序和病毒之間的“灰色地帶”,即包含惡意行為卻不足以被識別為病毒的程序。 二、采用了新方法:(1)避免依賴病毒庫的缺陷,通過程序安全行為模型準(zhǔn)確識別未知惡意行為和遭到的篡改;(2)用戶在運行程序前即可通過模型概覽安全行為,避免運行時中止,為用戶節(jié)省有限的電池;(3)面向特定程序自主配置安全策略,從而取得安全性和功能性的平衡。 技術(shù)關(guān)鍵和指標(biāo):(1)程序安全行為模型的自動生成,響應(yīng)時間≤10S;(2)模型安全性形式驗證器,能夠根據(jù)手機安全策略驗證模型的安全性,響應(yīng)時間≤15S;(3)運行時模型強制實施,增加耗時≤20%。
科學(xué)性、先進性
- 作品有著堅實的理論基礎(chǔ)。移動代碼安全領(lǐng)域已有諸多框架;入侵檢測領(lǐng)域發(fā)展了使用自動機建模的方法;面向?qū)ο笳Z言的靜態(tài)分析已較成熟。我們的作品以攜帶模型代碼(MCC)方法為依托,融合了入侵檢測和程序分析領(lǐng)域的研究成果,創(chuàng)新性地提出了基于擴展的下推自動機(EPDA)模型和面向?qū)ο笳Z言靜態(tài)分析技術(shù)的改進MCC方法。較以往安全機制有較大優(yōu)越性: 1) 代碼簽名僅能證明代碼來源可信; 2) 沙盒方法過分限制了代碼功能; 3) 攜帶證明代碼方法不切實際假定生產(chǎn)方知道使用方安全策略; 4) 協(xié)議安全為代碼生產(chǎn)方帶來了額外負(fù)擔(dān); 5) MCC方法既保證安全性又提供靈活性,同時基于自動化方法,方便使用,但模型描述能力不足、建模操作不便。 我們作品汲取了MCC方法的優(yōu)勢,并進行了改進: ● 采用EPDA作為描述程序安全行為的模型,更加精確,涵蓋大多數(shù)惡意行為; ● 從以往針對過程式語言提升到針對工程化面向?qū)ο笳Z言Java,具有更大的實用性和現(xiàn)實意義。
獲獎情況及鑒定結(jié)果
- 2008年被教育部評定為“國家大學(xué)生創(chuàng)新性實驗計劃”資助項目; 2009年獲本校“家曦杯”大學(xué)生課外學(xué)術(shù)科技作品競賽科技發(fā)明制作類一等獎; 2009年獲吉林省“挑戰(zhàn)杯”大學(xué)生課外學(xué)術(shù)科技作品競賽科技發(fā)明制作類一等獎。
作品所處階段
- 實用原型系統(tǒng)
技術(shù)轉(zhuǎn)讓方式
- 申請及轉(zhuǎn)讓專利,公司產(chǎn)品化 吉林融信電子科技有限公司已意愿協(xié)作
作品可展示的形式
- 實物、產(chǎn)品,現(xiàn)場演示,圖片,錄像 需220V電源、展桌、有線網(wǎng)接入、3G網(wǎng)絡(luò)覆蓋
使用說明,技術(shù)特點和優(yōu)勢,適應(yīng)范圍,推廣前景的技術(shù)性說明,市場分析,經(jīng)濟效益預(yù)測
- PC端供Java程序員使用。打開裝有CoS插件的Eclipse,只需單擊“產(chǎn)生模型”按鈕即可獲得模型文件。手機端供手機用戶使用:模型驗證器判定模型是否與本機安全策略沖突,用戶可自主配置策略;擴展的Java虛擬機CoS-PhoneME部署和使用與原虛擬機相同。 本作品適用于手機程序開發(fā)人員和手機用戶使用,特別是3G手機,可獲得現(xiàn)有機制無法提供的安全保障??赏茝V到各大手機廠商的Java平臺,用戶可安全盡享下載程序的豐富功能,將為廠商贏得更大市場。 中金公司預(yù)計,09年我國3G投資將達兩千億元。另據(jù)諾基亞調(diào)查顯示,55%的手機用戶使用了第三方程序??梢?,本作品為3G手機提供安全保障,具有巨大的市場需求,將會產(chǎn)生巨大的經(jīng)濟效益和社會效益。吉林融信電子科技有限公司已意愿協(xié)作本項目產(chǎn)品化及市場推廣。 本作品亦有顯著的理論意義??梢詳U展到入侵檢測、木馬病毒防護等領(lǐng)域。而且其中對程序行為模型的提取和驗證方法,也可應(yīng)用于程序行為建模、代碼錯誤檢查等更廣闊的范圍。
同類課題研究水平概述
- 早期Java語言的安全機制采用沙盒技術(shù),將程序分為兩類,一類不可以訪問任何本地資源,另外一類可以訪問任何資源,這種死板的模式極大限制了程序的功能。為了解決以上缺陷,人們采用病毒掃描、完整性檢測、行為檢測等主動偵測技術(shù)。病毒掃描技術(shù)是目前使用最廣泛的檢測技術(shù),但是每天都有成千上萬條病毒問世,維持特征碼數(shù)據(jù)庫的快速更新仍對新病毒無能為力;另外,由于網(wǎng)絡(luò)環(huán)境復(fù)雜化,人們對程序安全的粒度要求卻在提高,導(dǎo)致了越來越復(fù)雜的安全軟件配置。作為完整性檢測中的一種,代碼簽名技術(shù)被現(xiàn)代Java安全框架所采用,但是代碼簽名技術(shù)對第三方攻擊無能為力。 于是,更多的研究者將目光轉(zhuǎn)向了基于程序行為的檢測方法學(xué)。通過對程序行為建立模型來判定程序行為的安全性最早的工作可以追述到入侵檢測領(lǐng)域。手段主要可以分為兩類:誤用檢測和異常檢測。其中最著名的是攜帶證明代碼(Proof-Carrying Code)方法,要求代碼生產(chǎn)方提供移動代碼的安全性證明,代碼使用方檢查這個證明以確定是否執(zhí)行。PCC方法假定了代碼的生產(chǎn)方知道使用方的安全策略,顯然假設(shè)不現(xiàn)實,因為不同使用方的安全策略可以不同。 近年,由R. Saker提出的Model-Carrying Code(MCC)方法日益得到重視。該方法有機地組合了以上靜態(tài)驗證和動態(tài)監(jiān)測技術(shù)。驗證階段,程序行為模型與策略進行比較,這是一種誤用檢測的手段;程序運行時由運行監(jiān)控器保證程序的實際行為不超出模型描述,這是一種異常行為檢測手段。但MCC方法原有模型描述能力有限,無法處理模仿攻擊;基于動態(tài)檢測技術(shù)建模,給使用者帶來極大不便;且只能處理過程式語言,實用性不強。 最新提出的攜帶協(xié)議安全(Security by Contract)一定程度上解決了PCC的問題,移動代碼生產(chǎn)方可獲知手機公司的策略模板,并據(jù)此設(shè)定協(xié)議。但這一方法為移動代碼生產(chǎn)方帶來了額外負(fù)擔(dān),需要開發(fā)人員手工設(shè)定協(xié)議,尚無自動化機制。 運行時強制實施一般采用兩種方法,一種是通過修改Java字節(jié)碼,另外一種是通過修改Java虛擬機。前者的主要思想是插入一些監(jiān)控代碼,但由于Java類文件一般通過了加密,操作消耗時間較多。后者修改開源Java虛擬機,添加監(jiān)控操作,但修改后的虛擬機不在Java虛擬機規(guī)范的范圍內(nèi),因此這種方法的實用性比較低。