任 璐，尹 青，常 瑞，蔣 航

數(shù)學工程與先進計算國家重點實驗室，鄭州 450001

ARM-Android平臺的訪問控制機制研究進展*

任 璐，尹 青，常 瑞+，蔣 航

數(shù)學工程與先進計算國家重點實驗室，鄭州 450001

Abstract:With the increasing dependence on mobile devices,the security of mobile platforms has aroused extensive attention.Android is a popular open source software stack for a wide range of embedded devices.As the core of system security,the access control mechanism of Android is always a hot spot.This paper focuses on access control mechanisms for the ARM-Android platform,including the hardware isolation,application sandbox and permissionbased protection methods.Several model enhancements in different system levels are analyzed according to the comparison of specific control strategies.Then the status of research on multi-level comprehensive access control schemes is summarized.Furthermore,combining ARM TrustZone isolation environment,this paper proposes an access control model and its key technology.Mechanism specifications are obtained through the system analysis,and the formal method is applied to model abstraction and demonstration.Based on the vulnerability analysis and formal modeling work,directions for the relevant research are discussed at last.

Key words:ARM-Android;access control;model enhancement

隨著人們對移動設(shè)備的依賴，移動設(shè)備的安全性問題日益凸顯。Android設(shè)備是應(yīng)用廣泛的開源性移動平臺，其訪問控制機制作為系統(tǒng)安全的核心，更是備受關(guān)注。針對ARM-Android系統(tǒng)的硬件隔離、系統(tǒng)沙箱和權(quán)限保護機制，根據(jù)具體策略進行分類對比，綜合分析了不同系統(tǒng)層次的模型改進方案，并總結(jié)了多層次綜合策略訪問控制的研究現(xiàn)狀。進一步結(jié)合ARM TrustZone隔離環(huán)境，提出了一種系統(tǒng)訪問控制的安全模型及關(guān)鍵實現(xiàn)技術(shù)，通過系統(tǒng)分析得到機制規(guī)范，并利用形式化方法進行了模型抽象和證明。最后根據(jù)安全機制的漏洞分析和形式化建模工作，梳理了相關(guān)研究方向。

ARM-Android；訪問控制；模型改進

1 引言

在自攜設(shè)備（bring your own device，BYOD）、工業(yè)4.0等新型應(yīng)用場景下，伴隨著Android系統(tǒng)的應(yīng)用急劇增長及迅速更新?lián)Q代，移動嵌入式設(shè)備的安全需求更加復(fù)雜，Android的安全研究也隨之發(fā)展，如系統(tǒng)安全分析與系統(tǒng)改進[1-4]、應(yīng)用分析與惡意檢測[5-7]等。

設(shè)備應(yīng)用環(huán)境的多樣化，對系統(tǒng)訪問控制也有了更高的要求。ARM-Android作為流行的移動平臺架構(gòu)，主要通過自主訪問控制進行系統(tǒng)保護，在訪問控制粒度和授權(quán)管理上仍暴露出許多安全漏洞，如CVE-2015-38581）http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2015-3858.、CVE-2016-08052）http://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2016-0805.漏洞等，因此訪問控制模型研究一直是工業(yè)和學術(shù)界研究的熱點。此外，當前的可信執(zhí)行技術(shù)也為系統(tǒng)安全提供了更強的硬件隔離環(huán)境，利于實現(xiàn)更底層的訪問控制。然而由于嵌入式設(shè)備的資源受限，硬件隔離技術(shù)的應(yīng)用生態(tài)并不成熟，尚未出現(xiàn)一個通用的安全訪問控制模型，缺少理論支撐。

本文針對ARM-Android架構(gòu)，重點總結(jié)了2010年以來的Android訪問控制模型改進方案，并結(jié)合ARM TrustZone環(huán)境，提出了一種系統(tǒng)訪問控制的安全模型及形式化建模和驗證思路。結(jié)合機制安全性分析的相關(guān)工作，提出了可行的ARM-Android訪問控制安全研究方向。

2 ARM-Android平臺訪問控制機制

2.1 ARM-Android體系結(jié)構(gòu)

Android軟件棧自底向上依次是內(nèi)核、中間件和應(yīng)用層，其中中間件包括運行時環(huán)境和系統(tǒng)庫，以及應(yīng)用框架層。Android能搭載在不同架構(gòu)的硬件設(shè)備上，而ARM架構(gòu)在功耗和成本上的優(yōu)勢使其在移動終端占主要地位，其系統(tǒng)結(jié)構(gòu)如圖1所示。

Fig.1 ARM-Android system architecture圖1 ARM-Android系統(tǒng)結(jié)構(gòu)

2.2 訪問控制模型

訪問控制是信息安全保障機制的核心內(nèi)容，傳統(tǒng)的控制機制包括強制訪問控制（mandatory access control，MAC）和自主訪問控制（discretionary access control，DAC）。其中MAC通常是由系統(tǒng)對數(shù)據(jù)和用戶劃分安全等級標簽，用戶不能改變對象安全級別。DAC允許對象的屬主來制定該對象的保護策略，具有易用性與可擴展性。

根據(jù)策略應(yīng)用的具體場景，基本的訪問控制模型中加入了更多的授權(quán)環(huán)境要素，如基于角色的訪問控制（role-based access control，RBAC）、基于任務(wù)的訪問控制（task-based access control，TBAC）、基于屬性的訪問控制（attribute-based access control，ABAC）等，它們根據(jù)各自需求，能夠綜合實現(xiàn)MAC和DAC策略。圖2（a）是ABAC的基本授權(quán)示意圖。

