祝現(xiàn)威 朱智強(qiáng) 孫 磊

(信息工程大學(xué)密碼工程學(xué)院 河南 鄭州 450001)

XSM語(yǔ)義模型及安全需求形式化驗(yàn)證

祝現(xiàn)威 朱智強(qiáng) 孫 磊

(信息工程大學(xué)密碼工程學(xué)院 河南 鄭州 450001)

Xen作為一種開(kāi)源流行的虛擬化工具，使用越來(lái)越頻繁。作為Xen的安全框架XSM(Xen Security Module)也受到廣泛的關(guān)注。許多研究者通過(guò)形式化的方式對(duì)現(xiàn)有的操作系統(tǒng)進(jìn)行正確性的驗(yàn)證，目前已有的形式化研究主要是驗(yàn)證系統(tǒng)實(shí)現(xiàn)的代碼正確性。從系統(tǒng)功能角度提出了一種以主體行為為操作系統(tǒng)語(yǔ)義模型對(duì)系統(tǒng)進(jìn)行形式化建模，并采用CTL時(shí)序邏輯對(duì)XSM安全需求進(jìn)行分析。語(yǔ)義模型作為系統(tǒng)設(shè)計(jì)合理性和形式化驗(yàn)證的聯(lián)系，對(duì)XSM進(jìn)行形式化驗(yàn)證，并使用Isabelle/HOL驗(yàn)證功能和安全需求的一致性，以說(shuō)明XSM是否符合安全需求。

XSM 語(yǔ)義模型 形式化驗(yàn)證 安全性分析 Isabelle/HOL

0 引 言

云計(jì)算作為一種新型的計(jì)算模式，迅速成為計(jì)算機(jī)技術(shù)發(fā)展的熱點(diǎn)。然而近年來(lái)，隨著云計(jì)算的廣泛應(yīng)用，云安全問(wèn)題越來(lái)越被學(xué)術(shù)界和工業(yè)界所關(guān)注。在眾多的云安全問(wèn)題中，作為云計(jì)算基礎(chǔ)支撐的虛擬化平臺(tái)的安全問(wèn)題是基礎(chǔ)。

Xen是劍橋大學(xué)開(kāi)發(fā)的一個(gè)開(kāi)源的虛擬化平臺(tái)，在現(xiàn)有云計(jì)算環(huán)境中得到廣泛應(yīng)用，為了增強(qiáng)其安全性，一些研究學(xué)者借鑒安全操作系統(tǒng)的理論和技術(shù)提出了針對(duì)Xen虛擬化平臺(tái)的安全框架XSM。

XSM位于硬件和應(yīng)用軟件的中間層，一方面為Xen虛擬化平臺(tái)的安全性提供保證；另一方面還必須保證其自身的可靠性和安全性。然而，過(guò)去雖然研究人員對(duì)XSM開(kāi)展了很多研究并進(jìn)行了實(shí)現(xiàn)，但是XSM的安全性缺乏形式化方法的分析和驗(yàn)證。眾所周知，形式化方法的安全分析與驗(yàn)證是構(gòu)造高安全操作系統(tǒng)不可缺少的，同樣，本文認(rèn)為對(duì)XSM進(jìn)行形式化驗(yàn)證將為構(gòu)造高安全虛擬化平臺(tái)提供理論支撐和技術(shù)保障。

在安全系統(tǒng)領(lǐng)域，國(guó)內(nèi)外研究學(xué)者對(duì)形式化驗(yàn)證方法進(jìn)行了大量研究，典型研究工作有：澳大利亞的NICTA實(shí)驗(yàn)室完成了sel4安全操作系統(tǒng)的設(shè)計(jì)和實(shí)現(xiàn)[1,3]，該實(shí)驗(yàn)通過(guò)Haskell來(lái)搭建系統(tǒng)原型，從系統(tǒng)訪(fǎng)問(wèn)控制模型到系統(tǒng)代碼進(jìn)行了一系列的形式化證明。通過(guò)證明各抽象層的一致性來(lái)證明系統(tǒng)的正確性。耶魯大學(xué)Flint小組通過(guò)自主開(kāi)發(fā)的VeriML和λHOL邏輯系統(tǒng)設(shè)計(jì)來(lái)實(shí)現(xiàn)不同模塊的同一形式化驗(yàn)證。美國(guó)海軍學(xué)院使用Z語(yǔ)言對(duì)XENON[4-5](修改后的XSM)的功能一致性進(jìn)行了形式化的驗(yàn)證。國(guó)內(nèi)劉暢等[15]通過(guò)SPIN方法對(duì)安全框架進(jìn)行驗(yàn)證。屈延文[8]提出了通過(guò)運(yùn)營(yíng)，系統(tǒng)，技術(shù)三視圖來(lái)研究操作系統(tǒng)構(gòu)造方法并通過(guò)行為學(xué)理論對(duì)計(jì)算機(jī)系統(tǒng)進(jìn)行結(jié)構(gòu)劃分。周宇等[14]通過(guò)層次時(shí)間自動(dòng)機(jī)利用時(shí)間序列來(lái)描述系統(tǒng)狀態(tài)。

在安全虛擬化平臺(tái)領(lǐng)域，形式化安全驗(yàn)證方面的研究還處于起步階段，其對(duì)虛擬化平臺(tái)的驗(yàn)證還是對(duì)已有的代碼進(jìn)行形式化證明，主要是驗(yàn)證代碼的正確性。本文認(rèn)為除了代碼驗(yàn)證外還要對(duì)平臺(tái)功能進(jìn)行形式化描述，提出其安全需求。并對(duì)形式化模型和安全需求的一致性進(jìn)行形式化驗(yàn)證。但是上述形式化大多使用有限狀態(tài)機(jī)模型進(jìn)行建模，由于需要狀態(tài)的窮舉容易產(chǎn)生狀態(tài)膨脹，使其表現(xiàn)力不夠豐富或者建模建立復(fù)雜不易使用。本文提出了一種以主體動(dòng)作為描述框架采用運(yùn)行軌跡來(lái)表示狀態(tài)的變化，其模型要具有以下特點(diǎn)：

