TrustZone中斷隔離機(jī)制的形式化驗(yàn)證

付俊儀,張倩穎,2,3,王國輝,2,李希萌,4,施智平,4,關(guān) 永,5

1(首都師范大學(xué) 信息工程學(xué)院,北京 100048)

2(高可靠嵌入式系統(tǒng)北京市工程研究中心,北京 100048)

3(中國科學(xué)院計(jì)算技術(shù)研究所 計(jì)算機(jī)體系結(jié)構(gòu)國家重點(diǎn)實(shí)驗(yàn)室,北京 100190)

4(電子系統(tǒng)可靠性技術(shù)北京市重點(diǎn)實(shí)驗(yàn)室,北京 100048)

5(北京成像理論與技術(shù)高精尖創(chuàng)新中心,北京 100048)

1 引 言

嵌入式設(shè)備被廣泛應(yīng)用于生產(chǎn)生活的各個(gè)領(lǐng)域,能夠獲取、存儲(chǔ)以及操作大量敏感數(shù)據(jù),一旦遭受軟件攻擊會(huì)導(dǎo)致敏感信息泄露.為了解決嵌入式設(shè)備安全的問題,2003年ARM公司推出TrustZone技術(shù)[1],該技術(shù)通過對處理器、內(nèi)存、外設(shè)等硬件進(jìn)行安全擴(kuò)展,將軟件和硬件資源劃分為安全世界和普通世界,即可信執(zhí)行環(huán)境(Trusted Execution Environment,TEE)和通用執(zhí)行環(huán)境(Rich Execution Environment,REE).TEE和REE之間的切換由Monitor在監(jiān)視器模式下管理.TrustZone為TEE中的可信軟件提供安全保護(hù),確保REE無法獲取安全資源的訪問權(quán)限,從而為兩者提供可靠的安全邊界.通過在TEE中運(yùn)行安全性要求較高的應(yīng)用(如指紋識別等),在REE中運(yùn)行其他應(yīng)用(如音樂播放器等),可以保護(hù)高安全需求的應(yīng)用免受來自REE的軟件攻擊,提高嵌入式設(shè)備的安全性.

TEE的安全性是保證嵌入式系統(tǒng)安全的基礎(chǔ),一旦TEE隔離環(huán)境被破壞,那么受TEE保護(hù)的敏感信息就會(huì)被泄露,給用戶帶來極其嚴(yán)重的安全問題和財(cái)產(chǎn)損失.近些年TEE的漏洞不斷被發(fā)現(xiàn),例如NVIDIA公布了TEE OS存在由于缺乏堆強(qiáng)化(Heap Hardening)而導(dǎo)致堆溢出的漏洞(CVE-2021-34373)[2]和TEE OS訪問權(quán)限設(shè)置中因沒有正確限制本地特權(quán)用戶對資源的訪問而存在的漏洞(CVE-2021-34395)[2];360安全團(tuán)隊(duì)發(fā)現(xiàn)華為手機(jī)TEE OS模塊中存在輸入校驗(yàn)錯(cuò)誤,獲取root權(quán)限的攻擊者可以修改TEE OS模塊的內(nèi)核態(tài)內(nèi)存數(shù)據(jù),從而導(dǎo)致TEE OS被篡改或惡意代碼執(zhí)行(CVE-2015-4422)[3].因此,為了確保TEE的安全性,需要對TEE隔離機(jī)制的正確性進(jìn)行驗(yàn)證.

外設(shè)隔離是TrustZone硬件隔離技術(shù)之一,在TrustZone技術(shù)中,外設(shè)被劃分為安全世界外設(shè)和普通世界外設(shè),普通世界不能訪問安全世界外設(shè).中斷分為安全中斷和非安全中斷,安全外設(shè)發(fā)出安全中斷,非安全外設(shè)發(fā)出非安全中斷.安全中斷由安全世界處理,非安全中斷由普通世界處理.如果沒有正確的實(shí)現(xiàn)中斷隔離,可能會(huì)導(dǎo)致安全中斷被普通世界處理,從而導(dǎo)致安全世界外設(shè)遭受來自普通世界惡意軟件的攻擊.因此,對中斷隔離機(jī)制的驗(yàn)證是保障TrustZone安全性的重要環(huán)節(jié).

應(yīng)用形式化方法驗(yàn)證可信執(zhí)行環(huán)境已經(jīng)有很多研究工作,但是目前對ARM TrustZone中斷隔離機(jī)制的驗(yàn)證工作很少.現(xiàn)有大多數(shù)涉及中斷的驗(yàn)證工作主要存在3方面問題:首先,模型中主要建模了設(shè)備驅(qū)動(dòng)程序[4-7],未建模發(fā)生中斷時(shí)的中斷處理程序調(diào)用[4-7]、中斷處理時(shí)的上下文切換等過程[4,6],而這些過程都是中斷處理的必要環(huán)節(jié);其次,有些工作建模時(shí)僅考慮軟件和部分硬件組件[7,8],未考慮一些關(guān)鍵硬件組件,如未建模中斷控制器[7]和處理器[8],而中斷處理是軟件和硬件協(xié)同操作的過程,關(guān)鍵硬件操作的正確性是中斷隔離機(jī)制正確實(shí)現(xiàn)的基礎(chǔ);最后,大部分研究在驗(yàn)證時(shí)主要考慮正確性屬性[4-7],未考慮信息流安全性,而中斷處理的過程中可能存在隱蔽的信息流通道.