在開放式網(wǎng)絡(luò)環(huán)境中動態(tài)、連續(xù)的訪問控制需求下，使用控制的核心模型增加義務(wù)和條件作為授權(quán)相關(guān)元素[8]，即訪問決策時要考慮主體獲得或行使對客體的訪問權(quán)前或過程中必須完成的操作和滿足的約束條件，其模型示意如圖2（b）所示。

Fig.2 Access control model圖2 訪問控制模型

2.3 安全機制

根據(jù)ARM-Android的系統(tǒng)結(jié)構(gòu)，其訪問控制機制主要包括硬件層、中間件及應(yīng)用框架層安全，如表1所示。

Table 1 Access control mechanisms for ARM-Android platforms表1 ARM-Android平臺的訪問控制機制

（1）ARM硬件隔離機制

近年主流的系統(tǒng)底層隔離技術(shù)包括構(gòu)建可信執(zhí)行環(huán)境（trusted execution environment，TEE）及虛擬化方式。其中TEE[9]主要基于CPU的特殊模式或安全硬件實現(xiàn)安全系統(tǒng)與普通系統(tǒng)的隔離。ARM TrustZone技術(shù)、SIM卡以及可信平臺模塊（trusted platform module，TPM）等，都提供了TEE環(huán)境。虛擬化在硬件層上增加虛擬器監(jiān)控層Hypervisor，ARM正著力于硬件擴展，提供虛擬化支持。

ARM TrustZone[10]作為最具代表性的TEE方法，得到了研究者和工業(yè)界的關(guān)注利用。TrustZone技術(shù)隔離片上系統(tǒng)硬件和軟件資源，使它們處于兩個區(qū)域，分別用于安全子系統(tǒng)和存儲其他內(nèi)容，其整體架構(gòu)如圖3所示，其中硬件邏輯可確保普通世界組件無法訪問安全世界資源。

Fig.3 ARM TrustZone architecture圖3 ARM TrustZone架構(gòu)圖

（2）Android沙箱隔離

Android使用內(nèi)核層Linux的訪問控制機制和運行時的虛擬機來實現(xiàn)沙箱隔離，從系統(tǒng)底層提供了基本的訪問控制機制。

設(shè)備中的應(yīng)用程序在安裝時，Android為每個應(yīng)用程序包進程分配一個單獨的用戶空間，并為它創(chuàng)建一個隔離的沙箱，擁有獨立地址空間和資源，使得不同應(yīng)用程序和進程間能夠互相隔離。

（3）Android權(quán)限機制

在應(yīng)用程序框架層，Android定義了權(quán)限機制，對應(yīng)用可以執(zhí)行的某些具體操作進行權(quán)限細分和訪問控制，并向用戶通知應(yīng)用程序使用的權(quán)限情況。

每個權(quán)限被定義成一個字符串，權(quán)限可由系統(tǒng)或用戶定義，主要包含權(quán)限名稱、所屬權(quán)限組和保護級別，保護級別代表了應(yīng)用使用權(quán)限時的認證方式。

Android6.0版本3）https://developer.android.com/guide/topics/security/permissions.html.實現(xiàn)了運行時權(quán)限動態(tài)檢測。用戶可以直接安裝應(yīng)用，當應(yīng)用的權(quán)限請求中包含不恰當?shù)臋?quán)限時，用戶可以拒絕授權(quán)。在程序運行時刻，系統(tǒng)通過引用監(jiān)視器，監(jiān)控組件通信過程，對權(quán)限保護的組件進行權(quán)限檢查，判斷通信過程是否能夠進行。

3 訪問控制機制改進

在ARM-Android已有的訪問控制機制基礎(chǔ)上，研究者在硬件、內(nèi)核、中間件以及綜合層次對模型進行改進優(yōu)化，增強機制安全，實現(xiàn)開放環(huán)境下可信方對敏感信息的使用控制，具體研究如下。

3.1 硬件層隔離

移動設(shè)備的訪問控制機制普遍利用軟件實現(xiàn)，其部署開銷和維護成本較高，系統(tǒng)隔離技術(shù)的日漸成熟為訪問控制提出了新的發(fā)展方案。

Sabt等人[9]提出結(jié)合可信計算環(huán)境的使用控制方案，通過TPM保護加密數(shù)據(jù)，然而TPM只能提供預(yù)定義的編程接口，存在局限性。Xu等人[11]提出基于TrustZone的嵌入式系統(tǒng)訪問控制增強模型，采用Domain and Type Enforcement、Bell-Lapadula等多策略的訪問控制方案。在分布式計算環(huán)境下，Bonnet等人[12]提出TEE上部署存儲、計算和數(shù)據(jù)傳輸架構(gòu)等，進行互聯(lián)網(wǎng)數(shù)據(jù)的共享使用控制。

此外，ARM TrustZone技術(shù)也為虛擬化提供了硬件支持。Varanasi等人[13]基于現(xiàn)有的硬件擴展技術(shù)，最早設(shè)計和實現(xiàn)了一個支持完全虛擬化的虛擬機監(jiān)視器（virtual machine monitor,VMM），并在模擬硬件上進行性能測試。vTZ[14]提出TEE虛擬化方案，結(jié)合硬件虛擬化和TrustZone來支持多個相互隔離的安全空間，并允許無縫地從TEE部署到虛擬化環(huán)境。在工業(yè)界，ARM TrustZone架構(gòu)也在嵌入式設(shè)備上得到廣泛應(yīng)用，如華為和支付寶采用的指紋支付技術(shù)、三星KNOX等。