1) 具有完善的元邏輯描述，這種元邏輯作為形式化驗(yàn)證的基礎(chǔ)能提供良好的可信計(jì)算支持。

2) 具有豐富的表達(dá)能力，便于形式化的描述和驗(yàn)證。面對(duì)虛擬化平臺(tái)不同邏輯和不同層次，對(duì)模型需要表達(dá)不同的模塊的邏輯，提供統(tǒng)一的抽象描述。

3) 具有完整的狀態(tài)序列，能夠全面地描述虛擬化平臺(tái)的狀態(tài)序列。虛擬化平臺(tái)功能實(shí)現(xiàn)本質(zhì)是時(shí)間狀態(tài)的改變，模型需要在不損失其語(yǔ)義的情況下使用統(tǒng)一的時(shí)序邏輯描述方法對(duì)功能安全需求的描述。

針對(duì)上述問(wèn)題本文提出一種以動(dòng)作主體和資源為主體對(duì)象，建立主體論域，以主體對(duì)象變?cè)募系秸撚虻挠成鋪?lái)表示系統(tǒng)的狀態(tài)改變與系統(tǒng)的行為遷移。以謂詞邏輯對(duì)安全目標(biāo)進(jìn)行表示，將采用行為主體模型對(duì)XSM進(jìn)行形式化描述。

1 XSM簡(jiǎn)介

XSM[12]是位于Xen Hypervisor中的安全框架，其目的是為不同的安全目標(biāo)提供統(tǒng)一的安全框架，包括為Xen創(chuàng)建統(tǒng)一的接口，允許在模塊中定制安全功能以及從Xen中移除安全模塊特定的代碼。XSM借鑒了Linux操作系統(tǒng)的安全框架Flask。它是一個(gè)靈活的強(qiáng)制訪(fǎng)問(wèn)控制框架，清晰地將執(zhí)行和策略判斷分開(kāi)。它由客體管理器和安全服務(wù)器組成，客體管理器負(fù)責(zé)實(shí)施執(zhí)行安全策略，安全服務(wù)器對(duì)主體訪(fǎng)問(wèn)進(jìn)行判斷給出訪(fǎng)問(wèn)策略。安全框架執(zhí)行過(guò)程如下當(dāng)主體訪(fǎng)問(wèn)客體時(shí)客體管理器將主客體的安全標(biāo)識(shí)發(fā)送給安全服務(wù)器，根據(jù)主客體的安全上下文從安全服務(wù)器提供的通用接口獲取安全策略，再根據(jù)這些策略允許還是拒絕主體對(duì)客體的訪(fǎng)問(wèn)。默認(rèn)情況下主體對(duì)客體的訪(fǎng)問(wèn)是不允許的，只有在策略允許訪(fǎng)問(wèn)的情況下才允許進(jìn)行訪(fǎng)問(wèn)。

2 主體行為模型描述

圖1 XSM框架分解圖

本節(jié)主要闡述主體行為模型的基本框架。主體行為模型是一種將系統(tǒng)行為進(jìn)行抽象為行為對(duì)象的語(yǔ)義模型，該模型將系統(tǒng)的行為和資源抽象為語(yǔ)義對(duì)象變?cè)?，將其建立論域并通過(guò)謂詞來(lái)分析其安全性，把系統(tǒng)動(dòng)作執(zhí)行的功效和系統(tǒng)資源的集合分別看作對(duì)變?cè)獱顟B(tài)的改變和遷移。其框架分解如圖1所示。在行為主體層中主體有訪(fǎng)問(wèn)主體、客體管理器和安全服務(wù)器三個(gè)主體。在這三個(gè)主體間進(jìn)行訪(fǎng)問(wèn)請(qǐng)求，接受安全標(biāo)識(shí)，安全服務(wù)器判定結(jié)果返回三個(gè)行為。在行為實(shí)現(xiàn)層中客體管理器將最近使用的訪(fǎng)問(wèn)策略加入到緩存中，安全服務(wù)器通過(guò)安全標(biāo)識(shí)查找安全上下文找出相應(yīng)的安全策略。優(yōu)化層為了提高效率對(duì)系統(tǒng)緩存加入了RCU算法，其緩存的策略數(shù)為十六。在安全服務(wù)器上對(duì)策略存儲(chǔ)加入了存儲(chǔ)矩陣。

2.1 語(yǔ)義模型框架分析

主體行為模型不同于一般的對(duì)軟件的功能模塊和硬件模塊以功能為導(dǎo)向的分類(lèi)模型，而是使用以主客體來(lái)劃分的分層模型。 對(duì)操作系統(tǒng)進(jìn)行逐級(jí)細(xì)化。為此模型分為主體行為層，行為實(shí)現(xiàn)層，優(yōu)化層三層。

2.1.1 主體行為層

主體行為層是描述系統(tǒng)行為和系統(tǒng)狀態(tài)的改變并不對(duì)系統(tǒng)的動(dòng)作和行為機(jī)制進(jìn)行描述。XSM主要是實(shí)現(xiàn)四個(gè)動(dòng)作：1)主體對(duì)客體發(fā)出訪(fǎng)問(wèn)請(qǐng)求。2)客體管理器接收主體的安全標(biāo)識(shí)。3)將訪(fǎng)問(wèn)對(duì)象和訪(fǎng)問(wèn)主體的安全標(biāo)識(shí)發(fā)送給安全服務(wù)器。4)安全服務(wù)器將判定結(jié)果發(fā)送給客體管理器并由其執(zhí)行。

1) 主體集合

主體行為層對(duì)象集合M1包含以下對(duì)象集合：

