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

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

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

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

?，F(xiàn)威 朱智強 孫 磊

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

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

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

0 引 言

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

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

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

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

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

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

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

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

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

1 XSM簡介

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

2 主體行為模型描述

圖1 XSM框架分解圖

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

2.1 語義模型框架分析

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

2.1.1 主體行為層

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

1) 主體集合

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

(1) 訪問Domain

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

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

(2) 客體管理器

Object manager=(m_content,m_messbuf,m_vector);

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

(3) 安全服務器

Security service=(s_tye,s_messbuf,s_policy);

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

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

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

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

2) 行為語義

(1) 訪問請求行為

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

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

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

假設在s狀態(tài)下客體管理器manager獲取來自主體Domain1和客體Domain2的安全標識，在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)

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

Turn managr,security

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

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

Select security manager

w.security.s_type:=mem security.s_policy

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

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

(3) 標識分配行為

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

Assigned security Domain

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

s.security.s_policy

2.1.2 行為層

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

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:根據(jù)p_sid映射出的安全上下文。

2) 行為語義

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

(1) 訪問緩存

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

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

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

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

w. manager. m_messbuf:=

s.manager.VAC_type

if s.manager.VAC_flags=TRUE

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

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

if s.manager.VAC_flags:=FALSE

(2) 安全標識映射

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

① 安全服務器通過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狀態(tài)下生成新的客體，此時將客體相關的安全標識和訪問向量存入安全服務器的安全策略庫中,其行為在w狀態(tài)下完成，描述如下：

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

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

s.next_proc:=NEW

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

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)化層是為了提高行為語義層和行為層中行為執(zhí)行效率和性能而引入的對象和行為語義。

1) 對象集合

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

(1) M3包含對象集合M2

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

2) 行為語義

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

(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個節(jié)點，當緩存的決策數(shù)量超過16時刪除鏈表末尾，語義如下：

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

if list_number>16

(3) 當接收到新的訪問標識和訪問向量時遍歷決策鏈表，尋找匹配的訪問決策。如果存在相同的訪問策略則返回執(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來實現(xiàn)整個驗證過程。利用Isabelle/HOL對上一節(jié)的模型進行形式化建模。Isabelle/HOL是一種定理證明工具，采用與函數(shù)式編程類似的語法規(guī)范，支持歸納演算、Lambda演算，以及經典邏輯證明,擁有強大的類型表達能力。

3.1 Isabelle/HOL的描述

3.1.1 主體論域對象

針對第2節(jié)描述的對象，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節(jié)中的主體行為語義進行Isabelle/HOL表述。

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

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) 標簽分配行為就是客體管理器將新產生的主客體安全行為的標識添加到安全服務器的決策庫中，并由安全服務器為主客體賦予安全標識，其中分為兩個狀態(tài)添加新標識和更新標識，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保證主客體間不能出現(xiàn)違規(guī)訪問，以免泄露信息。完整性是指數(shù)據(jù)的完整性和系統(tǒng)功效的完整性，數(shù)據(jù)的完整性指數(shù)據(jù)代碼不能被惡意修改。系統(tǒng)功效的完整性指系統(tǒng)能達到設計所需的功能。隔離性有數(shù)據(jù)隔離性和行為隔離性：數(shù)據(jù)的隔離性指產生的數(shù)據(jù)頁表不存在交集；行為隔離性是指主體間產生狀態(tài)遷移不會干擾主體其他的行為。限于篇幅本文對訪問行為和決策查詢行為的行為隔離性進行證明。

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

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

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

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

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

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

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

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

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

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)

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

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

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

s0╞AG(φ1∧φ2)

4.4 隔離性形式化證明

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

datatype F= Atom ″state?bool″|

Neg F|

And F|

AG F|

EF F|

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

系統(tǒng)單步執(zhí)狀態(tài)轉換函數(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)對安全需求的滿足進行定義，即在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″。表示當前狀態(tài)和后繼狀態(tài)的集合。

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

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

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

之后我們定義滿足安全需求命題的狀態(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) ″

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

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

引理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轉化成單步執(zhí)行函數(shù)，構造訪問請求函數(shù)Send的訪問狀態(tài)和完成功效狀態(tài)。根據(jù)2.1.1節(jié)可知如果在s狀態(tài)的后繼狀態(tài)t執(zhí)行訪問行為Send Domain1 Domain2則此時t為接收狀態(tài)。按照Send函數(shù)定義在t直接后繼狀態(tài)w完成其功效，w即為完成狀態(tài)。其證明過程如下：

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)和系統(tǒng)行為(Send_def)進行展開化簡，使用″w=step t (send Domain2 Domain1)構造訪問狀態(tài)和完成功效狀態(tài)；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中l(wèi)ist的mem函數(shù)消除的前向推導；best采用最優(yōu)查找進行搜索驗證。

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

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狀態(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 證明結果

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

圖2 證明結果

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

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

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

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

[11] 佩萊德. 軟件可靠性方法[M]. 機械工業(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] 周宇, 胡軍, 葛季棟. 一種層次式時間自動機模型檢測方法[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。國家高技術研究發(fā)展計劃項目(2012AA012704)。?，F(xiàn)威，碩士生，主研領域：復雜的系統(tǒng)建模與仿真、信息安全。朱智強，教授。孫磊，副研究員。

TP311

A

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