本文根據(jù)ARMv8規(guī)范[9],對基于TrustZone構(gòu)建的可信執(zhí)行環(huán)境的中斷隔離機(jī)制進(jìn)行形式化建模與驗(yàn)證.本文模型充分考慮了中斷處理過程中的細(xì)節(jié),包括調(diào)用中斷處理程序、執(zhí)行上下文切換等過程以及關(guān)鍵軟硬件組件的操作,并在定理證明器Isabelle/HOL[10]中對ARMv8 TrustZone中斷隔離機(jī)制的正確性和信息流安全性進(jìn)行形式化定義與驗(yàn)證.本文的主要貢獻(xiàn)如下:

1)提出了一個(gè)包含TrustZone中斷隔離關(guān)鍵軟硬件的形式化模型.建模的軟件包括中斷處理程序、TrustZone Monitor和異常向量表,建模的硬件組件包括通用中斷控制器(Generic Interrupt Controller,GIC)[11]、TrustZone地址空間控制器(TrustZone Address Space Controller,TZASC)[12]、與中斷處理相關(guān)的寄存器和內(nèi)存.本文采用狀態(tài)遷移系統(tǒng)的建模方法,狀態(tài)包括寄存器和內(nèi)存,狀態(tài)遷移由中斷處理事件和內(nèi)存讀寫事件驅(qū)動(dòng).

2)定義了TrustZone中斷隔離機(jī)制的安全屬性:正確性和信息流安全性.正確性確保中斷被正確地處理,表示安全中斷在安全世界中處理,非安全中斷在普通世界中處理.信息流安全性通過無干擾、無泄露和無影響屬性定義,表示在系統(tǒng)運(yùn)行的過程中不存在違反安全策略的信息流.

3)驗(yàn)證了模型滿足定義的安全屬性.在Isabelle/HOL中建模并驗(yàn)證模型的安全屬性,采用展開條件(Unwinding Condition)證明模型的信息流安全性,驗(yàn)證結(jié)果表明在中斷處理的過程中不存在隱蔽的信息流通道.

本文的其余部分組織如下.第2節(jié)簡述TrustZone的中斷隔離機(jī)制.第3節(jié)介紹TrustZone中斷隔離機(jī)制的形式化模型.第4節(jié)描述TrustZone中斷處理功能正確性和信息流安全性的形式化定義.第5節(jié)闡述安全屬性的形式化驗(yàn)證.第6節(jié)介紹本文的相關(guān)工作.第7節(jié)總結(jié)全文.

2 TrustZone的中斷隔離機(jī)制

ARMv8 TrustZone的中斷處理架構(gòu)如圖1所示.ARMv8是ARM的64位指令集架構(gòu),支持4個(gè)異常級別,通常在EL0運(yùn)行應(yīng)用程序,EL1運(yùn)行操作系統(tǒng)內(nèi)核,EL2運(yùn)行虛擬機(jī)監(jiān)視器,EL3運(yùn)行Monitor.TrustZone將每個(gè)物理處理器核虛擬化為兩個(gè)核,分別用于安全世界和普通世界.安全配置寄存器(Secure Configuration Register,SCR)的NS位的值指明處理器當(dāng)前所處執(zhí)行環(huán)境:0表明處理器運(yùn)行在安全世界,1表明處理器運(yùn)行在普通世界.兩個(gè)世界通過Monitor執(zhí)行世界切換,并在安全內(nèi)存中保存兩個(gè)世界的上下文.內(nèi)存隔離和外設(shè)隔離是TrustZone隔離機(jī)制的核心.安全世界可以訪問所有的內(nèi)存區(qū)域及設(shè)備,TrustZone限制普通世界訪問安全世界的內(nèi)存區(qū)域及設(shè)備.

圖1 ARM TrustZone的中斷處理架構(gòu)Fig.1 Interrupt handling architecture of ARM TrustZone

中斷隔離是確保外設(shè)隔離的關(guān)鍵機(jī)制.如圖1所示,為了實(shí)現(xiàn)中斷隔離,基于TrustZone的處理器有3張異常向量表,分別用于普通世界的EL1、安全世界的EL1和Monitor模式.每張表有16個(gè)條目,這16個(gè)條目分為四類異常,分別為IRQ(Interrupt Request),FIQ(Fast Interrupt Request),SError,Synchronous,通過條目可以找到中斷對應(yīng)的處理程序.當(dāng)中斷的安全類型和處理器當(dāng)前所處執(zhí)行環(huán)境一致時(shí)(即安全中斷發(fā)生時(shí)處理器運(yùn)行在安全世界,非安全中斷發(fā)生時(shí)處理器運(yùn)行在普通世界),可以直接在當(dāng)前世界處理,否則Monitor執(zhí)行世界切換,使中斷在另一個(gè)世界被處理.

TZASC用于對內(nèi)存實(shí)施訪問控制.TrustZone使用TZASC可以把物理內(nèi)存劃分為多個(gè)區(qū)域,安全軟件配置TZASC,可以將劃分的內(nèi)存區(qū)域配置為安全內(nèi)存區(qū)域或者非安全內(nèi)存區(qū)域,并且拒絕非安全事務(wù)訪問安全內(nèi)存區(qū)域.