3.2 內(nèi)核層改進

在內(nèi)核層對沙箱隔離機制進行改進，主要通過Linux內(nèi)核提供的接口掛接相應(yīng)鉤子，形成MAC模型。按照實現(xiàn)原理，改進方案主要分為以下兩種。

（1）基于標簽的訪問控制

由SELinux保護的操作系統(tǒng)為每個對象和主體存儲安全上下文標簽，每個訪問控制決策都依賴于訪問主體和客體的標簽。Shabtai等人[15]克服了系統(tǒng)結(jié)構(gòu)、安全配置等問題，將SELinux用在Android系統(tǒng)中，然而系統(tǒng)較為復(fù)雜，策略創(chuàng)建、優(yōu)化和維護消耗較大。

（2）基于路徑名的訪問控制

Balá?等人[16]在Linux內(nèi)核中增加了一個安全模塊，為每個應(yīng)用定義安全策略，當應(yīng)用程序進行系統(tǒng)調(diào)用時，進入訪問控制模塊，與應(yīng)用請求的資源路徑名匹配，實現(xiàn)MAC策略。

Liu等人[17]針對Android數(shù)據(jù)同步和程序調(diào)試時的權(quán)限泄露隱患，令手機用戶對每個文件建立控制策略，包含文件路徑和對應(yīng)的權(quán)限列表，根據(jù)對應(yīng)系統(tǒng)調(diào)用的參數(shù)與文件路徑名進行匹配，實現(xiàn)訪問控制。

3.3 中間件改進

在中間件對Android權(quán)限機制進行改進，目標集中在靜態(tài)授權(quán)擴展，訪問控制粒度細化，防止權(quán)限提升攻擊等方面。按照實現(xiàn)原理，中間件的改進可主要分為以下幾種。

Fig.4 Policy tree of Saint model圖4 Saint安全策略樹

（1）基于策略的訪問控制

Apex[18]擴展了基本的權(quán)限策略，增加運行時訪問控制，允許用戶動態(tài)改變授權(quán)，保持向后兼容性。Saint[19]根據(jù)Android系統(tǒng)不同層次的安全需求，完善了原有的權(quán)限機制策略，進而實現(xiàn)細粒度的訪問控制，如圖4所示。

（2）基于行為的訪問控制

Lei等人[20]利用時序邏輯描述語言，為關(guān)鍵系統(tǒng)資源訪問定義安全的行為模式，動態(tài)監(jiān)視應(yīng)用行為，實現(xiàn)訪問控制。研究者在中間件增加資源訪問安全行為定義、分配和實施模塊，證明能有效抵御短信服務(wù)的惡意攻擊，但該方案存在安全行為模式定義的局限性，且當訪問的安全資源增加時，性能損耗增加，系統(tǒng)難以部署和維護。

（3）基于標簽的訪問控制

YAASE[21]將保護數(shù)據(jù)與用戶定義的標簽結(jié)合，利用TaintDroid[22]進行數(shù)據(jù)和跟蹤，并根據(jù)細粒度訪問策略控制數(shù)據(jù)傳遞，防止惡意軟件通過網(wǎng)絡(luò)訪問或共謀攻擊竊取敏感信息。Huang[23]在Android應(yīng)用框架層中引入保護域和應(yīng)用白名單，根據(jù)白名單將安裝應(yīng)用與相應(yīng)保護域綁定。將Android應(yīng)用的保護域作為訪問控制的標簽，保證應(yīng)用授予的權(quán)限范圍，進而限制應(yīng)用行為。然而，該方案僅使用權(quán)限靜態(tài)分析，在應(yīng)用安裝時刻指派保護域，仍存在運行時的權(quán)限泄露。

（4）基于上下文的訪問控制

CRePE[24]是早期在Android系統(tǒng)中實現(xiàn)上下文相關(guān)的訪問控制方案。根據(jù)用戶定義的上下文控制策略，在不同情境轉(zhuǎn)換時對應(yīng)用權(quán)限進行細粒度控制。在中間件，CRePE對系統(tǒng)代碼進行修改，增加了必要構(gòu)件，并為用戶和可信方提供了策略定義接口。Shebaro等人[25]使用輕量級的控制方案，利用4個構(gòu)件收集上下文信息，進行策略管理和執(zhí)行，增加應(yīng)用對資源的訪問權(quán)力、系統(tǒng)方法、功能、用戶數(shù)據(jù)和服務(wù)的限制。

3.4 多層次安全策略

多層次的安全策略同時借鑒了沙箱隔離和權(quán)限機制的改進模型思想，實現(xiàn)更加靈活的訪問控制。

Bugiel等人[26]通過對Android的系統(tǒng)行為進行啟發(fā)式分析，提出一個以系統(tǒng)為中心，策略驅(qū)動的多層次運行時控制，在中間件控制通信，并提供內(nèi)核和中間件間的回調(diào)機制。MPdroid[27]在內(nèi)核層利用Linux安全模塊（Linux security module,LSM）對進程間通信進行控制，在應(yīng)用框架層采用RBAC機制，框架層中的RBAC數(shù)據(jù)庫包括角色信息、權(quán)限信息和對應(yīng)用的控制規(guī)則。

TrustDroid[28]實現(xiàn)了Android軟件棧上不同層次上的隔離。在內(nèi)核層使用TOMOYO模型，在中間件控制域間的通信和數(shù)據(jù)訪問，在應(yīng)用層允許基于上下文的網(wǎng)絡(luò)訪問控制。該方案增加輕量級有效隔離，為訪問控制安全提供了新方向。

