CAJ | 학술논문

采用数学形式化方法对操作系统进行设计和验证可以保证系统的高度安全性。目前已有的操作系统形式化研究工作主要是验证系统的实现在代码级的程序正确性。提出一种操作系统形式化设计和验证的方法，采用操作系统对象语义模型（OSOSM）对系统的设计进行形式化建模，使用带有时序逻辑的高阶逻辑对操作系统的安全需求进行分析和定义。对象语义模型作为系统设计和形式化验证的联系。以实现和验证过的可信微内核操作系统VTOS为实例，阐述形式化设计和安全需求分析，并使用定理证明器Isabelle/HOL①对系统的设计和安全需求的一致性进行验证，表明VTOS达到预期的安全性。
채용수학형식화방법대조작계통진행설계화험증가이보증계통적고도안전성。목전이유적조작계통형식화연구공작주요시험증계통적실현재대마급적정서정학성。제출일충조작계통형식화설계화험증적방법，채용조작계통대상어의모형（OSOSM）대계통적설계진행형식화건모，사용대유시서라집적고계라집대조작계통적안전수구진행분석화정의。대상어의모형작위계통설계화형식화험증적련계。이실현화험증과적가신미내핵조작계통VTOS위실례，천술형식화설계화안전수구분석，병사용정리증명기Isabelle/HOL①대계통적설계화안전수구적일치성진행험증，표명VTOS체도예기적안전성。
The mathematical formal methods for operating system design and verification achievehigh assurance of system security.The existing formalization research works in the scope ofoperating system mainly focus on showing that an implementation complies with the program correctness in the code-level verification.In this paper,we propose a method for formal designand verification.We adopt the operating system object semantics model (OSOSM)for formal modeling of the system design,and analyze and define the security requirements using higher-order logic (HOL)with temporal logic (TL).We view OSOS Mas the link between systemdesign and formal verification,and take the self-implemented and verified trusted operating system (VTOS)as an example to illustrate formal design and analysis of security requirements.Meanwhile,we use the theorem prover Isabelle/HOL to verify the consistency between system design and security requirements,and show that VTOS achieves the desired security.