GIC用于管理中斷源,是連接外設(shè)中斷和CPU的重要組件,包含了分發(fā)器、再分發(fā)器和CPU接口.GIC接受外設(shè)發(fā)出的中斷后,由分發(fā)器和再分發(fā)器將不同的外部中斷分組為Group0和Group1,其中Group0為安全中斷,優(yōu)先級最高,CPU接口只發(fā)送FIQ信號給CPU.Group1又分為安全Group1和非安全Group1.對于分組為Group1的中斷,當(dāng)中斷安全類型和CPU所處執(zhí)行環(huán)境一致時(shí),CPU接口發(fā)送IRQ信號給CPU;否則,CPU接口發(fā)送FIQ信號給CPU.GIC和TrustZone的安全機(jī)制結(jié)合使用,可以使安全中斷源發(fā)出的中斷不能被普通世界軟件處理.

本文根據(jù)ARM可信固件(ARM Trusted Firmware,ATF)[13]的中斷管理框架建立中斷隔離機(jī)制的形式化模型.ATF是ARMv8架構(gòu)的開源底層固件,提供了安全世界軟件的參考實(shí)現(xiàn),統(tǒng)一了各種ARM接口標(biāo)準(zhǔn),如電源狀態(tài)協(xié)調(diào)接口(Power State Coordination Interface,PSCI)、可信板啟動(dòng)要求(Trusted Board Boot Requirements,TBBR)、SMC調(diào)用約定(Secure Monitor Call Calling Covention,SMCCC)等.在此簡介ATF的中斷配置和中斷處理流程.SCR寄存器的F位的值和I位的值分別表示FIQ中斷和IRQ中斷的路由級別:F位的值或I位的值為1時(shí),表示相應(yīng)的中斷路由至EL3,由Monitor處理;值為0時(shí),表示相應(yīng)的中斷路由至當(dāng)前世界的EL1,由當(dāng)前世界的OS處理.

本文模型采用常用的配置方式,即SCR寄存器的F位的值和I位的值分別為1和0.其他配置的驗(yàn)證方法與之類似,由于篇幅的限制,在此不展開敘述.如圖1所示,由外設(shè)發(fā)出電信號觸發(fā)中斷后,先由GIC處理,發(fā)送FIQ信號或IRQ信號,處理器自動(dòng)將PSTATE保存在程序狀態(tài)寄存器(Saved Program Status Register,SPSR)中,將程序計(jì)數(shù)器(Program Counter,PC)保存在異常鏈接寄存器(Exception Link Register,ELR)中,然后調(diào)用中斷處理程序.當(dāng)需要切換到另一個(gè)世界處理中斷時(shí),切換過程為將當(dāng)前世界上下文保存在安全內(nèi)存中,從安全內(nèi)存中恢復(fù)將要切換的世界的上下文.其中,要保存和恢復(fù)的上下文包括系統(tǒng)寄存器、通用寄存器和狀態(tài)寄存器,在圖1中分別用sys_regs、gp_regs和el3state表示.在另一個(gè)世界調(diào)用中斷處理程序處理完中斷后,執(zhí)行世界切換回到原來的世界,從SPSR中恢復(fù)處理器狀態(tài),從ELR中恢復(fù)PC.

3 TrustZone中斷隔離機(jī)制的形式化模型

本文依據(jù)ARMv8規(guī)范和ATF建立TrustZone中斷隔離機(jī)制的形式化模型,該模型為狀態(tài)遷移系統(tǒng),包括執(zhí)行模型和事件規(guī)約兩部分:執(zhí)行模型中主要包含系統(tǒng)的狀態(tài),狀態(tài)包括與中斷處理相關(guān)的寄存器和內(nèi)存;事件規(guī)約中建模軟硬件的行為,包括中斷處理事件和內(nèi)存讀寫事件.此外,為了便于驗(yàn)證模型的信息流安全性,引入了域和觀察等價(jià)的概念.本節(jié)主要介紹中斷處理模型、軟硬件組件的形式化定義、事件規(guī)約和安全模型.

3.1 中斷處理模型

本文中斷處理模型MI由一個(gè)四元組(S,E,s0,step)組成,包含系統(tǒng)狀態(tài),事件集合,初始狀態(tài)和遷移函數(shù).

系統(tǒng)狀態(tài)S=,其中regs表示ARM寄存器,包括通用寄存器、系統(tǒng)寄存器以及處理器狀態(tài)寄存器.mem:(D×64word)→W,表示域與64位物理地址到內(nèi)存值的映射.

如圖2所示,本文保存上下文的內(nèi)存區(qū)域有兩類:世界切換時(shí)保存上下文的內(nèi)存區(qū)域和當(dāng)前世界操作系統(tǒng)保存應(yīng)用層上下文的內(nèi)存區(qū)域,即基地址值base1至base3之間的內(nèi)存區(qū)域保存世界切換時(shí)的上下文,基地址值base3至base4之間以及基地址值base5至base6之間的內(nèi)存區(qū)域保存當(dāng)前世界應(yīng)用層的上下文.執(zhí)行世界切換從安全內(nèi)存中恢復(fù)普通世界上下文時(shí)會(huì)導(dǎo)致TEE中信息流向REE.為了準(zhǔn)確地建模包含世界切換的信息流策略,并限制TEE中非保存兩個(gè)世界上下文的內(nèi)存區(qū)域的信息直接流向REE,本文抽象定義了MON、TEE、REE 3個(gè)安全域.安全內(nèi)存劃分為3部分,分別屬于安全域MON和安全域TEE:MON域包含安全內(nèi)存中保存世界切換時(shí)的上下文的內(nèi)存區(qū)域,其它安全內(nèi)存劃分為兩部分,均屬于安全域TEE,即保存安全世界應(yīng)用層的上下文以及非保存上下文的內(nèi)存區(qū)域.非安全內(nèi)存屬于安全域REE,劃分為兩部分,即非安全內(nèi)存中保存普通世界應(yīng)用層的上下文以及非保存上下文的內(nèi)存區(qū)域.本文模型配置基地址值(base1,base2,base3,base4,base5,base6)=(0x0000,0x0200,0x0300,0x0400,0x0000,0x0100).