3.5 使用控制

結(jié)合分布式系統(tǒng)架構(gòu)中的使用控制策略，Lazouski等人[8]針對云端使用控制交互的終端設(shè)備，通過部署數(shù)據(jù)保護系統(tǒng)和UXACML授權(quán)系統(tǒng)兩個主要部件，實現(xiàn)了數(shù)據(jù)使用控制方案。其中，受保護的數(shù)據(jù)在設(shè)備中加密存儲，數(shù)字保護系統(tǒng)控制數(shù)據(jù)訪問，授權(quán)系統(tǒng)提供訪問決策與授權(quán)。

Bai等人[29]則采用在使用控制模型上增加上下文感知的方案，構(gòu)建ConUCON模型。形式化模型包括7個構(gòu)件，分別是主體、客體、屬性狀態(tài)、權(quán)力、權(quán)限、義務(wù)和上下文。其中上下文定義為環(huán)境和系統(tǒng)屬性，如CPU速率、電池、設(shè)備位置和時間等。

表2對強制訪問控制、權(quán)限機制以及使用控制機制在Android系統(tǒng)中的利用效率、靈活性和易用性等方面進行對比分析。表3具體總結(jié)了Android不同系統(tǒng)層次的訪問控制方案。聯(lián)系不同系統(tǒng)層次下模型改進的優(yōu)缺點，可以提出進一步的優(yōu)化方向。采用多層次多策略的訪問控制方案，能夠綜合策略的性能優(yōu)勢，然而這也同時增加了方案實現(xiàn)的復(fù)雜度，控制模型的設(shè)計不適用于復(fù)雜的機制實現(xiàn)。因此在優(yōu)化訪問控制策略的基礎(chǔ)上，也需要選擇一種面向應(yīng)用實現(xiàn)的模型設(shè)計方法。

Table 2 Comparison of access control mechanisms表2 訪問控制機制對比

4 基于B方法的訪問控制模型

基于TrustZone架構(gòu)的Android系統(tǒng)中，安全機制復(fù)雜，實現(xiàn)和證明難度較大，實際中也并未出現(xiàn)理想的系統(tǒng)設(shè)計方案與完備的評測體系。本研究從ARM-Android平臺的訪問控制著手，設(shè)計輕量級機制，并應(yīng)用B方法進行模型抽象和規(guī)范的形式化證明，在理論上保證設(shè)計模塊的安全性，并通過相應(yīng)工具生成系統(tǒng)可執(zhí)行代碼，保證工程實現(xiàn)與理論模型的統(tǒng)一，具有可行性。針對訪問控制機制的形式化抽象和分析方法，也能作為其他安全模塊的構(gòu)建和分析基礎(chǔ)，為更多的安全機制設(shè)計與系統(tǒng)安全證明提供一種實際有效的途徑。

Table 3 Access control security enhancements forAndroid表3 Android訪問控制改進方案

4.1 系統(tǒng)分析

在TrustZone架構(gòu)上實現(xiàn)Android系統(tǒng)保護，需要在嵌入式內(nèi)核中集成TrustZone驅(qū)動，并在中間件實現(xiàn)TrustZone本地系統(tǒng)庫和客戶端服務(wù)進程，Android系統(tǒng)本身也提供了強大的技術(shù)支持。以手機支付場景為例，對硬件安全世界內(nèi)的敏感信息進行訪問控制，大體過程如下：

（1）普通世界（normal world，NW）中，Android應(yīng)用層的支付應(yīng)用向應(yīng)用框架層的TrustZone客戶端服務(wù)發(fā)出請求。

（2）TrustZone客戶端服務(wù)收到應(yīng)用請求后，調(diào)用TrustZone API實現(xiàn)的本地系統(tǒng)庫，向內(nèi)核層的Trust-Zone驅(qū)動發(fā)出請求。

（3）TrustZone驅(qū)動處理相應(yīng)的請求，通過SMC命令，切換到安全世界（secure world，SW）中的Monitor模式。

（4）在Monitor模式下，完全切換到安全操作系統(tǒng)的系統(tǒng)堆?？臻g以及進程空間，安全操作系統(tǒng)通知TrustZone服務(wù)端處理任務(wù)，進而分發(fā)安全性任務(wù)請求。

（5）SW中，安全操作系統(tǒng)的應(yīng)用層處理對應(yīng)的任務(wù)請求，具體執(zhí)行安全代碼、敏感資源和相關(guān)外設(shè)訪問。

（6）SW中的任務(wù)執(zhí)行完畢后，根據(jù)需求切換到NW。

可見，一個基本的訪問過程包含硬件、軟件兩個層次，涉及了兩個獨立的操作系統(tǒng)及其切換過程等。因此需要根據(jù)實際的系統(tǒng)結(jié)構(gòu)分層建立基本抽象機，在操作規(guī)范中不僅要描述完整的資源訪問過程，還有系統(tǒng)世界切換動作，保證敏感資源始終處于安全隔離狀態(tài)。

此外，在Android軟件棧中的訪問控制包含了內(nèi)核層和中間件層次，類似于傳統(tǒng)操作系統(tǒng)中的用戶空間和內(nèi)核空間，軟件抽象機需要進一步分層，描述用戶空間的應(yīng)用運行與通信，并對應(yīng)內(nèi)核空間中的進程通信，在內(nèi)核空間中實現(xiàn)基于策略的強制訪問控制。根據(jù)上述分析，將采用形式化B方法模塊化構(gòu)建系統(tǒng)抽象機。