(1) 訪(fǎng)問(wèn)Domain

Domain=(D_messagebuff,D_rts_flags,D_sid,D_getfrom,D_vector)

D_messagebuff消息緩沖區(qū)；D_rts_flags表示域所處的狀態(tài)。D_sid表示域的安全標(biāo)識(shí)；D_getfrom:域接受的目標(biāo)對(duì)象標(biāo)識(shí)；D_vector:訪(fǎng)問(wèn)方式請(qǐng)求，主體對(duì)客體進(jìn)行訪(fǎng)問(wèn)請(qǐng)求。

(2) 客體管理器

Object manager=(m_content,m_messbuf,m_vector);

m_content:決策結(jié)果；m_messbuf:可以管理器的消息緩沖區(qū)；m_vector:訪(fǎng)問(wèn)查尋向量由D_sid和D_vector共同構(gòu)成。

(3) 安全服務(wù)器

Security service=(s_tye,s_messbuf,s_policy);

s_type:安全裁決，安全服務(wù)器查詢(xún)后給出的訪(fǎng)問(wèn)許可；s_messbuf:安全服務(wù)器的消息緩沖區(qū);s_policy:安全服務(wù)器庫(kù)中的訪(fǎng)問(wèn)策略隊(duì)列。

(4) 系統(tǒng)狀態(tài)

State=(pest,ss_buffer,next_proc,new_sid)。pest:當(dāng)前域的集合，ss_buffer:系統(tǒng)緩沖區(qū)；next_proc:下一個(gè)要進(jìn)行訪(fǎng)問(wèn)請(qǐng)求的對(duì)象其賦值為新客體NEW，已存在的客體OLD。

(5) 系統(tǒng)狀態(tài)集合S，狀態(tài)S是state的集合。

2) 行為語(yǔ)義

(1) 訪(fǎng)問(wèn)請(qǐng)求行為

訪(fǎng)問(wèn)請(qǐng)求行為在主體行為層中，主要是主體域所指示的消息緩沖區(qū)的請(qǐng)求發(fā)送給客體管理器中。

假設(shè)在狀態(tài)s下域Domain1訪(fǎng)問(wèn)Domain2。在狀態(tài)w下完成其功效，其邏輯功效表示如下：

Send Domain1,Domain2

w.pest.Domain2.D_messbuf:=s.pset.Domain1.D_messbuf

If s.pset.Domain2.D_rts_flags=RECIVE ∧

(s.pest.Domain2.D_getfrom=Domain1)∧

s.manager.m_content=ALLOW∪AUDIT ALLOW

Invariable if other.

(2) 訪(fǎng)問(wèn)判斷行為

當(dāng)主體要訪(fǎng)問(wèn)客體時(shí)，客體管理器會(huì)獲取主體和客體的安全標(biāo)識(shí)，通過(guò)主客體的安全標(biāo)識(shí)和訪(fǎng)問(wèn)向量進(jìn)行判斷查詢(xún)。

假設(shè)在s狀態(tài)下客體管理器manager獲取來(lái)自主體Domain1和客體Domain2的安全標(biāo)識(shí)，在w狀態(tài)下完成：

Gain manager,Domain1,Domain2；

w.manage.m_messbuf:=s.pest.Domain1.D_sid

s.pest.Domain2.D_sid∧s.pest.Domain1.D_vector

If s.pest.Domain1=SEND

(s.pest.Domain2.D_getfrom=Domain1)

客體管理器向安全服務(wù)器發(fā)送查詢(xún)請(qǐng)求，在s狀態(tài)下客體管理器manage向安全服務(wù)器security發(fā)送查詢(xún)，在w狀態(tài)下完成：

Turn managr,security

w.security.s_messbuf:=s.manager.m_content

安全服務(wù)器將查找決策并將決策返回給客體管理器，在s狀態(tài)下安全服務(wù)器security進(jìn)行決策查找返回客體管理器，在w狀態(tài)下完成。

Select security manager

w.security.s_type:=mem security.s_policy

w.manage.s_messbuf:=s.security.s_type

mem操作子為從安全策略隊(duì)列中選取安全策略。

(3) 標(biāo)識(shí)分配行為

當(dāng)產(chǎn)生新的客體時(shí)客體管理器給新客體賦予訪(fǎng)問(wèn)標(biāo)識(shí)并在安全服務(wù)器上產(chǎn)生相應(yīng)的訪(fǎng)問(wèn)上下文。假設(shè)在s狀態(tài)下，客體管理器將從安全服務(wù)器接收的安全標(biāo)識(shí)賦予新生成的Domain在w狀態(tài)下完成：

Assigned security Domain

w.pest.Domain.D_sid:=s.pest.Domain.D_sid∈

s.security.s_policy

2.1.2 行為層

行為層主要是指主體行為層中動(dòng)作具體實(shí)現(xiàn)所涉及的相關(guān)對(duì)象和行為語(yǔ)義。

1) 對(duì)象集合

行為層的對(duì)象集合為M2，其定義如下：

(1) M2包含M1中的元素對(duì)象。

(2) 客體管理器Object manager在主體行為層的基礎(chǔ)上增加VAC_type，VAC_messbuf和VAC_flags三項(xiàng)VAC_type:VAC中緩存的決策類(lèi)型；VAC_messbuf:VAC消息緩存緩存主體和客體的p_SID;VAC_flags:VAC中是否有有效的緩沖結(jié)果，取值有TRUE和FALSE。

(3) 在安全服務(wù)器在主體行為層的基礎(chǔ)上增加s_context。s_context:根據(jù)p_sid映射出的安全上下文。

2) 行為語(yǔ)義

在實(shí)現(xiàn)層的行為語(yǔ)義主要包括了訪(fǎng)問(wèn)緩存AVC查詢(xún)和安全標(biāo)識(shí)映射，安全標(biāo)識(shí)分配三個(gè)語(yǔ)義動(dòng)作。

