XSM語義模型及安全需求形式化驗證

祝現威 朱智強 孫 磊

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

XSM語義模型及安全需求形式化驗證

祝現威 朱智強 孫 磊

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

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

XSM 語義模型 形式化驗證 安全性分析 Isabelle/HOL

0 引 言

云計算作為一種新型的計算模式，迅速成為計算機技術發展的熱點。然而近年來，隨著云計算的廣泛應用，云安全問題越來越被學術界和工業界所關注。在眾多的云安全問題中，作為云計算基礎支撐的虛擬化平臺的安全問題是基礎。

Xen是劍橋大學開發的一個開源的虛擬化平臺，在現有云計算環境中得到廣泛應用，為了增強其安全性，一些研究學者借鑒安全操作系統的理論和技術提出了針對Xen虛擬化平臺的安全框架XSM。

XSM位于硬件和應用軟件的中間層，一方面為Xen虛擬化平臺的安全性提供保證；另一方面還必須保證其自身的可靠性和安全性。然而，過去雖然研究人員對XSM開展了很多研究并進行了實現，但是XSM的安全性缺乏形式化方法的分析和驗證。眾所周知，形式化方法的安全分析與驗證是構造高安全操作系統不可缺少的，同樣，本文認為對XSM進行形式化驗證將為構造高安全虛擬化平臺提供理論支撐和技術保障。

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

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

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

2) 具有豐富的表達能力，便于形式化的描述和驗證。面對虛擬化平臺不同邏輯和不同層次，對模型需要表達不同的模塊的邏輯，提供統一的抽象描述。

3) 具有完整的狀態序列，能夠全面地描述虛擬化平臺的狀態序列。虛擬化平臺功能實現本質是時間狀態的改變，模型需要在不損失其語義的情況下使用統一的時序邏輯描述方法對功能安全需求的描述。

針對上述問題本文提出一種以動作主體和資源為主體對象，建立主體論域，以主體對象變元的集合到論域的映射來表示系統的狀態改變與系統的行為遷移。以謂詞邏輯對安全目標進行表示，將采用行為主體模型對XSM進行形式化描述。

1 XSM簡介

XSM[12]是位于Xen Hypervisor中的安全框架，其目的是為不同的安全目標提供統一的安全框架，包括為Xen創建統一的接口，允許在模塊中定制安全功能以及從Xen中移除安全模塊特定的代碼。XSM借鑒了Linux操作系統的安全框架Flask。它是一個靈活的強制訪問控制框架，清晰地將執行和策略判斷分開。它由客體管理器和安全服務器組成，客體管理器負責實施執行安全策略，安全服務器對主體訪問進行判斷給出訪問策略。安全框架執行過程如下當主體訪問客體時客體管理器將主客體的安全標識發送給安全服務器，根據主客體的安全上下文從安全服務器提供的通用接口獲取安全策略，再根據這些策略允許還是拒絕主體對客體的訪問。默認情況下主體對客體的訪問是不允許的，只有在策略允許訪問的情況下才允許進行訪問。

2 主體行為模型描述

圖1 XSM框架分解圖

本節主要闡述主體行為模型的基本框架。主體行為模型是一種將系統行為進行抽象為行為對象的語義模型，該模型將系統的行為和資源抽象為語義對象變元，將其建立論域并通過謂詞來分析其安全性，把系統動作執行的功效和系統資源的集合分別看作對變元狀態的改變和遷移。其框架分解如圖1所示。在行為主體層中主體有訪問主體、客體管理器和安全服務器三個主體。在這三個主體間進行訪問請求，接受安全標識，安全服務器判定結果返回三個行為。在行為實現層中客體管理器將最近使用的訪問策略加入到緩存中，安全服務器通過安全標識查找安全上下文找出相應的安全策略。優化層為了提高效率對系統緩存加入了RCU算法，其緩存的策略數為十六。在安全服務器上對策略存儲加入了存儲矩陣。

2.1 語義模型框架分析

主體行為模型不同于一般的對軟件的功能模塊和硬件模塊以功能為導向的分類模型，而是使用以主客體來劃分的分層模型。 對操作系統進行逐級細化。為此模型分為主體行為層，行為實現層，優化層三層。

2.1.1 主體行為層

主體行為層是描述系統行為和系統狀態的改變并不對系統的動作和行為機制進行描述。XSM主要是實現四個動作：1)主體對客體發出訪問請求。2)客體管理器接收主體的安全標識。3)將訪問對象和訪問主體的安全標識發送給安全服務器。4)安全服務器將判定結果發送給客體管理器并由其執行。