4.2 B方法

在安全攸關(guān)的領(lǐng)域，利用基于模型的形式化方法進行軟件系統(tǒng)開發(fā)，可以彌補常見的需求規(guī)格說明與需求管理的缺陷。B方法[30]作為典型的形式化方法，在Atelier B等工具支持下，能夠根據(jù)需求構(gòu)建抽象模型，對抽象機不斷精化，最終生成系統(tǒng)的可執(zhí)行代碼，其過程如圖5所示。它在保證精確的形式化語義和嚴格推理的同時，更面向?qū)嶋H和計算機應(yīng)用。

Fig.5 Construction process of B method-based access control module圖5 基于B方法的訪問控制模塊構(gòu)建流程

4.3 模型抽象

依據(jù)上述系統(tǒng)分析，需要對兩個層次的訪問控制機制進行抽象。以硬件層訪問控制機制為例，首先對控制規(guī)則進行非形式化描述，再通過形式化抽象，得到抽象機規(guī)范。建模過程中并未描述應(yīng)用、組件通信、SW中的安全存儲、完整性驗證等細節(jié)，這是由于初步的模型高度抽象，主要包含安全屬性強相關(guān)的抽象結(jié)構(gòu)，在后續(xù)的模型精化過程中可以加入更多的具體化操作，用更接近計算機實現(xiàn)的結(jié)構(gòu)代替抽象結(jié)構(gòu)。

（1）基本要素

針對系統(tǒng)進程對敏感資源的訪問控制，需要定義基本的部分訪問控制要素和控制規(guī)則。其中，基本要素包括資源實體、系統(tǒng)狀態(tài)等，各要素抽象應(yīng)當符合B方法的語法定義。要素對應(yīng)的系統(tǒng)操作定義應(yīng)保證滿足定義的訪問控制規(guī)則。系統(tǒng)抽象機的訪問控制規(guī)則和部分要素分別如表4、表5所示。隨著抽象機規(guī)模的擴大，訪問要素及規(guī)則會繼續(xù)增加。

（2）構(gòu)建抽象機

依據(jù)上述訪問控制要素建立抽象機M1,建立TrustZone的訪問控制形式化規(guī)范，形式如圖6所示。

對Android軟件層次的訪問控制機制的抽象與上述步驟類似，在Android訪問控制模型研究的基礎(chǔ)上，提出對系統(tǒng)資源的強制訪問控制策略，并進行規(guī)范證明。在構(gòu)建軟件層的抽象機時，可以進一步分解為內(nèi)核層、中間件的訪問控制機制，獨立的成員抽象機的內(nèi)在一致性可以獨立證明。在構(gòu)建硬件、軟件層次的抽象機M1、M2后，以遞增的方式構(gòu)造抽象機規(guī)范，組合構(gòu)建為ARM-Android平臺上的訪問控制模塊，圖7（a）是抽象機合并構(gòu)造的語法定義，（b）是整體結(jié)構(gòu)。

Table 4 Basic control rules表4 基本控制規(guī)則

Fig.6 Abstract machine of hardware layer圖6 硬件層抽象機

Fig.7 Formal model structure圖7 形式化模型結(jié)構(gòu)圖

Table 5 Basic elements of access control mechanism表5 訪問控制基本要素

在得到B語言描述的訪問控制機制形式化規(guī)范后，進一步精化，在抽象模型中加入具體細節(jié)，并利用Atelier B工具生成證明任務(wù)，通過證明得到最終的可實現(xiàn)代碼。

5 相關(guān)工作

盡管ARM-Android采用了多層次的安全模型保證應(yīng)用隔離和訪問控制，其中仍存在系統(tǒng)漏洞，造成權(quán)限泄露等。對安全機制進行漏洞挖掘和形式化分析，也是機制研究的重要工作。以Android權(quán)限機制分析為例，研究者通過分析策略實現(xiàn)中的漏洞，用形式化方法分析安全策略的定義描述，保證安全機制完備性。

5.1 機制漏洞分析

Faruki等人[1]對Android系統(tǒng)安全進行綜述，提出Android系統(tǒng)安全問題主要分為版本更新、Native代碼執(zhí)行以及不同威脅攻擊。Fang等人[2]從直接、間接兩方面詳細分析了Android權(quán)限機制的安全風險，包括過度授權(quán)、權(quán)限提升攻擊等。其中，應(yīng)用級別的權(quán)限提升攻擊可以分為混淆代理攻擊和共謀攻擊。Felt等人[31]將權(quán)限提升稱為權(quán)限再次授權(quán)攻擊，分析了其攻擊方法和防御方案。此外，盡管Android系統(tǒng)新版本采用新的權(quán)限機制，并加強內(nèi)核層的訪問控制，但仍無法達到預(yù)期安全性，對于廣大用戶仍存在文檔說明不足，權(quán)限控制不力，影響用戶體驗等現(xiàn)實問題。因此，仍需要在理論分析和工程實踐兩方面對Android訪問控制機制深入研究。

5.2 形式化分析

Shin等人[32]最早針對權(quán)限機制建立了一個基于狀態(tài)的形式化模型，根據(jù)官方文檔對機制安全規(guī)范進行抽象，利用Coq工具輔助性證明機制安全規(guī)范存在的不足。該模型沒有考慮應(yīng)用與系統(tǒng)之間的交互關(guān)系。Fragkaki等人[33]從系統(tǒng)動態(tài)角度對Android權(quán)限機制進行抽象建模，直接對應(yīng)用組件進行形式化定義，分析權(quán)限再次授權(quán)和撤銷過程中的安全屬性。該模型缺少其他屬性的相關(guān)操作定義，如權(quán)限保護級別定義等。