(1) 訪(fǎng)問(wèn)緩存

在狀態(tài)s下，客體管理器manager的接收主客體的訪(fǎng)問(wèn)請(qǐng)求在w狀態(tài)下完成其實(shí)現(xiàn)過(guò)程分解如下：

① AVC接收主客體的sid和訪(fǎng)問(wèn)向量：

w.manager.VAC_messbuf:=s.manager.m_vector

② AVC通過(guò)m_vector進(jìn)行查詢(xún)是否有相應(yīng)的訪(fǎng)問(wèn)結(jié)果，如果存在則返回執(zhí)行相應(yīng)的結(jié)果：

w. manager. m_messbuf:=

s.manager.VAC_type

if s.manager.VAC_flags=TRUE

③ 若VAC中沒(méi)有相應(yīng)的訪(fǎng)問(wèn)結(jié)果則向安全服務(wù)器發(fā)送訪(fǎng)問(wèn)請(qǐng)求：

w.security.ss_buffer:=s.manager.VAC_messbuff

if s.manager.VAC_flags:=FALSE

(2) 安全標(biāo)識(shí)映射

在收到客體管理器的訪(fǎng)問(wèn)請(qǐng)求后，安全服務(wù)器會(huì)根據(jù)主體客體的p_sid來(lái)查找對(duì)應(yīng)的安全上下文，并給出安全裁定結(jié)果。假設(shè)在s狀態(tài)下目標(biāo)manager向security發(fā)出訪(fǎng)問(wèn)請(qǐng)求，在w狀態(tài)下完成這一功效，其行為語(yǔ)義表示如下：

① 安全服務(wù)器通過(guò)D_sid獲取安全上下文：

s.Domain.D_sid→w.security.s_context

② 將查找到的安全上下文對(duì)策略庫(kù)進(jìn)行查詢(xún)給出安全決斷：

w.security.s_policy:= tail s.security.s_policy

w.manager.AVC_messbuf:=s.security.s_type

(3) 標(biāo)識(shí)分配

標(biāo)識(shí)分配行為分為兩種情況，一種是生成新的客體進(jìn)行標(biāo)識(shí)分配，另一種是將訪(fǎng)問(wèn)策略修改為原有的客體賦予行動(dòng)標(biāo)識(shí)。

假設(shè)在s狀態(tài)下生成新的客體，此時(shí)將客體相關(guān)的安全標(biāo)識(shí)和訪(fǎng)問(wèn)向量存入安全服務(wù)器的安全策略庫(kù)中,其行為在w狀態(tài)下完成，描述如下：

① 新客體生成是將生成的新安全標(biāo)識(shí)和訪(fǎng)問(wèn)向量加入到安全服務(wù)器的策略庫(kù)中。

w.security.s_policy:=s.security.s_policy#m_vectorif

s.next_proc:=NEW

② 如果是對(duì)已有的客體進(jìn)行更新，將安全服務(wù)器決策數(shù)據(jù)庫(kù)中的決策進(jìn)行更新。

w.security.s_policy:=(tail s.security.s_policy)

∧ (s.security.s_policy/m_vector)

if s.next_proc:=OLD

2.1.3 優(yōu)化層

優(yōu)化層是為了提高行為語(yǔ)義層和行為層中行為執(zhí)行效率和性能而引入的對(duì)象和行為語(yǔ)義。

1) 對(duì)象集合

優(yōu)化層對(duì)象集合M3定義如下：

(1) M3包含對(duì)象集合M2

(2) 客體管理器object manager,在其下增加了如下語(yǔ)義對(duì)象list_q.list_q是AVC中就緒的訪(fǎng)問(wèn)決策鏈表

2) 行為語(yǔ)義

為了提高系統(tǒng)效率在AVC查詢(xún)的時(shí)候引入RCU算法進(jìn)行查詢(xún)假設(shè)在s狀態(tài)時(shí)在AVC中執(zhí)行sid的查詢(xún)操作，在w狀態(tài)下完成其在優(yōu)化層語(yǔ)義為：

(1) 當(dāng)生成一次在AVC中沒(méi)有計(jì)算過(guò)的訪(fǎng)問(wèn)決策后將訪(fǎng)問(wèn)決策加入決策鏈表表頭中，其對(duì)應(yīng)的語(yǔ)義如下：

w.list_q:=s_type#s.list_q

w.list_number:=s.list_number+1

if s.manager.VAC_flags:=FALSE

(2) 決策鏈表設(shè)置了16個(gè)節(jié)點(diǎn)，當(dāng)緩存的決策數(shù)量超過(guò)16時(shí)刪除鏈表末尾，語(yǔ)義如下：

w.list_q:=s.list_q/{s_type}

if list_number>16

(3) 當(dāng)接收到新的訪(fǎng)問(wèn)標(biāo)識(shí)和訪(fǎng)問(wèn)向量時(shí)遍歷決策鏈表，尋找匹配的訪(fǎng)問(wèn)決策。如果存在相同的訪(fǎng)問(wèn)策略則返回執(zhí)行決策：

w.manage.AVC_type:=m_vector→s.list_q

if w.manage.AVC_type={s_type|s_type∈list_q∧

list_number<16}

3 形式化描述

我們借助定理證明器Isabelle/HOL來(lái)實(shí)現(xiàn)整個(gè)驗(yàn)證過(guò)程。利用Isabelle/HOL對(duì)上一節(jié)的模型進(jìn)行形式化建模。Isabelle/HOL是一種定理證明工具，采用與函數(shù)式編程類(lèi)似的語(yǔ)法規(guī)范，支持歸納演算、Lambda演算，以及經(jīng)典邏輯證明,擁有強(qiáng)大的類(lèi)型表達(dá)能力。

3.1 Isabelle/HOL的描述

3.1.1 主體論域?qū)ο?/p>

