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