隨著Android平臺更新和機制研究逐步成熟，Betarte等人[34]提出了一個綜合的權(quán)限機制狀態(tài)機模型，在Android應(yīng)用定義中增加對組件的描述，并考慮到運行時實例化等，其完整性、可表達性更強。與單純地構(gòu)建權(quán)限形式化系統(tǒng)不同，Armando等人[35]采用基于語言的形式化建模，擴展了Chaudhuri[36]提出的類型系統(tǒng)，建立Android應(yīng)用框架模型和多層統(tǒng)一的完整評估方案。

不同于Shin[32]和Betarte[34]的工作，本文建立的形式化訪問控制模型考慮了硬件隔離，并綜合多層次策略，旨在構(gòu)建滿足安全需求的可行模塊。文獻[33]同樣采用了從抽象模型到工程實踐的思路，提出了SOREBET方案，但文中的模型抽象化程度高，無法證明形式化模型和應(yīng)用實現(xiàn)的統(tǒng)一性。而本文利用了形式化B方法面向應(yīng)用的獨有特點，抽象模型中的操作對應(yīng)工程應(yīng)用中的動作，并始終維持定義的安全不變式，通過逐步精化引入可實現(xiàn)結(jié)構(gòu)，能夠保證理論與實踐的統(tǒng)一。形式化建模為訪問控制機制研究提供了理論支撐，同時工程實現(xiàn)暴露出的機制漏洞，為抽象模型的安全性條件提供補充，促進模型的完善和進一步實現(xiàn)。

6 研究趨勢

總結(jié)近年來ARM-Android訪問控制機制研究可以看出，一些成熟的訪問控制模型在平臺中并不能充分適用，同時在開放環(huán)境下，需要軟硬件結(jié)合的隔離執(zhí)行方式。綜合考慮平臺攻擊和訪問控制模型的實用性、可靠性，提出以下幾點研究趨勢：

（1）建立面向隔離執(zhí)行環(huán)境的ARM-Android平臺的輕量級訪問控制模型，實現(xiàn)細粒度權(quán)限機制，并盡可能減小可信計算基的規(guī)模。

（2）結(jié)合常見形式化規(guī)范語言和定理證明方法，建立合理的形式化模型，并在理論上對訪問控制機制進行安全性分析。

（3）針對模型中的規(guī)則沖突問題，進行有效的沖突檢測，保證訪問控制規(guī)則的一致性和完整性。

（4）基于ARM-Android平臺在開放環(huán)境下的多種安全需求進一步完善機制，包括數(shù)據(jù)安全、安全連接、管理策略安全等需求，構(gòu)建成體系的模型系統(tǒng)。

本文根據(jù)ARM-Android平臺的訪問控制機制分析，為上述研究趨勢提出一個可行方案：采用基于標簽的訪問控制方法，定義關(guān)鍵資源的上下文標簽，將應(yīng)用的使用權(quán)限具體映射到系統(tǒng)資源以細化權(quán)限粒度，并進行使用控制。明確安全方案的保護目標，針對防止權(quán)限泄露定義訪問策略和安全屬性，建立相應(yīng)的威脅模型。進一步利用B語言形式化描述訪問控制方案，并對系統(tǒng)安全性進行邏輯證明?；谛问交疊方法建立訪問控制模型，既能夠在抽象階段通過類型檢查和模型證明檢驗設(shè)計方案的正確性和完備性，又能夠保證工程實現(xiàn)與形式化模型相統(tǒng)一，避免安全機制規(guī)范的不足。這是嵌入式系統(tǒng)訪問控制安全領(lǐng)域內(nèi)的較新嘗試。

7 總結(jié)

本文針對ARM-Android平臺上的訪問控制機制研究，總結(jié)了系統(tǒng)不同架構(gòu)層上的安全機制，并分類對比了不同策略的訪問控制模型改進方案。基于ARM TrustZone架構(gòu)，提出建立多層次、輕量級的訪問控制模型，并利用B方法進行形式化規(guī)范和驗證的研究方案。通過抽象控制要素和控制規(guī)則，限制系統(tǒng)對敏感資源的訪問操作。結(jié)合形式化B方法面向應(yīng)用的特點，通過建立規(guī)范抽象機，逐步精化實現(xiàn)可執(zhí)行的代碼模塊。最后結(jié)合機制安全分析相關(guān)工作，提出未來研究的方向，分析利用B方法進行訪問控制模塊設(shè)計的特點，保證形式化模型抽象與工程實際相統(tǒng)一。

[1]Faruki P,BharmalA,Laxmi V,et al.Android security:a survey of issues,malware penetration and defenses[J].IEEE Communications Surveys&Tutorials,2015,17(2):998-1022.

[2]Fang Zheran,Han Weili,Li Yingjiu.Permission based Android security:issues and countermeasures[J].Computers&Security,2014,43(6):205-218.

[3]Zhang Yuqing,Wang Kai,Yang Huan,et al.Survey of Android OS security[J].Journal of Computer Research and Development,2014,51(7):1385-1396.

[4]Arena V,Catania V,La Torre G,et al.SecureDroid:an Android security framework extension for context-aware policy enforcement[C]//Proceedings of the 2013 International Conference on Privacy and Security in Mobile Systems,Atlantic City,USA,Jun 24-27,2013.Piscataway,USA:IEEE,2013:1-8.