1) 主體集合

主體行為層對象集合M1包含以下對象集合：

(1) 訪問Domain

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

D_messagebuff消息緩沖區；D_rts_flags表示域所處的狀態。D_sid表示域的安全標識；D_getfrom:域接受的目標對象標識；D_vector:訪問方式請求，主體對客體進行訪問請求。

(2) 客體管理器

Object manager=(m_content,m_messbuf,m_vector);

m_content:決策結果；m_messbuf:可以管理器的消息緩沖區；m_vector:訪問查尋向量由D_sid和D_vector共同構成。

(3) 安全服務器

Security service=(s_tye,s_messbuf,s_policy);

s_type:安全裁決，安全服務器查詢后給出的訪問許可；s_messbuf:安全服務器的消息緩沖區;s_policy:安全服務器庫中的訪問策略隊列。

(4) 系統狀態

State=(pest,ss_buffer,next_proc,new_sid)。pest:當前域的集合，ss_buffer:系統緩沖區；next_proc:下一個要進行訪問請求的對象其賦值為新客體NEW，已存在的客體OLD。

(5) 系統狀態集合S，狀態S是state的集合。

2) 行為語義

(1) 訪問請求行為

訪問請求行為在主體行為層中，主要是主體域所指示的消息緩沖區的請求發送給客體管理器中。

假設在狀態s下域Domain1訪問Domain2。在狀態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) 訪問判斷行為

當主體要訪問客體時，客體管理器會獲取主體和客體的安全標識，通過主客體的安全標識和訪問向量進行判斷查詢。

假設在s狀態下客體管理器manager獲取來自主體Domain1和客體Domain2的安全標識，在w狀態下完成：

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)

客體管理器向安全服務器發送查詢請求，在s狀態下客體管理器manage向安全服務器security發送查詢，在w狀態下完成：

Turn managr,security

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

安全服務器將查找決策并將決策返回給客體管理器，在s狀態下安全服務器security進行決策查找返回客體管理器，在w狀態下完成。

Select security manager

w.security.s_type:=mem security.s_policy

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

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

(3) 標識分配行為

當產生新的客體時客體管理器給新客體賦予訪問標識并在安全服務器上產生相應的訪問上下文。假設在s狀態下，客體管理器將從安全服務器接收的安全標識賦予新生成的Domain在w狀態下完成：

Assigned security Domain

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

s.security.s_policy

2.1.2 行為層

行為層主要是指主體行為層中動作具體實現所涉及的相關對象和行為語義。

1) 對象集合

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

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

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

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

2) 行為語義

在實現層的行為語義主要包括了訪問緩存AVC查詢和安全標識映射，安全標識分配三個語義動作。

(1) 訪問緩存

在狀態s下，客體管理器manager的接收主客體的訪問請求在w狀態下完成其實現過程分解如下：

① AVC接收主客體的sid和訪問向量：

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

② AVC通過m_vector進行查詢是否有相應的訪問結果，如果存在則返回執行相應的結果：

w. manager. m_messbuf:=

s.manager.VAC_type

if s.manager.VAC_flags=TRUE

③ 若VAC中沒有相應的訪問結果則向安全服務器發送訪問請求：

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

if s.manager.VAC_flags:=FALSE

(2) 安全標識映射

在收到客體管理器的訪問請求后，安全服務器會根據主體客體的p_sid來查找對應的安全上下文，并給出安全裁定結果。假設在s狀態下目標manager向security發出訪問請求，在w狀態下完成這一功效，其行為語義表示如下：

① 安全服務器通過D_sid獲取安全上下文：

s.Domain.D_sid→w.security.s_context

② 將查找到的安全上下文對策略庫進行查詢給出安全決斷：

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

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

(3) 標識分配

標識分配行為分為兩種情況，一種是生成新的客體進行標識分配，另一種是將訪問策略修改為原有的客體賦予行動標識。

假設在s狀態下生成新的客體，此時將客體相關的安全標識和訪問向量存入安全服務器的安全策略庫中,其行為在w狀態下完成，描述如下：

① 新客體生成是將生成的新安全標識和訪問向量加入到安全服務器的策略庫中。

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

s.next_proc:=NEW

② 如果是對已有的客體進行更新，將安全服務器決策數據庫中的決策進行更新。

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

∧ (s.security.s_policy/m_vector)

if s.next_proc:=OLD