圖2 內(nèi)存分布Fig.2 Distribution of memory

事件集合E={handle_FIQ,handle_IRQ,mem_read,mem_write},分別表示FIQ處理程序、IRQ處理程序、內(nèi)存讀和內(nèi)存寫.

系統(tǒng)初始狀態(tài)s0∈S.在初始狀態(tài)時(shí),寄存器和內(nèi)存的值均設(shè)置為0x0000.

狀態(tài)遷移函數(shù)step:S×E→S,表示狀態(tài)與事件到后繼狀態(tài)的映射.

為了表示從狀態(tài)s執(zhí)行事件序列產(chǎn)生的狀態(tài),在step的基礎(chǔ)上歸納定義函數(shù)run:S×E*→S,具體定義為:

其中,Λ表示空序列,a#as表示在事件序列as前面加上事件a.

本文定義謂詞R用于表示狀態(tài)s是否可達(dá),即是否存在事件序列as,使得從初始狀態(tài)s0開始執(zhí)行as所產(chǎn)生的狀態(tài)為s.

定義1.狀態(tài)可達(dá)

3.2 軟硬件組件的形式化定義

本小節(jié)主要闡述關(guān)鍵軟硬組件的功能在模型中的形式化描述方式,包括TZASC、GIC、Monitor和異常向量表.

TZASC主要用于把內(nèi)存劃分為安全區(qū)域或者是非安全區(qū)域,并且配置每個(gè)內(nèi)存區(qū)域的訪問權(quán)限,拒絕非安全事務(wù)訪問安全內(nèi)存區(qū)域.本文模型將TZASC對內(nèi)存的訪問控制功能建模為函數(shù)tzasc_right,具體定義為:

其中,函數(shù)cworld返回處理器當(dāng)前所處執(zhí)行環(huán)境,addr_dom返回地址pa的域.函數(shù)tzasc_right表示TZASC對內(nèi)存訪問實(shí)施的控制,當(dāng)處理器當(dāng)前所處執(zhí)行環(huán)境為普通世界,地址pa位于安全內(nèi)存區(qū)域時(shí),不可以訪問;否則,可以訪問.

GIC主要用于對中斷進(jìn)行分組,并且向CPU發(fā)送中斷信號.本文模型將分發(fā)器和再分發(fā)器的功能建模為函數(shù)GIC_Group,將CPU接口的功能建模為函數(shù)ipt_type.函數(shù)GIC_Group的具體定義為:

其中,n表示任意待處理中斷的中斷號.G1S、G1NS、G0分別表示分組為安全Group1、非安全Group1、Group0的中斷.

函數(shù)ipt_type的具體定義為:

該函數(shù)根據(jù)中斷號的安全類型和處理器當(dāng)前所處執(zhí)行環(huán)境,相應(yīng)地發(fā)送FIQ或者IRQ信號,在上述函數(shù)定義中分別表示為fiq和irq.

Monitor主要用于世界切換.本文模型參考ATF建模世界切換的處理過程,將Monitor的世界切換功能建模為函數(shù)world_switch,具體定義為:

其中,函數(shù)save_context用于將當(dāng)前世界上下文保存在安全內(nèi)存中,函數(shù)restore_context用于從安全內(nèi)存中恢復(fù)將要切換的世界的上下文,并且在此過程中修改SCR寄存器的NS位值.本文模型將要保存的寄存器的偏移量設(shè)置為固定值,通過基地址值加偏移量將寄存器保存在內(nèi)存的不同位置.

異常向量表用于查找中斷處理程序.本文模型主要處理FIQ和IRQ,因此對3張異常向量表中用于處理FIQ和IRQ的條目進(jìn)行抽象建模,將查找相應(yīng)的異常向量表?xiàng)l目建模為查表函數(shù)look_up,具體定義為:

letg=GIC_Group(n)in

caseipt_type(s,n)offiq?monitor_fiq|

irq?(ifg=G1Sthentee_irqelseree_irq)|

error?Error

中斷號映射為fiq,則返回結(jié)果monitor_fiq,表示Monitor的異常向量表中FIQ對應(yīng)的異常向量表?xiàng)l目;中斷號映射為安全Group1的irq,則返回結(jié)果tee_irq,表示TEE EL1的異常向量表中IRQ對應(yīng)的異常向量表?xiàng)l目;中斷號映射為非安全Group1的irq,則返回結(jié)果ree_irq,表示REE EL1的異常向量表中IRQ對應(yīng)的異常向量表?xiàng)l目.

3.3 事件規(guī)約

本小節(jié)介紹模型中事件的形式化定義.因?yàn)樵谥袛嗵幚淼倪^程中涉及對上下文的保存和恢復(fù),所以為了建立完整的TrustZone中斷隔離機(jī)制的形式化模型,建模的事件包括FIQ和IRQ的中斷處理程序以及主要內(nèi)存操作事件.