[5]Sahs J,Khan L.A machine learning approach to Android malware detection[C]//Proceedings of the 2012 European Intelligence and Security Informatics Conference,Odense,Denmark,Aug 22-24,2012.Washington:IEEE Computer Society,2012:141-147.

[6]Feng Yu,Anand S,Dillig I,et al.Apposcopy:semanticsbased detection of Android malware through static analysis[C]//Proceedings of the 22nd International Symposium on Foundations of Software Engineering,Hong Kong,China,Nov 16-21,2014.New York:ACM,2014:576-587.

[7]Zhou Yajin,Wang Zhi,Zhou Wu,et al.Hey,you,get off of my market:detecting malicious Apps in official and alternative Android markets[C]//Proceedings of the 19th Annual Network and Distributed System Security Symposium,San Diego,USA,Feb 5-8,2012.Reston,USA:The Internet Society,2012.

[8]Lazouski A,Martinelli F,Mori P,et al.Stateful data usage control for Android mobile devices[J].International Journal of Information Security,2016,8743:1-25.

[9]Sabt M,Achemlal M,Bouabdallah A.Trusted execution environment:what it is,and what it is not[C]//Proceedings of the 14th International Conference on Trust,Security and Privacy in Computing and Communications,Helsinki,Finland,Aug 20-22,2015.Washington:IEEE Computer Society,2015:57-64.

[10]ARM security technology building a secure system using TrustZone technology[EB/OL].[2017-01-06].http://infocenter.arm.com/help/index.jsp?topic=/com.arm.doc.prd29-genc-009492c/index.html.

[11]Xu Yanling,Pan Wei,Zhang Xinguo.Design and implementation of secure embedded systems based on TrustZone[C]//Proceedings of the 2008 International Conference on Embedded Software and Systems,Chengdu,China,Jul 29-31,2008.Washington:IEEE Computer Society,2008:136-141.

[12]Bonnet P,González J,Granados J.A distributed architecture for sharing ecological data sets with access and usage control guarantees[C]//Proceedings of the 7th International Congress on Environmental Modelling and Software,San Diego,USA,Jun 15-19,2014:1-7.

[13]Varanasi P,Heiser G.Hardware-supported virtualization on ARM[C]//Proceedings of the 2011 Asia-Pacific Workshop on Systems,Shanghai,Jul 11-12,2011.New York:ACM,2011:11.

[14]vTZ:TrustZone and TEE virtualization[EB/OL].[2017-01-18].https://www.trustkernel.com/en/products/hypervisor/vtz.html.

[15]Shabtai A,Fledel Y,Elovici Y.Securing Android-poweredmobile devices using SELinux[J].IEEE Security&Privacy Magazine,2010,8(3):36-44.

[16]Balá? A,Mado? B,Ambróz M.Android access control extension[J].Acta Informatica Pragensia,2015,4(3):310-317.

[17]Liu Changping,Fan Mingyu,Wang Guangwei,et al.Lightweight access control oriented toward Android[J].Application Research of Computers,2010,27(7):2611-2613.

[18]Nauman M,Khan S,Zhang Xinwen.Apex:extending Android permission model and enforcement with user-defined runtime constraints[C]//Proceedings of the 5th ACM Symposium on Information,Computer and Communications Security,Beijing,Apr 13-16,2010.New York:ACM,2010:328-332.

[19]Ongtang M,Mclaughlin S,Enck W,et al.Semantically rich application-centric security in Android[J].Security&Communication Networks,2012,5(6):658-673.

[20]Lei Lingguang,Jing Jiwu,Wang Yuewu,et al.A behaviorbased system resources access control scheme for Android[J].Journal of Computer Research and Development,2014,51(5):1028-1038.

[21]Russello G,Crispo B,Fernandes E,et al.YAASE:yet another android security extension[C]//Proceedings of the 3rd International Conference on Privacy,Security,Risk and Trust and 3rd International Conference on Social Computing,Boston,USA,Oct 9-11,2011.Piscataway,USA:IEEE,2011:1033-1040.

[22]Enck W,Gilbert P,Han S,et al.TaintDroid:an informationflow tracking system for realtime privacy monitoring on smartphones[J].ACM Transactions on Computer Systems,2014,32(2):5.

[23]Huang Qing.An extension to the Android access control framework[D].Link?ping,Sweden:Link?ping University,2011.

[24]Conti M,Crispo B,Fernandes E,et al.CRêPE:a system for enforcing fine-grained context-related policies on Android[J].IEEE Transactions on Information Forensics&Security,2012,7(5):1426-1438.

[25]Shebaro B,Oluwatimi O,Bertino E.Context-based access control systems for mobile devices[J].IEEE Transactions on Dependable&Secure Computing,2015,12(2):150-163.

[26]Bugiel S,Davi L,Dmitrienko A,et al.Towards taming privilege-escalation attacks on Android[C]//Proceedings of the 19th Annual Network and Distributed System Security Symposium,San Diego,USA,Feb 5-8,2012.Reston,USA:The Internet Society,2012:346-360.

[27]Guo Tao,Zhang Puhan,Liang Hongliang,et al.Enforcing multiple security policies for Android system[C]//Proceedings of the 2nd International Symposium on Computer,Communication,Control and Automation,Singapore,Dec 1-2,2013.Red Hook,USA:CurranAssociates,2013:165-169.