針對(duì)第2節(jié)描述的對(duì)象，Isabelle/HOL方式定義：

datatype security type=

ALLOW|REJECT|AUDIT ALLOW

datatype permission=p1|p2|p3|p4|p5|p6

types pid=int

datatype rts flags=RECEIVE|SEND|NULL

record Domain=D_messagebuff∷message D_rts_flags∷rts flags D_getfrom∷pid D_sid∷pid D_vetor∷permission

record object manager=m_messbuff∷Domain m_content∷security type m_vector∷″pid×permission″ AVC_type∷security type AVC_messbuff ∷pid VAC_flags ∷″TRUE|FALSE″ list_q∷″nat pid list″ list_number∷nat

record security service=s_type∷security type s_messbuf∷string s_context∷string s_policy∷nat list

record state=pest∷″pid Domain″ next_proc∷″NEW|OLD″ S∷″state sett″

security type 是安全決策類(lèi)型；m_vector由域安全標(biāo)識(shí)和訪(fǎng)問(wèn)類(lèi)型共同構(gòu)成，permission為主體訪(fǎng)問(wèn)客體的訪(fǎng)問(wèn)類(lèi)型共有六類(lèi)

3.1.2 行為語(yǔ)義描述

接下來(lái)對(duì)第2節(jié)中的主體行為語(yǔ)義進(jìn)行Isabelle/HOL表述。

(1) 訪(fǎng)問(wèn)請(qǐng)求行為在主體行為層中是“state?state”類(lèi)型函數(shù)。當(dāng)要被訪(fǎng)問(wèn)的Domain處在接收狀態(tài)時(shí)，客體管理器給出的安全決策是允許和審計(jì)允許。同時(shí)將主體消息緩沖區(qū)的消息內(nèi)容發(fā)送到客體的緩沖區(qū)中過(guò)程描述如下：

definition

Send∷″pid ?state?pid?state″where

″Send Domain1 Domain2 s≡

(let newDomain2=(pest s)Domain2

(|D_messbuf:=(D_messbuf((pest s)Domain1)|));

In(if D_rts_flags((pest s)Domain2)=RECEIVE∧

(D_getfrom((pest s)Domian2)=Domain1)∧

m_content((s)manager)=ALLOW|AUDIT ALLOW)

Then s (|pest:=(pest s)(Domain1:=newDomain2))|)″

(2) 訪(fǎng)問(wèn)判斷中客體管理器的AVC緩存要進(jìn)行隊(duì)列刪除，其中用Isabelle/HOL定義的過(guò)濾操作子filter，將不滿(mǎn)足條件的列表元素刪除。

filter type []≡[]

filter type (x#x s)≡(if type x then x#filter type xs else filter type xs)

在列表中尋找符合條件的項(xiàng)的操作子men:

x men []=false

x men (y#ys)≡(if y=x then True else x men ys)

訪(fǎng)問(wèn)判斷就是通過(guò)主體和客體的安全標(biāo)識(shí)和訪(fǎng)問(wèn)方式進(jìn)行判斷。其判斷過(guò)程是先在客體管理器的緩存中查詢(xún)?nèi)绻麤](méi)有將向安全服務(wù)器進(jìn)行查詢(xún)。其描述如下：

definition Gain∷″pid?state?state″ where

″gain manager (Domain1,Domain2) s≡

(let List:=list_q((s)s_type);

newDomain1_1=(pest s)Domain1)(|m_messbuf:=

(D_sid(pest s)Domain1)|);

newDomain1_2=(pest s)Domian1

(|ss_messbuf:=D_sid(pest s)Domain1|);

new Domain2_1=((pest s))Domain2

