积分商城

最新搜索： 系统安全工程手册 软件评估 stm8s 电子线路SPICE设计与仿真 Allegro封装库 库
您现在的位置是：首页 > 技术资料 > 微内核架构内存管理的形式化设计和验证方法研究
推荐星级：
  • 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

【关注视频号领20积分】   【关注公众号立即送20积分】

部分页面预览

（完整内容请下载后查看）
1
Vol． 45 No． 1  
Jan． 2017  
第
期
电
子
学
报
2017  
1
ACTA ELECTRONICA SINICA  
年
月
微内核架构内存管理的形式化设计和验证方法研究  
1，2  
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  
1，2  
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 Technology，Nanjing University，Nanjing，Jiangsu 210023，China;  
2． School of Computer Science and Engineering，Changshu Institute of Technology，Suzhou，Jiangsu 215500，China)  
Abstract: The correctness of design and implementation of operating systems is difficult to be described with the tra-  
ditional quantitative methods，because 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 level，and use the Hoare triples to describe the previous and post conditions of the interface functions，as the  
definitions of function correctness． We take the module of memory management in the self-implemented VSOS ( Verified  
Secure Operating System) as an example，to illustrate our formal method． Meanwhile，we formally describe the constructed  
memory management model and operation semantics of system behaviors in the Isabelle/HOL theorem prover，and 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  
对于关键的核心软件系统如操作系统  
．
并未得到完全验证  
System，OS) ，  
如何保证其正确可靠一直以来都是学术界  
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，  
、 (  
负责处理中断和异常 进程调度以及进程间通信 即  
，{ 0…MaxPage} Isabelle/HOL  
，
集
是
中的集合表示方法  
MaxPage  
的整数构成的  
) ; 1，  
消息的发送与接收 系统任务运行在特权级 负责向  
0
表示由大于等于 且小于等于  
，
用户态的系统进程提供内核调用的服务 这些内核调  
．
集合  
I/O  
、 ，  
端口 在进程间拷贝数据等 它们是一  
pa state  
－
， record，  
表示页框分配器的状态 类型为 其  
用包括读写  
，
组特权的调用 仅授权的用户态系统进程能够请求这  
Free  
nat “int list” ，  
到 的映射 给定输入  
中字段  
是一个从  
， ;  
组服务 其他的用户进程则无法请求这组服务 时钟任  
i( i MaxOrder) ，  
≤
“Free i”  
i
表示 级空闲链  
参数  
函数值  
1， ，  
务运行在特权级 负责管理硬件时钟 用户态进程无  
;
表中所有空闲块的编号 字段  
Allocated  
用来表示已分  
，
法直接获取它的服务 而必须通过系统任务间接地获  
． order、num、retval  
配物理页框的编号所构成的集合  
等
．
．
取它的服务  
字段用来记录参数和返回值  
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日榜单

热门下载

推荐下载

本站上的所有资源均为源于网上收集或者由用户自行上传，仅供学习和研究使用，无任何商业目的，版权归原作如有侵权，请 来信指出，本站将立即改正。

ICP许可证号：京ICP证070360号     21IC电子网 2000- 版权所有

京ICP备11013301号

京公网安备 11010802024343号