刘苇

作品数：3被引量：19H指数：2
导出分析报告
供职机构：南京大学更多>>
发文主题：形式化验证操作系统形式化设计定理证明ISABELLE更多>>
发文领域：自动化与计算机技术更多>>
发文期刊：《计算机研究与发展》《计算机工程》《计算机学报》更多>>
所获基金：国家高技术研究发展计划江苏省科技支撑计划项目江苏省“六大人才高峰”高层次人才项目江苏省高校自然科学研究项目更多>>
-
在结果中检索

检索结果分析

署名顺序

  • 全部
  • 第一作者
结果分析中...
共 条 记 录，以下是1-3
全选清除导出
参考文献引证文献引用追踪
视图：
排序：
操作系统对象语义模型(OSOSM)及形式化验证被引量：11
《计算机研究与发展》2012年第12期2702-2712,共11页钱振江 刘苇 黄皓 
国家"八六三"高技术研究发展计划基金项目(2011AA01A202);江苏省科技支撑计划基金项目(BE2008124);国家自然科学基金创新研究群体项目(60721002);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035);江苏省高校自然科学研究项目(12KJB520001)
操作系统的复杂性使得其安全性问题日益突出.有不少的研究工作采用形式化的方式对现有的操作系统进行了正确性的验证,这些工作主要是采用程序形式逻辑验证代码级的功能实现性.从系统设计的角度,以高阶逻辑和类型论为基础,提出了操作系...
关键词：操作系统对象 语义模型 形式化设计 安全性验证 Isabelle定理证明 
操作系统形式化设计与验证综述被引量：7
《计算机工程》2012年第11期234-238,共5页钱振江 刘苇 黄皓 
国家"863"计划基金资助项目"分布式可信计算系统研究"(2007AA01Z409);国家自然科学基金资助项目(60721002);江苏省科技支撑计划基金资助项目"可信操作系统新技术研发"(BE2008124)
对操作系统的形式化设计和验证的概念进行介绍,描述其框架和基本方法。比较和分析操作系统宏内核和微内核结构,调查多个设计和验证项目,阐述项目的验证目标、方法、优缺点和进展情况。在总结研究现状的基础上,分析和展望操作系统形式化...
关键词：操作系统 形式化设计 形式化验证 定理证明 系统安全 框架设计 
HybridHP:一种轻型的内核完整性监控方案及其形式化验证被引量：2
《计算机学报》2012年第7期1462-1474,共13页钱振江 刘苇 黄皓 
国家"八六三"高技术研究发展计划项目基金(2007AA01Z409);江苏省科技支撑计划自然科学基金(BE2008124);江苏省"六大人才高峰"高层次人才项目(2011-DZXX-035)资助~~
虽然传统的虚拟化监控方法可以在一定程度上保障操作系统安全.然而,虚拟监控器VMM中管理域Domain0的存在以及操作系统级的切换所带来的性能损失是很多具有大型应用的操作系统所不能接受的.注重硬件虚拟化技术的监控能力而摒弃其不必要...
关键词：硬件虚拟化 内核完整性 安全监控 安全攻击 Isabelle形式化验证 
全选清除导出
共1页<1>
检索报告 对象比较 聚类工具 使用帮助 返回顶部