(|m_messbuf:=(D_sid(pest(|m_messbuf:=

(D_sid(pest s) Domain2)|);

in(if VAC_flags(object manager s)=true)

then s (|manage:=new Domain1_1 new Domain2_1)|)

else(if AVC_flgs(object manager s)=false)

then s (|security:=new Domain1_2 Domain2_1|)″

definition select∷state?state where

″select security manager s≡

(let security_1=(security service s)

(|D_sid(pest s)Domain s_context,s_type:=

(security s)s_policy@(s_type#[])|);

let manager_1=

(object manager s)(|list_q((s)m_type):=filter (x.x≠

m_type)((s)(list_q((s)m_type))),

List:=s_type#((Domain2 s)List),

AVC_messbuf:=(security s)s_type |);

in(if AVC_flags(object manager s)=false)

then s(|manager:=manager_1,security:=security_1)|)″

″gain manager (Domain1,Domain2) s≡

(let List:=list_q((s)s_type);

newDomain1_1=(pest s)Domain1)(|m_messbuf:=

(D_sid(pest s)Domain1)|);

newDomain1_2=(pest s)

Domian1(|ss_messbuf:=D_sid(pest s)Domain1|);

new Domain2_1=((pest s))Domain2

(|m_messbuf:=(D_sid(pest(|m_messbuf:=(D_sid(pest s)

Domain2)|);

in(if VAC_flags(object manager s)=true)

then s (|manage:=new Domain1_1∧new Domain2_1)|)

else(if AVC_flgs(object manager s)=false)then s

(|security:=new Domain1_2∧Domain2_1|)″

definition Select∷state?state where

″select security manager s≡

(let security_1=(security service s)(|D_sid(pest s)

Domain?s_context,s_type:=

(security s)s_policy@(s_type#[])|);

let manager_1=(object manager s)

(|list_q((s)m_type):=filter (λx.x≠

m_type)((s)(list_q((s)m_type))),

List:=s_type#((Domain2 s)List),

AVC_messbuf:=(security s)s_type |);

in(if AVC_flags(object manager s)=false)

then s (|manager:=manager_1,security:=security_1)|) ″

(3) 標(biāo)簽分配行為就是客體管理器將新產(chǎn)生的主客體安全行為的標(biāo)識(shí)添加到安全服務(wù)器的決策庫(kù)中，并由安全服務(wù)器為主客體賦予安全標(biāo)識(shí)，其中分為兩個(gè)狀態(tài)添加新標(biāo)識(shí)和更新標(biāo)識(shí)，Isabelle/HOL過(guò)程描述如下：

definition Assigned∷″state?state″ where

″Assigned security manager s≡

(let security_1=(security service s)

(|s_messbuf:=(s)m_vector,s_policy+1:=

(security s)s_policy@(m_vector#[])|);

let security_2:=(security security s)(|s_messbuf:=(manager s)

m_vector,s_policy:=(security s)s_policy@(m_vector#[])|);

let Domain=(pest s)Domain(|D_sid((pest s)Domain):=|)

in (if(next_proc):=NEW)

then s(|security:=(security s)security_1,Domain:=(pest s)

Domain|)else s(security:=(security s)security_2,Domain:=(pest s)Domain))″

4 安全框架驗(yàn)證

4.1 安全框架的安全需求

XSM的安全需求包括機(jī)密性、完整性和隔離性。機(jī)密性是XSM保證主客體間不能出現(xiàn)違規(guī)訪(fǎng)問(wèn)，以免泄露信息。完整性是指數(shù)據(jù)的完整性和系統(tǒng)功效的完整性，數(shù)據(jù)的完整性指數(shù)據(jù)代碼不能被惡意修改。系統(tǒng)功效的完整性指系統(tǒng)能達(dá)到設(shè)計(jì)所需的功能。隔離性有數(shù)據(jù)隔離性和行為隔離性：數(shù)據(jù)的隔離性指產(chǎn)生的數(shù)據(jù)頁(yè)表不存在交集；行為隔離性是指主體間產(chǎn)生狀態(tài)遷移不會(huì)干擾主體其他的行為。限于篇幅本文對(duì)訪(fǎng)問(wèn)行為和決策查詢(xún)行為的行為隔離性進(jìn)行證明。

4.2 安全需求描述的時(shí)序邏輯

分層模型采用狀態(tài)機(jī)模型進(jìn)行描述，即系統(tǒng)是每一個(gè)主體集合，通過(guò)行為作為主體間狀態(tài)轉(zhuǎn)移的約束條件。設(shè)V是有限的主體狀態(tài)集合，V0是初始的主體的狀態(tài)集合，T是主體狀態(tài)V的遷移集合，假設(shè)安全需求為pr，如果有(V,T)╞pr,(V0,T)╞pr那么稱(chēng)其滿(mǎn)足安全需求。

由于模型是對(duì)狀態(tài)序列的描述，由于每個(gè)狀態(tài)下的后續(xù)狀態(tài)的不確定性，所以我們使用CTL對(duì)安全需求進(jìn)行描述。設(shè)φ是時(shí)序上的狀態(tài)命題，則描述如下：

s╞Aφ,對(duì)于狀態(tài)s之后所有路徑上的時(shí)序上命題φ成立；

s╞Eφ，對(duì)于狀態(tài)s之后存在某個(gè)路徑上的時(shí)序上命題φ成立；

對(duì)于單條路徑的CTL描述如下：

s╞Xφ，在單序列上狀態(tài)s的下一時(shí)序上的命題φ成立；

s╞Fφ，在s狀態(tài)后的在單個(gè)序列下將來(lái)的時(shí)序上的命題φ成立；

s╞Gφ，在s狀態(tài)后的某個(gè)序列下將來(lái)所有的時(shí)序上，命題φ成立。

4.3 隔離性的謂詞描述

(1) 訪(fǎng)問(wèn)請(qǐng)求行為，主體能通過(guò)客體管理器賦予的訪(fǎng)問(wèn)權(quán)限訪(fǎng)問(wèn)客體行為，謂詞表示如下：

?s∈S,Domain1∷Domain,Domain2∷Domain.(s(send Domain1 Domain2 )├EF(λw∷state.w.pest.Domain2.D_messbuf:=

s.pest.Domain1.D_messbuf)) (φ1)

其中λ是完成功效的狀態(tài)抽象

(2) 安全服務(wù)器查詢(xún)行為，通過(guò)Domain的sid映射出安全上下文，通過(guò)安全上下文給出安全策略，謂詞表示如下：

?s∈S, security∷security service, manager∷object manager(s(Select security manager)├EF(λw∷state.s.Domain.D_sid→w.security.s_type)) (φ2)

安全框架的隔離性是指訪(fǎng)問(wèn)請(qǐng)求行為與安全服務(wù)器安全策略查詢(xún)?cè)诔跏紶顟B(tài)s0下，后續(xù)序列中的時(shí)序狀態(tài)都成立。謂詞公式表示如下：

s0╞AG(φ1∧φ2)

4.4 隔離性形式化證明

本節(jié)對(duì)上述公式進(jìn)行證明已滿(mǎn)足隔離性。在實(shí)驗(yàn)中需要用到的命題類(lèi)型為：

datatype F= Atom ″state?bool″|

Neg F|

And F|

AG F|

EF F|

其中Atom為原子命題，合取命題And，否定命題Neg，時(shí)序命題AG，EF等。state?bool表示狀態(tài)s下原子命題f成立時(shí)，f.fs=true。

系統(tǒng)單步執(zhí)狀態(tài)轉(zhuǎn)換函數(shù)step定義：

fun step∷″state?action?state″

″step s (send Domain1 Domain2)=Send Domain1 Domain2 s″|″

″step s (gain Domain1 Domain2)= Gain Domain1 Domain2 s″|″

″step s (select security manager)=Select security manager s″|″

首先要將狀態(tài)對(duì)安全需求的滿(mǎn)足進(jìn)行定義，即在s狀態(tài)下f成立，定義如下：

primrec sat∷″sate?F?bool″(″__?_″)where

″s╞Atomic a=(a∈Sat_Atomic s) ″ |

″s╞And b c=(s╞b∧s╞c ) ″|

″s╞AG f=(?w.(s,w)∈SS*→w╞f) ″

″ s╞EF f=(?w.(s,w)∈SS*→w╞f) ″

其中SS為狀態(tài)后繼定義為SS∷″(state×state)set″。表示當(dāng)前狀態(tài)和后繼狀態(tài)的集合。

接下來(lái)我們可以將“state,action├formula”的邏輯演算式轉(zhuǎn)變成“state╞formula”的證明式，其轉(zhuǎn)換方法如下:

definition action∷″state?(state?state)?F?bool″

(″(_,_├_)″) where ″s,act├f≡(act s)╞f″

之后我們定義滿(mǎn)足安全需求命題的狀態(tài)集的函數(shù)：

primrec SAT∷″F?state set″ where

″SAT(Atomic a)={s.a∈Sat_Atomic s }″|

″SAT(And b c)=SAT b∩SAT c″|

″SAT(Negitive d)=─SAT d″|

″SAT(AG f)={s.?w.(s,w)∈SS*→w∈SAT f)}″

″SAT(EX f)=Ifp(ΛX.(SS-1X)∪SAT f) ″

對(duì)于EF f的滿(mǎn)足性證明過(guò)程首先證明其滿(mǎn)足狀態(tài)f,即函數(shù)SAT f;當(dāng)計(jì)算得到狀態(tài)集X，接下來(lái)計(jì)算f的前繼狀態(tài)，即“SS-1X”;最終在Ifp函數(shù)來(lái)計(jì)算最小不動(dòng)點(diǎn)。根據(jù)上述EF f可知我們需要通過(guò)構(gòu)造主體行為的完成狀態(tài)實(shí)現(xiàn)來(lái)證明在當(dāng)前狀態(tài)下滿(mǎn)足f，然后通過(guò)推演來(lái)證明主體行為完成狀態(tài)是行為發(fā)生狀態(tài)的后繼。

下面開(kāi)始對(duì)安全框架的語(yǔ)義模型是否滿(mǎn)足安全需求進(jìn)行證明。

引理1 主體訪(fǎng)問(wèn)行為滿(mǎn)足φ1：

lemma Send_ok:

″?s∈S,Domain1∷Domain,Domain2∷Domain.

(s(send Domain1 Domain2 )├

EF(λw∷state.w.pest.Domain2.D_messbuf:=

s.pest.Domain1.D_messbuf)) ″

證明：通過(guò)state，action├f轉(zhuǎn)化成單步執(zhí)行函數(shù)，構(gòu)造訪(fǎng)問(wèn)請(qǐng)求函數(shù)Send的訪(fǎng)問(wèn)狀態(tài)和完成功效狀態(tài)。根據(jù)2.1.1節(jié)可知如果在s狀態(tài)的后繼狀態(tài)t執(zhí)行訪(fǎng)問(wèn)行為Send Domain1 Domain2則此時(shí)t為接收狀態(tài)。按照Send函數(shù)定義在t直接后繼狀態(tài)w完成其功效，w即為完成狀態(tài)。其證明過(guò)程如下：

apply(simp add: step_def sat_def Send_def )

apply(subgoal_tac ″w=step t (send Domain2 Domain1) ″)

apply (blast)

apply (simp add:send_def)

apply (auto)

done

使用simp方法對(duì)單步滿(mǎn)足性(step_def)和系統(tǒng)行為(Send_def)進(jìn)行展開(kāi)化簡(jiǎn)，使用″w=step t (send Domain2 Domain1)構(gòu)造訪(fǎng)問(wèn)狀態(tài)和完成功效狀態(tài)；blast使用經(jīng)典推理方法進(jìn)行前向推導(dǎo)，由auto進(jìn)行目標(biāo)簡(jiǎn)化，通過(guò)已有的結(jié)論進(jìn)行證明。

類(lèi)似的,可以證明引理2安全服務(wù)器查詢(xún)行為功效完整性。

引理2 安全服務(wù)器查詢(xún)行為完整性符合φ2的功效完整性，定義如下：

lemma select_ok:

″?s∈S, security∷security service, manager∷object manager (s(select security manager)├A(λw∷state.?i.(security mem(s_policy w)i))) ″

證明過(guò)程如下：

apply(simp add:step_def sat_def Select_def )

apply(subgoal_tac ″w=step t (Select security gain) ″)

apply(blast)

apply(erule mem_def)

apply(best)

apply(auto)

done

其中erule mem_def表示對(duì)Isabelle/HOL中l(wèi)ist的mem函數(shù)消除的前向推導(dǎo)；best采用最優(yōu)查找進(jìn)行搜索驗(yàn)證。

定理1 訪(fǎng)問(wèn)詢(xún)問(wèn)功能的隔離性，在s0之后的將來(lái)狀態(tài)中，具有主客體訪(fǎng)問(wèn)的完整性和訪(fǎng)問(wèn)策略查詢(xún)的完整性。

theorem MSI:

″s0╞AG(?s∈S,Domain1∷Domain,Domain2∷Domain.(s(send Domain1 Domain2 )├EF(λw∷state.w.pest.Domain2.D_messbuf:=s.pest.Domain1.D_messbuf))∧?s∈S, security∷security service manager∷object manager (s (select security manager)├A(λw∷state.i.(security mem(s_policy w)i)))) ″

由引理1和引理2可知當(dāng)客體管理器在授權(quán)訪(fǎng)問(wèn)的同時(shí)不會(huì)影響安全服務(wù)器對(duì)其他客體的訪(fǎng)問(wèn)決策的查詢(xún)，因此在s0狀態(tài)的后續(xù)狀態(tài)可以保證其隔離性。

apply(simp add: step_sat_def sat_def)

apply(blast intro: send_ok select_ok)

apply(auto)

done

證明完成

4.5 證明結(jié)果

通過(guò)Isabelle證明如圖2所示。證明結(jié)果為“No subgoals”表明證明邏輯完備，不存在未證明的子目標(biāo)。

圖2 證明結(jié)果

通過(guò)結(jié)果可知，其兩個(gè)子目標(biāo)主客體訪(fǎng)問(wèn)的完整性和安全服務(wù)器查詢(xún)功能的完整性證明完備。兩個(gè)功能的完整性實(shí)現(xiàn)未產(chǎn)生沖突和干擾，安全框架滿(mǎn)足系統(tǒng)的隔離性。

通過(guò)引理1的證明成立，證明主客體功能的完整性，對(duì)引理2的證明，說(shuō)明安全服務(wù)器查詢(xún)功能的完整性。引理1和引理2共同證明定理1成立。換句話(huà)說(shuō)隔離性是建立在功能完整性上的。系統(tǒng)在初始狀態(tài)s下任何后續(xù)狀態(tài)都能完成期望的功效。

5 結(jié) 語(yǔ)

本文基于主體與動(dòng)作對(duì)XSM進(jìn)行建模，采用Isabelle/HOL對(duì)其過(guò)程進(jìn)行形式化描述并驗(yàn)證其隔離性，提出一種通過(guò)主體與動(dòng)作進(jìn)行形式化分析的方法，為形式化分析和驗(yàn)證工作提供一種方法和思路。然而在驗(yàn)證過(guò)程中還存在繁瑣的手工驗(yàn)證使其工作量巨大的問(wèn)題，安全需求的謂詞分析還有不很直觀的地方，其產(chǎn)生的原因主要是通過(guò)時(shí)序邏輯進(jìn)行描述。這些都不利于以后的應(yīng)用，因此下一步可通過(guò)類(lèi)型論引入自動(dòng)證明，借鑒信息流的方法進(jìn)行安全需求分析的表示。

[1] Klein G, Andronick J, Elphinstone K, et al. seL4: formal verification of an operating-system kernel[J]. Communications of the Acm, 2010, 53(6):107-115.

[3] Elphinstone K, Heiser G. From L3 to seL4 what have we learnt in 20 years of L4 microkernels?[C]// Twenty-Fourth ACM Symposium on Operating Systems Principles. 2013:133-150.

[4] Freitas L, Mcdermott J. Formal methods for security in the Xenon hypervisor[J]. International Journal on Software Tools for Technology Transfer, 2011, 13(5):463-489.

[5] Calzavara S, Rabitti A, Bugliesi M. Formal Verification of Liferay RBAC[M]// Engineering Secure Software and Systems. Springer International Publishing, 2015:1-16.

[6] Nipkow T, Paulson L C, Wenzel M. Isabelle/HOL: a proof assistant for higher-order logic[M]. Springer Science & Business Media, 2002.

[7] Jansen B, Ramasamy H G V, Schunter M. Policy enforcement and compliance proofs for Xen virtual machines.[C]// International Conference on Virtual Execution Environments. 2008:101-110.

[8] Von Hagen W. Professional Xen Virtualization[J]. Wiley John+Sons, 2008.

[9] 錢(qián)振江, 劉葦, 黃皓. 操作系統(tǒng)對(duì)象語(yǔ)義模型(OSOSM)及形式化驗(yàn)證[J]. 計(jì)算機(jī)研究與發(fā)展, 2012, 49(12):2702-2712.

[10] 屈延文. 形式語(yǔ)義學(xué)基礎(chǔ)與形式說(shuō)明[M]. 科學(xué)出版社, 2009.

[11] 佩萊德. 軟件可靠性方法[M]. 機(jī)械工業(yè)出版社, 2012.

[12] O'Sullivan B, Goerzen J, Stewart D B. Real world haskell: Code you can believe in[M]. O'Reilly Media, Inc., 2008.

[13] Freitas L, Whiteside I. Proof patterns for formal methods[M]. Springer International Publishing, 2014.

[14] 周宇, 胡軍, 葛季棟. 一種層次式時(shí)間自動(dòng)機(jī)模型檢測(cè)方法[J]. 計(jì)算機(jī)應(yīng)用與軟件, 2012,29(11):48-51.

[15] 劉暢, 李海峰, 沈國(guó)華,等. 支持SPIN驗(yàn)證的詳細(xì)級(jí)SFMEA方法研究[J]. 計(jì)算機(jī)應(yīng)用與軟件, 2016,33(5):281-284.

XSM SEMANTIC MODEL AND FORMAL VERIFICATIO OF SECURITY REQUIREMENTS

Zhu Xianwei Zhu Zhiqiang Sun Lei

(InformationEngineeringUniversity,Zhengzhou450001,Henan,China)

As a popular open-source virtualization tools, Xen is used more and more frequently. Xsm (Xen Security Module), as the security framework of the Xen, has also been widespread concern. There are a lot of research to verify the system operations correctness by formal method. The existing formalization research is mainly concerned with the code correctness of the system implementation. Thus, the system is modeled formally which subject behavior is taken as operating system semantic model in the perspective of system function, and the security requirements of XMS is analyzed by adopting the CLT sequential logic. As the connection of the rationality of system design and formal verification, the semantic model is responsible for the formal verification of the XSM, and the Isabelle/HOL is utilized to verify the consistency between functions and security requirements so as to demonstrate whether the XSM meets the security requirements.

XSM Semantic model Formal verification Security analysis Isabelle/HOL

2016-07-09。國(guó)家高技術(shù)研究發(fā)展計(jì)劃項(xiàng)目(2012AA012704)。?，F(xiàn)威，碩士生，主研領(lǐng)域：復(fù)雜的系統(tǒng)建模與仿真、信息安全。朱智強(qiáng)，教授。孫磊，副研究員。

TP311

A

10.3969/j.issn.1000-386x.2017.06.056