期刊导航
期刊开放获取
河南省图书馆
退出
期刊文献
+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息
检索
高级检索
期刊导航
共找到
1
篇文章
<
1
>
每页显示
20
50
100
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
显示方式:
文摘
详细
列表
相关度排序
被引量排序
时效性排序
XSM语义模型及安全需求形式化验证
被引量:
1
1
作者
祝现威
朱智强
孙磊
《计算机应用与软件》
2017年第6期314-321,共8页
Xen作为一种开源流行的虚拟化工具,使用越来越频繁。作为Xen的安全框架XSM(Xen Security Module)也受到广泛的关注。许多研究者通过形式化的方式对现有的操作系统进行正确性的验证,目前已有的形式化研究主要是验证系统实现的代码正确性...
Xen作为一种开源流行的虚拟化工具,使用越来越频繁。作为Xen的安全框架XSM(Xen Security Module)也受到广泛的关注。许多研究者通过形式化的方式对现有的操作系统进行正确性的验证,目前已有的形式化研究主要是验证系统实现的代码正确性。从系统功能角度提出了一种以主体行为为操作系统语义模型对系统进行形式化建模,并采用CTL时序逻辑对XSM安全需求进行分析。语义模型作为系统设计合理性和形式化验证的联系,对XSM进行形式化验证,并使用Isabelle/HOL验证功能和安全需求的一致性,以说明XSM是否符合安全需求。
展开更多
关键词
xsm
语义模型
形式化验证
安全性分析
isabelle/
hol
下载PDF
职称材料
题名
XSM语义模型及安全需求形式化验证
被引量:
1
1
作者
祝现威
朱智强
孙磊
机构
信息工程大学密码工程学院
出处
《计算机应用与软件》
2017年第6期314-321,共8页
基金
国家高技术研究发展计划项目(2012AA012704)
文摘
Xen作为一种开源流行的虚拟化工具,使用越来越频繁。作为Xen的安全框架XSM(Xen Security Module)也受到广泛的关注。许多研究者通过形式化的方式对现有的操作系统进行正确性的验证,目前已有的形式化研究主要是验证系统实现的代码正确性。从系统功能角度提出了一种以主体行为为操作系统语义模型对系统进行形式化建模,并采用CTL时序逻辑对XSM安全需求进行分析。语义模型作为系统设计合理性和形式化验证的联系,对XSM进行形式化验证,并使用Isabelle/HOL验证功能和安全需求的一致性,以说明XSM是否符合安全需求。
关键词
xsm
语义模型
形式化验证
安全性分析
isabelle/
hol
Keywords
xsm semantic model formal verification security analysis isabelle/hol
分类号
TP311 [自动化与计算机技术—计算机软件与理论]
下载PDF
职称材料
题名
作者
出处
发文年
被引量
操作
1
XSM语义模型及安全需求形式化验证
祝现威
朱智强
孙磊
《计算机应用与软件》
2017
1
下载PDF
职称材料
已选择
0
条
导出题录
引用分析
参考文献
引证文献
统计分析
检索结果
已选文献
上一页
1
下一页
到第
页
确定
用户登录
登录
IP登录
使用帮助
返回顶部