1)FIQ中斷處理程序

當(dāng)在當(dāng)前狀態(tài)s下,處理器根據(jù)中斷號n在異常向量表中查找處理該中斷的相應(yīng)條目為monitor_fiq,該中斷的安全類型為G0、G1S或者G1NS時(shí),執(zhí)行FIQ的中斷處理操作得到新狀態(tài)并返回True,否則當(dāng)前狀態(tài)不變并返回False.

定義2.FIQ中斷處理程序

if(look_up(s,n)=monitor_fiq∧GIC_Group(n)=G0)

then(EL3_handle(s),True)

elseif(look_up(s,n)=monitor_fiq∧GIC_Group(n)≠G0)

then(world_switch(s),True)

else(s,False)

函數(shù)EL3_handle返回處理Group0中斷得到的新狀態(tài)s′:當(dāng)處理器當(dāng)前所處執(zhí)行環(huán)境為安全世界時(shí),s′為保存安全世界的SPSR和ELR寄存器后產(chǎn)生的新狀態(tài);當(dāng)處理器當(dāng)前所處執(zhí)行環(huán)境為普通世界時(shí),s′為保存普通世界上下文,恢復(fù)安全世界上下文產(chǎn)生的新狀態(tài).

2)IRQ中斷處理程序

與處理FIQ類似,在當(dāng)前狀態(tài)s下處理IRQ時(shí),處理器根據(jù)中斷號n在異常向量表中查找處理IRQ的條目為tee_irq或者ree_irq時(shí),執(zhí)行IRQ的中斷處理操作得到新狀態(tài)并返回True,否則當(dāng)前狀態(tài)不變并返回False.

定義3.IRQ中斷處理程序

iflook_up(s,n)=tee_irq

then(TEE_EL1_handle(s),True)

elseiflook_up(s,n)=ree_irq

then(REE_EL1_handle(s),True)

else(s,False)

函數(shù)TEE_EL1_handle返回由TEE OS處理IRQ得到的新狀態(tài),該狀態(tài)為保存安全世界的SPSR和ELR寄存器后產(chǎn)生的狀態(tài).函數(shù)REE_EL1_handle返回由REE OS處理IRQ得到的新狀態(tài),該狀態(tài)為保存普通世界的SPSR和ELR寄存器后產(chǎn)生的新狀態(tài).

3)內(nèi)存讀

當(dāng)在當(dāng)前狀態(tài)s下,處理器可以訪問物理地址pa,內(nèi)存訪問權(quán)限為可讀可寫rw或只讀ro,pa不是保存上下文的內(nèi)存區(qū)域時(shí),執(zhí)行內(nèi)存讀操作得到新狀態(tài)并返回True和內(nèi)存值;否則,禁止該操作,當(dāng)前狀態(tài)不變并返回False和None.

定義4.內(nèi)存讀操作

letm=mem(s)in

if(tzasc_right(s,pa)∨save(s,pa))

then(s,False,None)

else(caseacofno?(s,False,None)

| _?(s,True,Some(the(m(addr_dom(pa),

addr_val(pa))))))

其中,訪問權(quán)限ac=(rw,ro,no),rw表示可讀可寫,ro表示只讀,no表示沒有訪問權(quán)限.函數(shù)save判斷pa是否為保存上下文的內(nèi)存區(qū)域.函數(shù)addr_val返回物理地址中64位地址值.

4)內(nèi)存寫

TrustZone的訪問控制模型允許安全世界寫非安全內(nèi)存,因此TEE向REE有直接信息流,然而這會(huì)導(dǎo)致TEE向REE泄露敏感信息,不適用于對安全性要求較高的應(yīng)用場景.為了驗(yàn)證在安全性要求較高的應(yīng)用場景中TrustZone中斷隔離機(jī)制的信息流安全性,本文限制了安全世界對非安全內(nèi)存的寫操作,在這種情況下驗(yàn)證中斷處理過程中是否存在TEE到REE的隱蔽信息流.

當(dāng)在當(dāng)前狀態(tài)s下,處理器可以訪問物理地址pa,處理器的執(zhí)行環(huán)境為安全世界時(shí)pa不位于非安全內(nèi)存區(qū)域,內(nèi)存訪問權(quán)限為可讀可寫rw,pa不是保存上下文的內(nèi)存區(qū)域時(shí),執(zhí)行內(nèi)存寫操作,即在當(dāng)前狀態(tài)下將值v寫入內(nèi)存得到新狀態(tài)并返回True;否則禁止該操作,當(dāng)前狀態(tài)不變并返回False.

定義5.內(nèi)存寫操作

letm=mem(s)in

if((cworld(s)=TEE)∧(addr_dom(pa)=REE))

then(s,False)

elseif(┐tzasc_right(s,pa)∨(ac≠rw)∨save(s,pa))

then(s,False)

else(s(|mem:=

m((addr_dom(pa),addr_val(pa)):=Somev)|),True)

3.4 安全模型

如前文所述,本文模型根據(jù)事件執(zhí)行的不同安全權(quán)限將安全域定義為TEE,REE和MON,其中TEE表示安全世界域,REE表示普通世界域,MON表示如圖2所示的保存兩個(gè)世界上下文的域.D是模型中安全域的集合,定義為D={REE,TEE,MON}.