2.1.3 優化層

優化層是為了提高行為語義層和行為層中行為執行效率和性能而引入的對象和行為語義。

1) 對象集合

優化層對象集合M3定義如下：

(1) M3包含對象集合M2

(2) 客體管理器object manager,在其下增加了如下語義對象list_q.list_q是AVC中就緒的訪問決策鏈表

2) 行為語義

為了提高系統效率在AVC查詢的時候引入RCU算法進行查詢假設在s狀態時在AVC中執行sid的查詢操作，在w狀態下完成其在優化層語義為：

(1) 當生成一次在AVC中沒有計算過的訪問決策后將訪問決策加入決策鏈表表頭中，其對應的語義如下：

w.list_q:=s_type#s.list_q

w.list_number:=s.list_number+1

if s.manager.VAC_flags:=FALSE

(2) 決策鏈表設置了16個節點，當緩存的決策數量超過16時刪除鏈表末尾，語義如下：

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

if list_number>16

(3) 當接收到新的訪問標識和訪問向量時遍歷決策鏈表，尋找匹配的訪問決策。如果存在相同的訪問策略則返回執行決策：

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來實現整個驗證過程。利用Isabelle/HOL對上一節的模型進行形式化建模。Isabelle/HOL是一種定理證明工具，采用與函數式編程類似的語法規范，支持歸納演算、Lambda演算，以及經典邏輯證明,擁有強大的類型表達能力。

3.1 Isabelle/HOL的描述

3.1.1 主體論域對象

針對第2節描述的對象，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 是安全決策類型；m_vector由域安全標識和訪問類型共同構成，permission為主體訪問客體的訪問類型共有六類

3.1.2 行為語義描述

接下來對第2節中的主體行為語義進行Isabelle/HOL表述。

(1) 訪問請求行為在主體行為層中是“state?state”類型函數。當要被訪問的Domain處在接收狀態時，客體管理器給出的安全決策是允許和審計允許。同時將主體消息緩沖區的消息內容發送到客體的緩沖區中過程描述如下：

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) 訪問判斷中客體管理器的AVC緩存要進行隊列刪除，其中用Isabelle/HOL定義的過濾操作子filter，將不滿足條件的列表元素刪除。

filter type []≡[]

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

在列表中尋找符合條件的項的操作子men:

x men []=false

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

訪問判斷就是通過主體和客體的安全標識和訪問方式進行判斷。其判斷過程是先在客體管理器的緩存中查詢如果沒有將向安全服務器進行查詢。其描述如下：

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) 標簽分配行為就是客體管理器將新產生的主客體安全行為的標識添加到安全服務器的決策庫中，并由安全服務器為主客體賦予安全標識，其中分為兩個狀態添加新標識和更新標識，Isabelle/HOL過程描述如下：

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 安全框架驗證

4.1 安全框架的安全需求

XSM的安全需求包括機密性、完整性和隔離性。機密性是XSM保證主客體間不能出現違規訪問，以免泄露信息。完整性是指數據的完整性和系統功效的完整性，數據的完整性指數據代碼不能被惡意修改。系統功效的完整性指系統能達到設計所需的功能。隔離性有數據隔離性和行為隔離性：數據的隔離性指產生的數據頁表不存在交集；行為隔離性是指主體間產生狀態遷移不會干擾主體其他的行為。限于篇幅本文對訪問行為和決策查詢行為的行為隔離性進行證明。

4.2 安全需求描述的時序邏輯

分層模型采用狀態機模型進行描述，即系統是每一個主體集合，通過行為作為主體間狀態轉移的約束條件。設V是有限的主體狀態集合，V0是初始的主體的狀態集合，T是主體狀態V的遷移集合，假設安全需求為pr，如果有(V,T)╞pr,(V0,T)╞pr那么稱其滿足安全需求。

由于模型是對狀態序列的描述，由于每個狀態下的后續狀態的不確定性，所以我們使用CTL對安全需求進行描述。設φ是時序上的狀態命題，則描述如下：

s╞Aφ,對于狀態s之后所有路徑上的時序上命題φ成立；

s╞Eφ，對于狀態s之后存在某個路徑上的時序上命題φ成立；

對于單條路徑的CTL描述如下：

s╞Xφ，在單序列上狀態s的下一時序上的命題φ成立；

s╞Fφ，在s狀態后的在單個序列下將來的時序上的命題φ成立；

s╞Gφ，在s狀態后的某個序列下將來所有的時序上，命題φ成立。