[28]Bugiel S,Davi L,Dmitrienko A,et al.Practical and lightweight domain isolation on Android[C]//Proceedings of the 1st ACM Workshop Security and Privacy in Smartphones and Mobile Devices,Chicago,USA,Oct 17,2011.New York:ACM,2011:51-62.

[29]Bai Guangdong,Gu Liang,Feng Tao,et al.Context-aware usage control for Android[C]//LNICST 50:Proceedings of the 2010 International Conference on Security and Privacy in Communication Systems,Singapore,Sep 7-9,2010.Berlin,Heidelberg:Springer,2010:326-343.

[30]Abrial J R.The B-book:assigning programs to meanings[M].New York:Cambridge University Press,2005.

[31]Felt A P,Wang H J,Moshchuk A,et al.Permission redelegation:attacks and defenses[C]//Proceedings of the 20th USENIX Conference on Security,San Francisco,USA,Aug 8-12,2011.Berkeley,USA:USENIX Association,2011:22-22.

[32]Shin W,Kiyomoto S,Fukushima K,et al.A formal model to analyze the permission authorization and enforcement in the Android framework[C]//Proceedings of the 2nd International Conference on Social Computing,Minneapolis,USA,Aug 20-22,2010.Washington:IEEE Computer Society,2010:944-951.

[33]Fragkaki E,Bauer L,Jia L,et al.Modeling and enhancing Android’s permission system[C]//LNCS 7459:Proceedings of the 17th European Symposium on Research in Computer Security,Pisa,Italy,Sep 10-12,2012.Berlin,Heidelberg:Springer,2012:1-18.

[34]Betarte G,Campo J D,Luna C,et al.Verifying Android’s permission model[C]//LNCS 9399:Proceedings of the 12th International Colloquium on Theoretical Aspects of Computing,Cali,Colombia,Oct 29-31,2015.Cham:Springer,2015:485-504.

[35]Armando A,Costa G,Merlo A.Formal modeling and rea-soning about the Android security framework[C]//LNCS 8191:Proceedings of the 7th International Symposium on Trustworthy Global Computing,Newcastle upon Tyne,UK,Sep 7-8,2012.Berlin,Heidelberg:Springer,2012:64-81.

[36]Chaudhuri A.Language-based security on Android[C]//Proceedings of the 4th Workshop on Programming Languages and Analysis for Security,Dublin,Ireland,Jun 15-21,2009.New York:ACM,2009:1-7.

附中文參考文獻：

[3]張玉清,王凱,楊歡,等.Android安全綜述[J].計算機研究與發(fā)展,2014,51(7):1385-1396.

[17]劉昌平,范明鈺,王光衛(wèi),等.Android手機的輕量級訪問控制[J].計算機應(yīng)用研究,2010,27(7):2611-2613.

[20]雷靈光,荊繼武,王躍武,等.一種基于行為的Android系統(tǒng)資源訪問控制方案[J].計算機研究與發(fā)展,2014,51(5):1028-1038.

Research Progress onAccess Control Mechanisms forARM-Android Platforms*

REN Lu,YIN Qing,CHANG Rui+,JIANG Hang
State Key Laboratory of Mathematical Engineering andAdvanced Computing,Zhengzhou 450001,China

A

TP309.1

+Corresponding author:E-mail:crix1021@163.com

REN Lu,YIN Qing,CHANG Rui,et al.Research progress on access control mechanisms for ARM-Android platforms.Journal of Frontiers of Computer Science and Technology,2017,11(10)：1545-1556.

ISSN 1673-9418 CODEN JKYTA8

Journal of Frontiers of Computer Science and Technology

1673-9418/2017/11(10)-1545-12

10.3778/j.issn.1673-9418.1702049

E-mail:fcst@vip.163.com

http://www.ceaj.org

Tel:+86-10-89056056

*The National Natural Science Foundation of China under Grant No.61572516(國家自然科學基金).

Received 2017-02,Accepted 2017-07.

CNKI網(wǎng)絡(luò)優(yōu)先出版:2017-07-04,http://kns.cnki.net/kcms/detail/11.5602.TP.20170704.1805.004.html

REN Lu was born in 1993.She is an M.S.candidate at Information Engineering University.Her research interest is embedded system security.

任璐（1993—），女，河南開封人，信息工程大學碩士研究生，主要研究領(lǐng)域為嵌入式系統(tǒng)安全。

YIN Qing was born in 1968.She received the Ph.D.degree from Information Engineering University in 2006.Now she is a professor at Information Engineering University.Her research interest is computer application.

尹青（1968—），女，湖北武漢人，2006年于信息工程大學獲得博士學位，現(xiàn)為信息工程大學教授，主要研究領(lǐng)域為計算機應(yīng)用。

CHANG Rui was born in 1981.She received the M.S.degree from Wuhan University of Technology in 2007.Now she is an associate professor at Information Engineering University,and Ph.D.candidate and visiting scholar at Zhejiang University.Her research interests include computer architecture and embedded system security,etc.

常瑞（1981—），女，河南鄭州人，2007年于武漢理工大學獲得碩士學位，現(xiàn)為信息工程大學副教授，浙江大學博士訪問學者，主要研究領(lǐng)域為計算機體系架構(gòu)，嵌入式系統(tǒng)安全等。

JIANG Hang was born in 1989.He is an M.S.candidate at Information Engineering University.His research interest is embedded system security.

蔣航（1989—），男，浙江東陽人，信息工程大學碩士研究生，主要研究領(lǐng)域為嵌入式系統(tǒng)安全。