推荐星级:
  • 1
  • 2
  • 3
  • 4
  • 5

微内核架构内存管理的形式化设计和验证方法研究

更新时间:2019-12-25 02:56:53 大小:1M 上传用户:zhiyao6查看TA发布的资源 标签:内存管理 下载积分:1分 评价赚积分 (如何评价?) 打赏 收藏 评论(0) 举报

资料介绍

由于巨大的规模和复杂性,操作系统的设计和实现的正确性很难用传统的定量方法来描述.本文阐述对微内核操作系统的形式化设计和验证的方法.在汇编层利用非确定性自动机对系统进行形式化建模,并使用Hoare三元组描述模块接口函数的前后置条件,作为函数正确性的定义.以实现的VSOS(Verified Secure Operating System)内存管理模块为例,在Isabelle/HOL定理证明器环境中对建立的内存管理模型和系统行为的操作语义进行形式化描述,并对内存管理模块的设计和实现的正确性进行验证.结果表明,这一方法是可行的和高效的.


部分文件列表

文件名 大小
微内核架构内存管理的形式化设计和验证方法研究.pdf 1M

部分页面预览

(完整内容请下载后查看)
1
Vol. 45 No. 1  
Jan. 2017  
2017  
1
ACTA ELECTRONICA SINICA  
构内证方法研究  
12  
2
2
2
1
1
, , , , ,  
江 刘汤 力 敏  
( 1.  
京大学计算机科学与技术系 京  
210023; 2.  
理工算机科学与苏苏  
215500)  
:
.  
大的规模复杂系统的实现的正确统的定方法来描述 本文述  
,  
系统的方法 自动机对系统进行使用  
Hoare  
.  
描述正确的定实现的  
VSOS( Verified Secure Operating System)  
Isabelle/HOL  
理证明器环境对建模型系统行为进行描述  
在  
对内实现的正确进行方法和高效的  
:
;
;
;
;
关键词  
中图分类号  
URL: http: / /www. ejournal. org. cn  
系统 化验理证明  
TP316 0372-2112 ( 2017) 01-0251-06  
DOI: 10. 3969 /j. issn. 0372-2112. 2017. 01. 035  
:
:
A
:
文章编号  
文献标识码  
电子学报  
Research on Method of Formal Design and Verification of  
Memory Management Based on Microkernel Architecture  
12  
2
2
2
1
1
QIAN Zhen-jiang LIU Yong-jun YAO Yu-feng TANG Li HUANG Hao SONG Fang-min  
( 1. Department of Computer Science and TechnologyNanjing UniversityNanjingJiangsu 210023China;  
2. School of Computer Science and EngineeringChangshu Institute of TechnologySuzhouJiangsu 215500China)  
Abstract: The correctness of design and implementation of operating systems is difficult to be described with the tra-  
ditional quantitative methodsbecause of the enormous size and complexity. This paper illustrates our method of formal de-  
sign and verification of microkernel operating system. We construct the system model with the non-deterministic automaton  
in the assembly leveland use the Hoare triples to describe the previous and post conditions of the interface functionsas the  
definitions of function correctness. We take the module of memory management in the self-implemented VSOS ( Verified  
Secure Operating System) as an exampleto illustrate our formal method. Meanwhilewe formally describe the constructed  
memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem proverand verify the  
correctness of design and implementation of the memory management. The result shows that the method proposed is feasible  
and efficient.  
Key words: operating system; memory management; formal design; formal verification; theorem proving  
Verification) .  
于系统的大规模  
1
引言  
大的 并且块  
2]  
( Operating  
系统如系统  
得到证  
SystemOS) ,  
正确以来学术界  
90  
现 在 大 学  
Shao  
上 世  
和工化验技术以数理为  
Zhong  
Flint  
的  
项目化验证方了  
Ver-  
实现 辑 编 言  
3]  
, ,  
基础 点 目公认为是软  
作  
4]  
ind  
正确技术 化验指根系统的规  
iML  
HOL  
提出λ  
对数  
或属使方法正确正确  
丰富描述特  
Verisoft  
大 型 的 计 算 机 系 统 发 项  
在于整个算机系统自层  
( Pervasive Formal  
时  
Flint  
项目方  
1]  
5]  
OS  
中的能  
方法证  
6]  
应用明  
块  
: 2015-05-15;  
: 2015-08-17;  
:
责任编辑 怀银  
收稿日期  
修回日期  
:
基金项目 国 家 自 然 科 学 基 金  
( No. 61402057 ) ;  
( No. BK20140418 ) ;  
( No.  
中 国 博 士 科 学 基 金  
科 技 计 划 自 然 科 学 研 究 项 目  
( No. 2011-DZXX-035) ;  
2015M571737) ;  
“ ”  
项目  
( No. 12KJB520001)  
自然科学研究项目  
252  
2017  
ICT  
( NICTA)  
L4.  
的任本质且  
国家  
实验室  
导的  
verified seL4  
项目对  
进行化的正确验  
实现程  
. VSOS  
7]  
. Klein  
在报介绍工作 的目标是  
的 一的虚拟图  
8]  
Isabelle/HOL  
使用  
证明效果模  
为两个模  
. L4. verified  
: .  
配器和配器子模负  
型的期定义  
项目主要中于本  
OS  
系统进行化验未过考虑环  
( al-  
统的框  
loc pages) ( free pages) .  
程  
正确证  
框  
OS  
证工作项目组  
的  
OS  
子模配器的基础之上进  
9]  
( OSOSM)  
OS  
虚 拟 虚 拟 区 间  
提出了采用  
进行描述方法 实现全可信  
VTOS( Verified Trusted Operating System) .  
象语模型  
作  
OS  
( mmap)  
( munmap) 、  
及扩展用于  
虚拟区间  
( brk)  
提  
本文以实  
区  
VTOS  
VSOS ( Verified Secure Operating  
的虚拟图  
现的  
本  
System)  
对  
OS  
计  
3
VSOS  
存管理模式化建模  
,  
方法 考虑因素提下 利定  
10]  
VSOS  
以  
配器子模块  
VSOS  
方  
VSOS  
自动对  
进行形  
描述前  
述  
使用  
Hoare  
助  
Isabelle/HOL  
、 、  
理证明器表 函数  
,  
正确的定本文对建的  
,  
数 和件  
Isabelle/HOL  
模型系统的在  
Isabelle/HOL  
证明 器 进 行 描 述 尝 试 在  
理  
环 境 对  
模型的描述  
( 1)  
态  
配器关常量在  
VSOS  
实现的正确进行证  
Isabelle/HOL  
2
VSOS  
存管理模计  
的定下  
2. 1 VSOS  
MaxPage  
0x7fff,  
框架  
大的为  
MaxPage  
修  
VSOS  
4 .  
框架分成 最  
理内存总小  
; MaxOrder 10,  
明  
、  
心态系统任时  
10  
.  
务组成 它们共权级  
2
; U  
全  
支持为  
页  
0,  
(  
处理常 进度以即  
{ 0MaxPage} Isabelle/HOL  
中的集合方法  
MaxPage  
数构的  
) ; 1,  
息的发收 系统任权级 向  
0
示由大于等于 且小于等于  
的系统用的服务 这调  
集合  
I/O  
,  
它们一  
pa state  
record,  
配器态 类为 其  
读写  
组特的用系统求这  
Free  
nat int list,  
入  
段  
从  
, ;  
组服务 其的用无法求这组服务 任  
i( i MaxOrder) ,  
Free i”  
i
链  
数  
值  
1, ,  
权级 态进无  
;
的编段  
Allocated  
分  
直接获服务 必须系统任获  
. ordernumretval  
的编合  
服务  
记录数和值  
2 ,  
位于第 是设备理和管  
state  
C  
机器态 其段 是到  
. 3  
直接供服务位于第 服务  
word32”  
射 用程序示  
服务器提服务即作为  
OS  
32  
; D  
段 是到字型的射  
户提接  
. 4  
系统用 第 括  
Shell  
程序 其  
; R  
程序段 是器  
Shell OS  
与  
存管理模计  
VSOS  
口  
其类型  
regs,  
包含寄  
2. 2  
、 、  
指针 器和器  
; call ret  
段  
记录用的次函令  
于系统任核  
系统供服务 将模  
call call ret  
1,  
令  
ret  
加  
1.  
于系统任可以在基本不的  
call ret  
减  
表  
配器在  
, ,  
减少信的而提高系统的  
( 2)  
Isabelle/HOL  
data-  
使用  
能  

全部评论(0)

暂无评论

上传资源 上传优质资源有赏金

  • 打赏
  • 30日榜单

推荐下载