函數(shù)edom是狀態(tài)和事件到安全域的映射,表示在當(dāng)前狀態(tài)下事件的執(zhí)行域.例如:edom(s,FIQ(n))=MON,表示執(zhí)行FIQ中斷處理事件的安全域是MON.edom(s,IRQ(n))=cworld(s),表示執(zhí)行IRQ中斷處理事件的安全域是動(dòng)態(tài)的,取決于處理器當(dāng)前所處執(zhí)行環(huán)境.

～表示等價(jià)關(guān)系,包括狀態(tài)等價(jià)和觀察等價(jià),其形式化定義如下:

1)狀態(tài)等價(jià)

狀態(tài)s和t等價(jià)即s～d～t,表示在狀態(tài)s和t下安全域d可觀察的狀態(tài)相同.由于不同的安全域d可觀察到的狀態(tài)不同,本文模型基于d可觀察到的狀態(tài)定義狀態(tài)等價(jià).

定義6.狀態(tài)s和t關(guān)于安全域d=TEE狀態(tài)等價(jià)

∧cworld(s)=cworld(t)∧(cworld(s)=TEE→reg(s)=reg(t))

上述定義的含義為:若狀態(tài)s和t下安全內(nèi)存的值相等,處理器當(dāng)前所處執(zhí)行環(huán)境相同,并且如果狀態(tài)s下處理器當(dāng)前所處執(zhí)行環(huán)境為安全世界,那么s和t下的寄存器的值相等,則稱s和t關(guān)于安全域TEE狀態(tài)等價(jià).

定義7.狀態(tài)s和t關(guān)于安全域d=REE狀態(tài)等價(jià)

∧cworld(s)=cworld(t)∧(cworld(s)=REE→reg(s)=reg(t))

上述定義的含義為:若狀態(tài)s和t下非安全內(nèi)存的值相等,處理器當(dāng)前所處執(zhí)行環(huán)境相同,并且如果狀態(tài)s下處理器當(dāng)前所處執(zhí)行環(huán)境為普通世界,那么s和t下的寄存器的值相等,則稱s和t關(guān)于安全域REE狀態(tài)等價(jià).

定義8.狀態(tài)s和t關(guān)于安全域d=MON狀態(tài)等價(jià)

∧cworld(s)=cworld(t)∧reg(s)=reg(t)

上述定義的含義為:若狀態(tài)s和t下保存兩個(gè)世界上下文的安全內(nèi)存的值相等、處理器當(dāng)前所處執(zhí)行環(huán)境相同,并且寄存器的值相等,則稱s和t關(guān)于安全域MON狀態(tài)等價(jià).

2)觀察等價(jià)

4 安全屬性的定義

本文模型采用一階邏輯公式定義中斷處理功能正確性和信息流安全性.中斷處理功能正確性是保證中斷隔離正確實(shí)現(xiàn)的基礎(chǔ),表示中斷被正確地處理.信息流安全性則表示在系統(tǒng)運(yùn)行的過程中不存在違反安全策略的隱蔽信息流通道.

4.1 正確性

中斷處理功能正確性是確保中斷被正確處理的安全屬性.在TrustZone中,安全中斷被配置為由安全世界處理,非安全中斷被配置為由普通世界處理,當(dāng)系統(tǒng)違反該配置運(yùn)行時(shí),安全中斷可能會(huì)被普通世界處理,從而導(dǎo)致安全世界外設(shè)存在安全隱患.因此,為了驗(yàn)證中斷處理功能正確性,本文對正確性屬性進(jìn)行定義.

1)處理FIQ中斷的正確性

定理1.處理安全類型為Group0的FIQ中斷時(shí),系統(tǒng)運(yùn)行在安全世界

?ss′n.R(s)∧GIC_Group(n)=G0

∧snd(handle_FIQ(s,n))∧s′=fst(handle_FIQ(s,n))

→cworld(s′)=TEE

其中,fst和snd分別用于提取有序?qū)Φ牡?個(gè)分量和第2個(gè)分量.上述定理的含義為:若狀態(tài)s可達(dá),發(fā)生Group0中斷,執(zhí)行FIQ中斷處理事件,得到新狀態(tài)s′,則新狀態(tài)s′下處理器所處執(zhí)行環(huán)境為安全世界,即在安全世界處理該中斷.

定理2.處理安全類型為Group1的FIQ中斷時(shí),系統(tǒng)進(jìn)行世界切換

?ss′n.R(s)∧GIC_Group(n)≠G0∧snd(handle_FIQ(s,n))

∧s′=fst(handle_FIQ(s,n))→cworld(s)≠cworld(s′)

上述定理的含義為:若狀態(tài)s可達(dá),發(fā)生Group1中斷,執(zhí)行FIQ中斷處理事件,得到新狀態(tài)s′,則狀態(tài)s′和s下處理器所處執(zhí)行環(huán)境不同,即系統(tǒng)處理該中斷時(shí)進(jìn)行了世界切換.

2)處理IRQ中斷的正確性

定理3.IRQ中斷在當(dāng)前世界處理

?ss′n.R(s)∧GIC_Group(n)≠G0

∧snd(handle_IRQ(s,n))∧s′=fst(handle_IRQ(s,n))

→cworld(s)=cworld(s′)

上述定理的含義為:若狀態(tài)s可達(dá),發(fā)生Group1中斷,執(zhí)行IRQ處理事件,得到新狀態(tài)s′,則狀態(tài)s′和s下處理器所處執(zhí)行環(huán)境相同,即在當(dāng)前世界處理該中斷.