4.3 隔離性的謂詞描述

(1) 訪問請求行為，主體能通過客體管理器賦予的訪問權限訪問客體行為，謂詞表示如下：

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

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

其中λ是完成功效的狀態抽象

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

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

安全框架的隔離性是指訪問請求行為與安全服務器安全策略查詢在初始狀態s0下，后續序列中的時序狀態都成立。謂詞公式表示如下：

s0╞AG(φ1∧φ2)

4.4 隔離性形式化證明

本節對上述公式進行證明已滿足隔離性。在實驗中需要用到的命題類型為：

datatype F= Atom ″state?bool″|

Neg F|

And F|

AG F|

EF F|

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

系統單步執狀態轉換函數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″|″

首先要將狀態對安全需求的滿足進行定義，即在s狀態下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為狀態后繼定義為SS∷″(state×state)set″。表示當前狀態和后繼狀態的集合。

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

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

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

之后我們定義滿足安全需求命題的狀態集的函數：

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) ″

對于EF f的滿足性證明過程首先證明其滿足狀態f,即函數SAT f;當計算得到狀態集X，接下來計算f的前繼狀態，即“SS-1X”;最終在Ifp函數來計算最小不動點。根據上述EF f可知我們需要通過構造主體行為的完成狀態實現來證明在當前狀態下滿足f，然后通過推演來證明主體行為完成狀態是行為發生狀態的后繼。

下面開始對安全框架的語義模型是否滿足安全需求進行證明。

引理1 主體訪問行為滿足φ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)) ″

證明：通過state，action├f轉化成單步執行函數，構造訪問請求函數Send的訪問狀態和完成功效狀態。根據2.1.1節可知如果在s狀態的后繼狀態t執行訪問行為Send Domain1 Domain2則此時t為接收狀態。按照Send函數定義在t直接后繼狀態w完成其功效，w即為完成狀態。其證明過程如下：

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方法對單步滿足性(step_def)和系統行為(Send_def)進行展開化簡，使用″w=step t (send Domain2 Domain1)構造訪問狀態和完成功效狀態；blast使用經典推理方法進行前向推導，由auto進行目標簡化，通過已有的結論進行證明。

類似的,可以證明引理2安全服務器查詢行為功效完整性。

引理2 安全服務器查詢行為完整性符合φ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))) ″

證明過程如下：

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表示對Isabelle/HOL中list的mem函數消除的前向推導；best采用最優查找進行搜索驗證。

定理1 訪問詢問功能的隔離性，在s0之后的將來狀態中，具有主客體訪問的完整性和訪問策略查詢的完整性。

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可知當客體管理器在授權訪問的同時不會影響安全服務器對其他客體的訪問決策的查詢，因此在s0狀態的后續狀態可以保證其隔離性。

apply(simp add: step_sat_def sat_def)

apply(blast intro: send_ok select_ok)

apply(auto)

done

證明完成

4.5 證明結果

通過Isabelle證明如圖2所示。證明結果為“No subgoals”表明證明邏輯完備，不存在未證明的子目標。

圖2 證明結果

通過結果可知，其兩個子目標主客體訪問的完整性和安全服務器查詢功能的完整性證明完備。兩個功能的完整性實現未產生沖突和干擾，安全框架滿足系統的隔離性。

通過引理1的證明成立，證明主客體功能的完整性，對引理2的證明，說明安全服務器查詢功能的完整性。引理1和引理2共同證明定理1成立。換句話說隔離性是建立在功能完整性上的。系統在初始狀態s下任何后續狀態都能完成期望的功效。

5 結 語

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

[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] 錢振江, 劉葦, 黃皓. 操作系統對象語義模型(OSOSM)及形式化驗證[J]. 計算機研究與發展, 2012, 49(12):2702-2712.

[10] 屈延文. 形式語義學基礎與形式說明[M]. 科學出版社, 2009.

[11] 佩萊德. 軟件可靠性方法[M]. 機械工業出版社, 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] 周宇, 胡軍, 葛季棟. 一種層次式時間自動機模型檢測方法[J]. 計算機應用與軟件, 2012,29(11):48-51.

[15] 劉暢, 李海峰, 沈國華,等. 支持SPIN驗證的詳細級SFMEA方法研究[J]. 計算機應用與軟件, 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。國家高技術研究發展計劃項目(2012AA012704)。祝現威，碩士生，主研領域：復雜的系統建模與仿真、信息安全。朱智強，教授。孫磊，副研究員。

TP311

A

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