南京大学学报（自然科学版）2017，Vol.53Issue(3)：579-589,11.DOI:10.13232/j.cnki.jnju.2017.03.022
VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究
VSOS-HAM:Research on Isabelle/HOL-based OS kernel hardwareabstract model and formal verification method
摘要
Abstract
The formal method is a reliable one to ensure the correctness of design and implementation of operating system.The formal design and verification of operating system is still an extremely complex progress.Because of its low-level,it is difficult to validate the correctness of the assembly layer.How to effectively model for assembly codes,and easily validate the correctness of the semantics and effectiveness becomes a hot topic in the field of operating system formalization.In this paper,we present the method of formal verification of design and implementation of operating system on the assembly layer.We construct the kernel hardware abstract model of operating system,and describe the operational semantics of instructions.Based on this abstract model,we define the data objects affecting the system state,and establish the system state domain.With the description of operational semantics of instructions,we describe the transition functions of system states.Meanwhile,we define the constructed kernel hardware abstract model of operating system in Isabelle/HOL theorem prover,and take the self-implemented trusted operating system(VSOS)as the example to validate the correctness of the design and implementation of system on the assembly layer.The result shows that the proposed method is feasible and efficient.关键词
操作系统/内核硬件抽象模型/形式化验证/Isabelle/HOL/定理证明Key words
operating system/kernel hardware abstract model/formal verification/Isabelle/HOL/theorem proving分类
信息技术与安全科学引用本文复制引用
钱振江,黄皓,宋方敏..VSOS-HAM:基于Isabelle/HOL的OS内核硬件抽象模型和形式化验证方法研究[J].南京大学学报（自然科学版）,2017,53(3):579-589,11.基金项目
国家自然科学基金(61402057),江苏省科技计划自然科学研究项目(BK20140418),中国博士后科学基金(2015M571737),江苏省高校"青蓝工程"优秀青年骨干教师培养对象项目(2017) （61402057）