4.2 信息流安全屬性

本文定義的信息流安全屬性包括無干擾[14]、無泄露[15]和無影響[15].定義基于狀態(tài)事件的信息流安全性的方法主要有信息流無干擾屬性和GWV策略[16],本文模型采用無干擾屬性的定義方法.無干擾屬性表示系統(tǒng)運(yùn)行的過程中,安全域不會(huì)被安全策略不允許向其有信息流的其它域干擾.無泄露屬性表示機(jī)密數(shù)據(jù)不會(huì)流向安全策略不允許流向的其它域.無影響屬性是無干擾屬性和無泄露屬性的結(jié)合.信息流安全屬性的定義通常采用輔助函數(shù)sources[14]和ipurge[14].

函數(shù)sources能夠表示非傳遞策略所允許的信息流.對于事件序列as和安全域d,sources描述了執(zhí)行事件序列as時(shí)允許向安全域d有信息流的域集合.

定義9.函數(shù)sources

sources(Λ,s,d)=j5i0abt0b

sources(a#as,s,d)=

函數(shù)ipurge用于清除向安全域沒有信息流的事件.ipurge(as,s,d)表示對于事件序列as和安全域d,函數(shù)ipurge清除從狀態(tài)s執(zhí)行as時(shí)不允許直接或間接向安全域d有信息流的事件.

定義10.函數(shù)ipurge

ipurge(Λ,s,d)=Λ

ipurge(a#as,s,d)=

無干擾屬性的本質(zhì)是指系統(tǒng)執(zhí)行事件序列的過程中,安全策略中向安全域沒有信息流的域不會(huì)影響該安全域可觀察到的狀態(tài).

定義11.無干擾屬性

上述定義的含義是:從初始狀態(tài)s0執(zhí)行事件序列as得到的最終狀態(tài)與執(zhí)行as經(jīng)過清除操作后的事件序列得到的最終狀態(tài)關(guān)于安全域d觀察等價(jià).

無泄露屬性的本質(zhì)是指初始狀態(tài)時(shí)沒有泄露機(jī)密數(shù)據(jù),那么執(zhí)行后續(xù)事件時(shí)機(jī)密數(shù)據(jù)也不會(huì)被泄露.無泄露屬性是無干擾屬性的補(bǔ)充,可以表達(dá)安全世界的敏感信息不會(huì)泄露到普通世界.

定義12.無泄露屬性

上述定義的含義是:若狀態(tài)s和t可達(dá),并且s和t關(guān)于允許向安全域d有信息流的所有域等價(jià),則從s和t執(zhí)行事件序列as后得到的狀態(tài)關(guān)于安全域d觀察等價(jià).

無影響是無干擾和無泄露的結(jié)合,包含這兩個(gè)安全屬性的特點(diǎn),確保了秘密事件不被觀察到,機(jī)密數(shù)據(jù)不被泄露.

定義13.無影響屬性

∧(s≈sources(as,s,d)≈t)

→(s?as?t?ipurge(as,t,d)@d)

上述定義的含義為:若狀態(tài)s和t可達(dá),并且s和t關(guān)于允許向安全域d有信息流的所有域等價(jià),則從s執(zhí)行事件序列as與從t執(zhí)行as經(jīng)過清除操作后的事件序列得到的最終狀態(tài)關(guān)于安全域d觀察等價(jià).

5 安全屬性的形式化驗(yàn)證

本節(jié)概述安全屬性的形式化驗(yàn)證,包括正確性證明、信息流安全性證明和驗(yàn)證結(jié)論.

5.1 正確性證明

本文在Isabelle/HOL中通過大約90個(gè)引理直接證明了中斷處理功能正確性.結(jié)果表明,安全中斷在安全世界被處理,非安全中斷在普通世界被處理,即中斷在相應(yīng)的世界被正確地處理,為后續(xù)證明信息流安全性奠定了基礎(chǔ).

5.2 信息流安全性證明

信息流安全性利用展開定理[14]證明,通過證明模型中每個(gè)事件滿足展開條件weak_step_consistent和local_respect,可以證明模型滿足信息流安全性.展開條件的定義和展開定理如下:

定義14.weak_step_consistent條件

上述定義的含義為:若任意兩個(gè)可達(dá)狀態(tài)s和t關(guān)于安全域d和事件a的事件域等價(jià),并且安全策略允許事件a的事件域向安全域d有信息流,則狀態(tài)s和t執(zhí)行事件a后的狀態(tài)仍然關(guān)于安全域d等價(jià).

定義15.local_respect條件

∧s′=step(s,a)→(s～d～s′)

上述定義的含義為:若任意狀態(tài)s可達(dá),安全策略不允許事件a的事件域向安全域d有信息流,狀態(tài)s下執(zhí)行事件a后得到新狀態(tài)s′,則狀態(tài)s和新狀態(tài)s′關(guān)于安全域d等價(jià).

定理4.展開定理

(weak_step_consistent∧local_respect)?noninfluence

上述定理的含義為:若展開條件weak_step_consistent和local_respect成立,則無影響屬性成立.

本文信息流安全屬性推導(dǎo)關(guān)系如圖4所示.首先定義每個(gè)事件的展開條件weak_step_consistent和local_respect,驗(yàn)證所有事件的兩個(gè)展開條件weak_step_consistent和local_respect成立,然后通過定理4證明模型滿足無影響屬性,最終通過無影響屬性推導(dǎo)證明模型滿足無干擾屬性和無泄露屬性.本文模型定義了每個(gè)事件的展開條件,例如,FIQ中斷處理事件的展開條件如下:

圖4 信息流安全屬性推導(dǎo)關(guān)系Fig.4 Inference relations of information flow security properties

定理5.FIQ中斷處理事件滿足weak_step_consistent

上述定理的含義為:若任意可達(dá)狀態(tài)s和t關(guān)于安全域d和處理FIQ的事件域等價(jià),安全策略允許處理FIQ的事件域向安全域d有信息流,則狀態(tài)s和狀態(tài)t下分別執(zhí)行FIQ中斷處理事件得到的下一個(gè)狀態(tài)s′和t′關(guān)于安全域d等價(jià).

定理6.FIQ中斷處理事件滿足local_respect

上述定理的含義為:若狀態(tài)s可達(dá),安全策略不允許處理FIQ的事件域向安全域d有信息流,狀態(tài)s下執(zhí)行FIQ中斷處理事件得到下一個(gè)狀態(tài)s′,則s和s′關(guān)于安全域d等價(jià).

5.3 驗(yàn)證結(jié)論

本文在Isabelle/HOL中建立TrustZone中斷隔離機(jī)制的形式化模型,并對模型的正確性和信息流安全性進(jìn)行了驗(yàn)證,建模和驗(yàn)證代碼總計(jì)大約2830行,模型代碼大約200行,安全屬性代碼大約30行,安全屬性的驗(yàn)證代碼大約2600行.

本文在Isabelle/HOL中驗(yàn)證了模型滿足正確性和信息流安全性,驗(yàn)證結(jié)果表明安全中斷在安全世界處理,非安全中斷在普通世界處理,中斷處理的過程中不存在違反安全策略的信息流,保證了安全世界敏感數(shù)據(jù)的安全性,并且普通世界不會(huì)干擾安全世界的運(yùn)行.

6 相關(guān)工作

本節(jié)概述本文的相關(guān)工作,包括ARM處理器形式化驗(yàn)證、TEE形式化驗(yàn)證、信息流安全形式化驗(yàn)證.

6.1 ARM處理器形式化驗(yàn)證

瑞典皇家理工學(xué)院使用包含內(nèi)存管理單元(Memory Management Unit,MMU)的ARMv7 ISA(Instruction Set Architecture)模型,驗(yàn)證了虛擬化平臺的內(nèi)存隔離和信息流安全性[17].哥倫比亞大學(xué)使用放松內(nèi)存驗(yàn)證(Verification on Relaxed Memory,VRM)框架驗(yàn)證了ARM上運(yùn)行的改進(jìn)的Linux KVM虛擬機(jī)監(jiān)視器的安全屬性[18].新南威爾士大學(xué)抽象了ARMv7架構(gòu)MMU,并驗(yàn)證了轉(zhuǎn)換后備緩沖區(qū)(Translation Lookaside Buffer,TLB)的正確性[19].

6.2 TEE形式化驗(yàn)證

首都師范大學(xué)驗(yàn)證了基于TrustZone技術(shù)的TEE內(nèi)存管理的正確性以及內(nèi)存隔離機(jī)制的信息流安全性[20].俄亥俄州立大學(xué)驗(yàn)證了SGX飛地程序關(guān)于單調(diào)計(jì)數(shù)器、全局變量和封裝數(shù)據(jù)的狀態(tài)連續(xù)性,并將該技術(shù)應(yīng)用于3個(gè)SGX開源應(yīng)用程序的驗(yàn)證[21].加州大學(xué)伯克利分校驗(yàn)證了可信抽象平臺(Trusted Abstract Platform,TAP)的安全遠(yuǎn)程執(zhí)行的完整性、機(jī)密性和安全度量,并證明了改進(jìn)后的SGX和Sanctum實(shí)現(xiàn)了安全的飛地[22].

6.3 信息流安全形式化驗(yàn)證

電子科技大學(xué)基于ARM TrustZone技術(shù),設(shè)計(jì)了TEE多層架構(gòu)以及安全通信通道,提出了該架構(gòu)的形式化模型,并驗(yàn)證了模型的信息流無干擾屬性[23].北京航空航天大學(xué)驗(yàn)證了遵循ARINC 653信道通信標(biāo)準(zhǔn)的隔離內(nèi)核的信息流安全性[24].南洋理工大學(xué)驗(yàn)證了SPARCv8 ISA的整數(shù)單元(Integer Unit)的無干擾屬性[25].

7 結(jié) 論

本文提出了TrustZone中斷隔離機(jī)制的形式化模型,充分考慮了中斷處理過程中涉及到的細(xì)節(jié),包含了發(fā)生中斷時(shí)軟硬件的處理過程,并在Isabelle/HOL中對模型的正確性和信息流安全性進(jìn)行驗(yàn)證.驗(yàn)證結(jié)果表明安全中斷不會(huì)被普通世界處理,在中斷處理的過程中不存在隱蔽的信息流通道.未來工作是在現(xiàn)有模型的基礎(chǔ)上,進(jìn)一步完善,對缺頁中斷等具體中斷處理過程進(jìn)行驗(yàn)證,從而為基于TrustZone架構(gòu)的可信執(zhí)行環(huán)境的中斷隔離機(jī)制提供更全面的驗(yàn)證.